# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588127072 -32400
# Node ID 9652159bda4bad179b8d2db21e0075ffda9e4076
# Parent  eaf90711a6fd2d6deef433df6988c10bbd956fb2
CCC to Graph forgetful functor

diff -r eaf90711a6fd -r 9652159bda4b CCCGraph.agda
--- a/CCCGraph.agda	Wed Apr 29 04:07:44 2020 +0900
+++ b/CCCGraph.agda	Wed Apr 29 11:24:32 2020 +0900
@@ -398,26 +398,16 @@
 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
 fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) ; econg = IsFunctor.≈-cong (Functor.isFunctor (cmap f))  }
 
-UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
-    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
-FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
-FMap (UX ≈-to-≡)  f =  fmap f
-isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
-  -- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
-  open import HomReasoning
-  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
+UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
+FObj UX a = fobj a
+FMap UX f =  fmap f
+isFunctor UX  = isf where
+  isf : IsFunctor Cart Grph 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} 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