# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588100864 -32400
# Node ID eaf90711a6fd2d6deef433df6988c10bbd956fb2
# Parent  e20853d2c6b0f3f34908478e30b7fa8533ccf32e
Forgetful  functor from CCC to Graph done

diff -r e20853d2c6b0 -r eaf90711a6fd CCCGraph.agda
--- a/CCCGraph.agda	Wed Apr 29 03:01:05 2020 +0900
+++ b/CCCGraph.agda	Wed Apr 29 04:07:44 2020 +0900
@@ -408,18 +408,20 @@
   isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
   IsFunctor.identity isf {a} {b} {f} e = mrefl (erefl (fobj a))
   IsFunctor.distr isf {a} {b} {c} f = mrefl (erefl (fobj c))
-  IsFunctor.≈-cong isf {a} {b} {f} {g} eq1 {A} {B} e with eq1 {A} {B} e | FMap (cmap f) e | FMap (cmap g) e | inspect eq1 e
-  ... | t | x | y | record { eq = ee } = lemma  x y {!!} where
-      lemma : ( x : Hom (cat b)  (FObj (cmap f) A)  (FObj (cmap f) B) ) ( y : Hom (cat b)  (FObj (cmap g) A)  (FObj (cmap g) B) ) → 
-         [ cat b ] x ~ y → [ fobj b ] x == y
-      lemma x y t2 = {!!}
+  IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = 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
+    -- ... | t | x | y | record { eq = ee } = lemma  x y {!!} where
+    --   lemma : ( x : Hom (cat b)  (FObj (cmap f) A)  (FObj (cmap f) B) ) ( y : Hom (cat b)  (FObj (cmap g) A)  (FObj (cmap g) B) ) → 
+    --     [ cat b ] x ~ y → [ fobj b ] x == y
+    --  lemma x y t2 = {!!}
     --   lemma (extensionality Sets ( λ z → lemma4 (
     --           ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
     --      ))) (eq e) where
-    --  lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
-    --  lemma4 (refl eqv) = refl 
-    --  lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
-    --  lemma refl (refl eqv) = mrefl {!!} -- (econg (fmap f ) ? ) -- ( ≈-to-≡ (cat b) eqv )
+    lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
+    lemma4 (refl eqv) = refl 
+    lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
+    lemma refl (refl eqv) = mrefl eqv