# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588594403 -32400
# Node ID 5eed22f4a75dc14074aaa0c97d6627178aa29db1
# Parent  625baac95ec8bb82d71daf20ee8fb68e018763bf
again ...

diff -r 625baac95ec8 -r 5eed22f4a75d CCCGraph.agda
--- a/CCCGraph.agda	Mon May 04 15:45:20 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 21:13:23 2020 +0900
@@ -263,9 +263,12 @@
        pε : {a c : Objs } (f : Arrows a ((atom b <= c) ∧ c))
            → plcase (iv ε f) (λ y → proj₁ (fmap f y ) (proj₂ (fmap f y )) )
 
-   rev : {a : Objs } → {b : vertex G}  → ( sf : Hom CSC a (atom b)) → {f : Hom PL a (atom b)} →  Hom PL a (atom b) 
-   rev {a} {b} sf {f} with plcase f sf
-   ... | t = {!!}
+   rev : {a : Objs } → {b : vertex G}  → ( sf : Hom CSC a (atom b)) → ∀{f : Hom PL a (atom b)} → FMap CS f ≡ sf  →  Hom PL a (atom b) 
+   rev {atom b} {b} .(λ x → x) {id (atom b)} refl = id (atom b)
+   rev {a} {b} .(λ a₁ y → graphtocat.next x (fmap f₁ a₁ y)) {iv (arrow x) f₁} refl = iv (arrow x) f₁
+   rev {a} {b} .(λ a₁ → proj₁ (fmap f₁ a₁)) {iv π f₁} refl = iv π f₁
+   rev {a} {b} .(λ a₁ → proj₂ (fmap f₁ a₁)) {iv π' f₁} refl = iv π' f₁
+   rev {a} {b} .(λ a₁ → proj₁ (fmap f₁ a₁) (proj₂ (fmap f₁ a₁))) {iv ε f₁} refl = iv ε f₁
 
 
 ---
@@ -434,7 +437,12 @@
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
        c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Obj (cat (csc g))}
            → (f : Hom Grph g (FObj UX c) ) → Hom (cat (csc g)) A B → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       c-map {g} {c} {a} {atom x} f y = ?
+       c-map {g} {c} {a} {atom x} f y with ccc-from-graph.rev g y {{!!}} refl
+       c-map {g} {c} {atom x} {atom x} f y | id (atom x) = id1 (cat c) (cobj {g} {c} f (atom x))
+       c-map {g} {c} {a} {atom x} f y | iv (arrow x₁) t = {!!}
+       c-map {g} {c} {a} {atom x} f y | iv π t = {!!}
+       c-map {g} {c} {a} {atom x} f y | iv π' t = {!!}
+       c-map {g} {c} {a} {atom x} f y | iv ε t = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ w → proj₁ (z w))) (c-map f (λ w → proj₂ (z w)))
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ w → x (proj₁ w) (proj₂ w)))