# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588546130 -32400
# Node ID a79b08e1244705b9e3d62309c6ec964039673d37
# Parent  fa302d99fa40634c2268e0cf8aeb97bbe1e5c619
reverse functor of CS

diff -r fa302d99fa40 -r a79b08e12447 CCCGraph.agda
--- a/CCCGraph.agda	Sat May 02 09:30:44 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 07:48:50 2020 +0900
@@ -252,6 +252,18 @@
                     Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
         *-cong refl = refl
 
+   csc-origin :  {a b : Obj PL} → Hom CSC a b → {p : Arrows a b } → Hom PL a b
+   csc-origin {a} {b} f {p} with p
+   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} {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
 
 
 ---
@@ -419,16 +431,15 @@
        cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
        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} {atom a} {atom b} f y with y (λ w → {!!} ) a
-       c-map {g} {c} {atom a} {atom a} f y | id a = id1 (cat c) (cobj {g} {c} f (atom a))
-       c-map {g} {c} {atom a} {atom b} f y | next {a} {d} {b} x t = (cat c) [ emap f x o {!!} ] 
-       c-map {g} {c} {⊤} {atom x} f y = {!!}
-       c-map {g} {c} {a ∧ b} {atom x} f y = {!!}
-       c-map {g} {c} {b <= a} {atom x} f y = {!!}
+           → (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} {⊤} 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)) ))
+       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ w → x (proj₁ w) (proj₂ w)))
        solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
        solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = c-map {g} {c} f ; isFunctor = {!!} } ; ccf = {!!} }