# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556714103 -32400
# Node ID f57c9603d9895cce3da324ee5e8c4845d756a38a
# Parent  4c0580d9dda4ea7cec612c37048ed7a34661ce35
add ≈-to-≡ assumption

diff -r 4c0580d9dda4 -r f57c9603d989 CCCGraph.agda
--- a/CCCGraph.agda	Wed May 01 21:16:58 2019 +0900
+++ b/CCCGraph.agda	Wed May 01 21:35:03 2019 +0900
@@ -350,10 +350,11 @@
           ∎  )
   
 
-UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
-FObj (UX {c₁} {c₂} {ℓ}) a = fobj a
-FMap UX f =  fmap f
-isFunctor (UX {c₁} {c₂} {ℓ}) = isf where
+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₂} {ℓ} ) (Grp {c₁} {c₂})
+FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
+FMap (UX ≈-to-≡)  f =  fmap f
+isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
   open import HomReasoning
   lemma0 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a b : Obj B} → [_]_~_ B  (id1 B a) (id1 B b) → a ≡ b 
   lemma0 {A} {B} {f} {g} (refl eqv) = refl
@@ -365,12 +366,12 @@
        → (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ] → vmap (fmap f) ≡ vmap (fmap g)
   lemma1 {a} {b} {f} {g} eq = extensionality Sets ( λ z → lemma01 {cat a} {cat b} {cmap f} {cmap g} eq  )
   lemma20 : {A B : Category c₁ c₂ ℓ }  {a b : Obj A} → ( e : Hom A a b ) → ( g : Functor A B )  → ( f : Hom A a b → Hom B (FObj g a) (FObj g b) ) 
-       → B [ f e ≈ FMap g e ] → f e ≅ FMap g e
-  lemma20 e g f eq = {!!}
+       → B [ f e ≈ FMap g e ] → f e  ≡ FMap g e
+  lemma20 {_} {B} e g f eq = ≈-to-≡ B eq
   lemma2 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B} →
       (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ]  → vmap (fmap f) ≡ vmap (fmap g)  → {a b : vertex (fobj A)} {e : edge (fobj A) a b} → emap (fmap f) e ≅ emap (fmap g) e
   lemma2 {A} {B} {f} {g} eq refl {a} {b} {e} with ( eq e )
-  ... | refl {h} eqv =  lemma20 e (cmap g) (FMap (cmap f)) eqv
+  ... | refl {h} eqv = Relation.Binary.HeterogeneousEquality.≡-to-≅ ( lemma20 e (cmap g) (FMap (cmap f)) eqv )
   isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
   IsFunctor.identity isf = mrefl refl refl
   IsFunctor.distr isf = mrefl refl refl