--- a/CCCGraph.agda	Mon May 04 07:48:50 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 08:59:08 2020 +0900
@@ -257,13 +257,14 @@
    csc-origin {a} {a} f {p} | id a = id a
    csc-origin {a} {⊤} f {p} | ○ a = ○ a
    csc-origin {a} {c ∧ d} f {p} | < g , h > = < csc-origin (λ x → (proj₁ (f x))) {g} , csc-origin (λ x → (proj₂ (f x)))  {h} >
-   csc-origin {a} {atom b} f {p} | iv {_} {_} {d} (arrow {e} {b} x) g = iv (arrow x) ( csc-origin {!!} {g} ) where
-       lemma : ?
-       lemma = ?
-   csc-origin {a} {b} f {p} | iv π g = iv π ( csc-origin (λ x → (f x , {!!} ) ) {g} )
+   csc-origin {a} {atom b} f {p} | iv {_} {_} {d} (arrow {e} {b} x) g = {!!}
+   csc-origin {b ∧ b1} {b} f {p} | iv {b ∧ b1} {b} {b ∧ b1} π (id (b ∧ b1)) = iv π (id (b ∧ b1))
+   csc-origin {a} {b} f {p} | iv {a} {b} {b ∧ b1} π < g , h > = iv π < csc-origin f {g} , id a >  
+   csc-origin {a} {b} f {p} | iv {a} {b} {b ∧ b1} π (iv h g) = iv π ( csc-origin (λ x → (f x , {!!} )) {iv h g} )
    csc-origin {a} {b} f {p} | iv π' g = {!!}
    csc-origin {a} {b} f {p} | iv ε g = {!!}
-   csc-origin {a} {c <= b} f {p} | iv {_} {_} {d} (x *) g = iv ( ( csc-origin (λ x → f {!!} (proj₂ x)) {x} ) * ) ( csc-origin (λ y → {!!} ) {{!!}} ) -- f  : fobj a → fobj b → fobj c
+   csc-origin {a} {c <= b} f {p} | iv {a} {c <= b} {d} (x *) g = 
+      iv {a} {c <= b} {d} ( ( csc-origin (λ x → f {!!} (proj₂ x)) {x} ) * ) ( csc-origin (λ y → {!!} ) {g} ) where -- f  : fobj a → fobj b → fobj c
 
 
 ---