# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589684130 -32400
# Node ID 5084433e07267f70759f74f5100574cd7e761da6
# Parent  d26f21112e1c82c09c365ee2317891d43e931e53
...

diff -r d26f21112e1c -r 5084433e0726 CCCGraph.agda
--- a/CCCGraph.agda	Sun May 17 10:32:22 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 11:55:30 2020 +0900
@@ -364,9 +364,9 @@
      m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} )  → GMap  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g)
      m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} )  → GMap  {c₁} {c₂}  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g
      giso→  : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
-          → {a b : vertex g } → {e : edge g a b } →  (m12 g & m21 g) =m= id1 Grph g
+          → {a b : vertex g } →  (m12 g & m21 g) =m= id1 Grph g
      giso←  : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
-          → {a b : vertex (g21 g) } → {e : edge (g21 g) a b } →  (m21 g & m12 g ) =m= id1 Grph (g21 g)
+          → {a b : vertex (g21 g) } →  (m21 g & m12 g ) =m= id1 Grph (g21 g)
                 -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ]
   
   fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph
@@ -381,15 +381,13 @@
   FMap UX f =  fmap f
   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 = {!!}
     IsFunctor.identity isf {a} {b} {f} = begin
          fmap (id1 Cart a) 
        ≈⟨⟩
          fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x })
        ≈⟨⟩
          record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )}
-       ≈⟨ giso← {fobj a} {f} {f} {eff a f } ⟩
+       ≈⟨ giso← {fobj a} {f} {f}  ⟩
          record { vmap = λ y → y ; emap = λ f → f }
        ≈⟨⟩
          id1 Grph (g21 (fobj a))
@@ -397,11 +395,15 @@
     IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
          fmap ( Cart [ g o f ] )
        ≈⟨⟩
-         record { vmap = λ e →  vmap (m21 (fobj c)) (FObj (cmap (Cart [ g o f ] )) (vmap (m12 (fobj a)) e)) ;
-                  emap = λ e →  emap (m21 (fobj c)) (FMap (cmap (Cart [ g o f ] )) (emap (m12 (fobj a)) e)) } 
+         ( m21 (fobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} &  m12 (fobj a) ) )
        ≈⟨ {!!} ⟩
-         record { vmap = λ e →  vmap (m21 (fobj c)) (FObj (cmap g) (vmap (m12 (fobj b)) (vmap (fmap f) e)));
-                  emap = λ e →  emap (m21 (fobj c)) (FMap (cmap g) (emap (m12 (fobj b)) (emap (fmap f) e))) } 
+         ( m21 (fobj c) &  (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e)  ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) }
+            &  m12 (fobj a)))
+       ≈⟨ cdr (cdr (car (giso← {fobj b} )))  ⟩
+         ( m21 (fobj c) &  (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e}
+            &  ((m12 (fobj b) 
+            &  (m21 (fobj b))) &  (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e}
+            &  (m12 (fobj a) )))))
        ≈⟨⟩
          Grph [ fmap g o fmap f ]
        ∎ where open ≈-Reasoning Grph 
@@ -446,8 +448,6 @@
        --                          ↓                                                       |
        --  Sets  ((z : vertx g) → C z x)  ----> ((z : vertx g) → C z y)  = h : Hom Sets (fobj (atom x)) (fobj (atom y))
        --
-       cs : {c₁ c₂ : Level}  → (g : Graph  {c₁} {c₂} ) → Functor  (ccc-from-graph.PL g) (Sets {_})
-       cs g = CS g
        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))
@@ -484,6 +484,12 @@
                      ≈-cong = {!!} 
                   }
             }
+       submap : (g : Graph {c₁} {c₂}) → Functor (Sets  {c₁ ⊔ c₂} )(Sets  {c₁ ⊔ c₂} )
+       submap g = record {
+             FObj = λ x → Objs {!!} ;
+             FMap = λ {x} {y} h → {!!} ;
+             isFunctor = {!!}
+          }
        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 ) ;