# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589541009 -32400
# Node ID d13e0981e6676971f9277af4f165b136716a2862
# Parent  92f8f57467e355771918094dd888e85cf4c4113b
η on Graph to CCC

diff -r 92f8f57467e3 -r d13e0981e667 CCCGraph.agda
--- a/CCCGraph.agda	Fri May 15 17:59:15 2020 +0900
+++ b/CCCGraph.agda	Fri May 15 20:10:09 2020 +0900
@@ -416,7 +416,7 @@
        open forgetful  
        open ccc-from-graph
        --                                        η : Hom Grph a (FObj UX (F a))
-       --                    f : edge g x y   ----------------------------------->  g21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
+       --                    f : edge g x y   ----------------------------------->  m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
        --  Graph g     x  ----------------------> y : vertex g                             ↑
        --                       arrow f             : Hom (PL g) (atom x) (atom y)         |
        --  PL g     atom x  ------------------> atom y : Obj (PL g)                        | UX : Functor Sets Graph
@@ -430,7 +430,14 @@
        F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
        F g = record { cat = Sets  {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
        η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a))
-       η a = record { vmap = λ y → {!!} y ;  emap = λ f → {!!} } where
+       η a = record { vmap = λ y → vm y ;  emap = λ f → em f }  where
+            fo : Graph  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}
+            fo = forgetful.fobj {c₁} {c₂} (F a)
+            vm : (y : vertex a ) →  vertex (g21 fo) 
+            vm y =  vmap (m21 fo) (ccc-from-graph.fobj a (atom y))
+            em :  { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y)
+            em {x} {y} f = emap (m21 fo) (ccc-from-graph.fmap a (iv (arrow f) (id _)))
+            
        --    k : ( y : vertex a) → Set (c₁ ⊔ c₂)
        --    k y = ( e : vertex a ) → graphtocat.Chain a e y
        --    mm : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}