# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589640333 -32400
# Node ID 24248f9249c558c343273d93cfc59c1a7450b749
# Parent  2385fdd6818beba5abc2a84461bbc92c8c86dc6f
...

diff -r 2385fdd6818b -r 24248f9249c5 CCCGraph.agda
--- a/CCCGraph.agda	Fri May 15 20:43:42 2020 +0900
+++ b/CCCGraph.agda	Sat May 16 23:45:33 2020 +0900
@@ -283,6 +283,19 @@
      : ∀{X Y : vertex C} → edge C X Y → Set (c₁ ⊔ c₂ ) where
   mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
 
+eq-vertex1 : {c₁ c₂ : Level} (C : Graph  {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
+      {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → A ≡ X
+eq-vertex1 _ (mrefl refl) = refl
+
+eq-vertex2 : {c₁ c₂ : Level} (C : Graph  {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
+      {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → B ≡ Y
+eq-vertex2 _ (mrefl refl) = refl
+
+eq-edge : {c₁ c₂ : Level} (C : Graph  {c₁} {c₂}) {A B : vertex C} {f : edge C A B}
+      {X Y : vertex C} → {g : edge C X Y } → ( [ C ] f == g ) → f ≅ g
+eq-edge C eq with eq-vertex1 C eq | eq-vertex2 C eq
+eq-edge C (mrefl refl) | refl | refl = refl
+
 _=m=_ : {c₁ c₂ c₁' c₂'  : Level} {C : Graph {c₁} {c₂} } {D : Graph {c₁'} {c₂'} }
     → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂')
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
@@ -369,7 +382,14 @@
   isFunctor UX  = isf where
     isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap
     eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f
-    eff a f = {!!}
+    eff a f with giso→ {fobj a} {_} {_} {id1 (cat a) (vmap (m12 (fobj a)) f )} (id1 (cat a) (vmap (m12 (fobj a)) f )) 
+    ... | tt = subst₂ (λ j k → edge (g21 (fobj a)) j k ) {!!} {!!} m  where
+         fuga : ? ≡ ?
+         fuga = eq-vertex1 (fobj a) tt
+         hoge : vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f) ≡ f
+         hoge = eq-vertex1 (g21 (fobj a)) {!!}
+         m :  edge (g21 (fobj a)) (vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f )) (vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f ))
+         m  = emap (m21 (fobj a)) (id1 (cat a) _)
     IsFunctor.identity isf {a} {b} {f} = begin
          fmap (id1 Cart a) 
        ≈⟨⟩
@@ -416,7 +436,6 @@
        open forgetful  
        open ccc-from-graph
        -- 
-       --  In our scheme, CAT/Cart/Grph does not allow different levels of objects, so we assume level conversion on Graph
        -- 
        --                                        η : Hom Grph a (FObj UX (F a))
        --                    f : edge g x y   ----------------------------------->  m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
@@ -443,7 +462,7 @@
        pl : {c₁ c₂ : Level}  → (g : Graph {c₁} {c₂} ) → Category _ _ _
        pl g = PL g
        cobj  :  {g : Obj (Grph {c₁} {c₂} ) } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
-       cobj {g} {c} f (atom x) = {!!} -- vmap f x
+       cobj {g} {c} f (atom x) = {!!}
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
        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) 
@@ -456,15 +475,29 @@
        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 {!!}) (c-map f {!!})
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
+       SG : (g : Graph {c₁} {c₂}) → Functor (Sets {c₁ ⊔ c₂}) (ccc-from-graph.PL g)
+       SG g = record {
+                FObj = λ x → ccc-from-graph.atom {!!}  ;
+                FMap = λ f → ccc-from-graph.iv ( ccc-from-graph.arrow {!!}) (ccc-from-graph.id _) ;
+                isFunctor = record {
+                     identity = {!!} ;
+                     distr = {!!} ;
+                     ≈-cong = {!!} 
+                  }
+            }
        solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c
        solution  {g} {c} f = record { cmap = record {
              FObj = λ x → cobj {g} {c} f (xtog x) ;
              FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h )  ;
              isFunctor = {!!} } ;
              ccf = {!!} } where
+                mp : GMap (FObj UX c) (forgetful.fobj c)
+                mp = record { vmap = {!!} ; emap = {!!} }
+                mm : Hom Grph g (forgetful.fobj c)
+                mm = mp & f
                 xtog : Obj Sets → Objs g
                 xtog x = {!!}
-                htop : {x y : Set (c₁ ⊔ c₂) } → (x → y) →  Hom (pl g) {!!} {!!}
+                htop : {x y : Set (c₁ ⊔ c₂) } → (x → y) →  Hom (pl g) (xtog x) (xtog y)
                 htop = {!!}
                 fo : Graph  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}
                 fo = forgetful.fobj {c₁} {c₂} c