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

diff -r 5084433e0726 -r 3f2525c2b999 CCCGraph.agda
--- a/CCCGraph.agda	Sun May 17 11:55:30 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 12:35:49 2020 +0900
@@ -397,14 +397,14 @@
        ≈⟨⟩
          ( 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) ) )
        ≈⟨ {!!} ⟩
-         ( 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) )))))
-       ≈⟨⟩
+--         ( 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 
     IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 (
@@ -460,50 +460,13 @@
             em {x} {y} f = emap (m21 fo) (ccc-from-graph.fmap a (iv (arrow f) (id _)))
        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) = {!!}
-       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) 
-       c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs g} 
-           → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       c-map {g} {c} {atom a} {atom x} f y = {!!}
-       c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!}
-       c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!}
-       c-map {g} {c} {b <= a} {atom x} f y = {!!}
-       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 = {!!} 
-                  }
-            }
-       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 ) ;
-             FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h )  ;
+             FObj = λ x → cobj x ;
+             FMap = λ {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 : (x : Obj Sets) → Objs g
-                xtog x = ccc-from-graph.atom {!!}
-                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
-
+                  fvmap :  vertex g → vertex (g21 (forgetful.fobj c))
+                  fvmap = vmap f
+                  cobj : Obj Sets → Obj (cat c)
+                  cobj = {!!}