--- a/src/CCCGraph.agda	Sat Mar 06 11:42:01 2021 +0900
+++ b/src/CCCGraph.agda	Sat Mar 06 13:35:45 2021 +0900
@@ -359,7 +359,7 @@
 
 module forgetful {c₁ : Level} where
 
-  ≃-cong : {c₁ c₁ ℓ : Level}  (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
+  ≃-cong : {c₁ ℓ : Level}  (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
       → { f f'   : Hom B a b }
       → { g g' : Hom B a' b' }
       → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
@@ -373,6 +373,18 @@
              g'
           ∎  )
 
+  ≃→a=a : {c₁ ℓ : Level}  (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
+      → ( f : Hom B a b )
+      → ( g : Hom B a' b' )
+      → [_]_~_ B f g → a ≡ a'
+  ≃→a=a B f g (refl eqv) = refl
+
+  ≃→b=b : {c₁ ℓ : Level}  (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B }
+      → ( f : Hom B a b )
+      → ( g : Hom B a' b' )
+      → [_]_~_ B f g → b ≡ b'
+  ≃→b=b B f g (refl eqv) = refl
+
   -- Grph does not allow morph on different level graphs
   -- simply assumes c₁ and c₂ has the same
   
@@ -398,22 +410,18 @@
          id1 Grph ((uobj a))
        ∎ where open ≈-Reasoning Grph 
     IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
-         umap ( Cart [ g o f ] )
-       ≈⟨⟩
-         record { vmap = {!!} ; emap = {!!} }
-       ≈⟨ {!!} ⟩
-         record { vmap = {!!} ; emap = {!!} }
-       ≈⟨⟩
+         umap ( Cart [ g o f ] )  -- FMap (cmap g) (FMap (cmap f) x)   = FMap (cmap g) (FMap (cmap f) x)
+       ≈⟨ (λ x → mrefl refl ) ⟩
          Grph [ umap g o umap f ]
-       ∎ where open ≈-Reasoning Grph 
-    IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 (
-          --       ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
-          --  )))) (f=g e) where
-      lemma4 : {x y : vertex (uobj b)} →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
-      lemma4 (refl eqv) = refl 
-      -- lemma : vmap (umap f) ≡ vmap (umap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ g21 (uobj b)] emap (umap f) {!!} == emap (umap g) {!!}
-      -- lemma = {!!} -- refl (refl eqv) = mrefl (≡←≈ b eqv)
-
+       ∎ where open ≈-Reasoning Grph  --  FMap (cmap f) e emap (umap f) e =  emap (umap g) e  <-  Cart [ f ≈ g ]
+    IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e with
+           f=g e
+         | ≃→a=a (cat b) (FMap (cmap f) e) (FMap (cmap g) e) (f=g e)
+         | ≃→b=b (cat b) (FMap (cmap f) e) (FMap (cmap g) e) (f=g e)
+    ... | eq | eqa | eqb =  cc11 (FMap (cmap f) e) (FMap (cmap g) e) eq eqa eqb where
+           cc11 : {a c a' c' : Obj (cat b) } → ( f : Hom (cat b) a c ) → ( g : Hom (cat b) a' c' )
+               → [ cat b ] f ~ g → a ≡ a'  → c  ≡ c'  →  [ uobj b ] f == g 
+           cc11 f g (refl eqv) refl refl =  mrefl (≡←≈ b eqv) 
 
 open ccc-from-graph.Objs
 open ccc-from-graph.Arrow
@@ -439,7 +447,7 @@
                     identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
                     identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
                     o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
-                    associative  = {!!} -- IsCategory.associative (Category.isCategory B) 
+                    associative  = λ {a} {b} {c} {f} {g} {h} → ? -- IsCategory.associative (Category.isCategory B) {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} {{!!}}
              }
           } ;
          ≡←≈  = λ eq → eq ;