# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588558542 -32400
# Node ID b33007dfdc4e8c6bac0b514f62d4ee9c9af83d71
# Parent  8fa27a146c845c75896f4e3a82863a70116f4bbc
...

diff -r 8fa27a146c84 -r b33007dfdc4e CCCGraph.agda
--- a/CCCGraph.agda	Mon May 04 08:59:08 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 11:15:42 2020 +0900
@@ -258,13 +258,20 @@
    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 = {!!}
-   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 {b ∧ b1} {b} f {p} | iv π (id (b ∧ b1)) = iv π (id (b ∧ b1))
+   csc-origin {a} {b} f {p} | iv  π < 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 {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
+      iv {a} {c <= b} {d} ( ( csc-origin (λ y → h (proj₂ y)) {x} ) * ) (csc-origin (λ z → {!!} ) {{!!}} )  where -- f  : fobj a → fobj b → fobj c
+        h : fobj b → fobj c
+        h = f {!!}
+      --     h : fobj d → fobj a
+      --     h dx = {!!}
+
+   rev :   {a : Obj PL} {b : vertex G } → Hom CSC a (atom b) → {p : Arrows a (atom b) } → Hom PL a (atom b)
+   rev = {!!}
 
 
 ---
@@ -433,11 +440,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) ) → (y : 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 b} f y = {!!} where
-          c-map-b :  (a : ccc-from-graph.Objs g ) → (y : Hom (cat (csc g)) a (atom b) )
-             →  Hom (cat c) (cobj {g} {c} f a) (cobj {g} {c} f (atom b))
-          c-map-b a y with FObj (ccc-from-graph.CS g ) a 
-          ... | t = {!!}
+       c-map {g} {c} {a} {atom b} f y with ccc-from-graph.rev g {a} {b} y {?}
+       c-map {g} {c} {atom b} {atom b} f y | id (atom b) = {!!}
+       c-map {g} {c} {a} {atom b} f y | iv (arrow x) t = {!!}
+       c-map {g} {c} {a} {atom b} f y | iv π t = {!!}
+       c-map {g} {c} {a} {atom b} f y | iv π' t = {!!}
+       c-map {g} {c} {a} {atom b} 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)))