# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556765649 -32400
# Node ID 878d8643214fbb3e8397acb0c22c45b0dd3cb110
# Parent  f57c9603d9895cce3da324ee5e8c4845d756a38a
...

diff -r f57c9603d989 -r 878d8643214f CCCGraph.agda
--- a/CCCGraph.agda	Wed May 01 21:35:03 2019 +0900
+++ b/CCCGraph.agda	Thu May 02 11:54:09 2019 +0900
@@ -251,7 +251,7 @@
 Cart {c₁} {c₂} {ℓ} = record {
     Obj = CCCObj {c₁} {c₂} {ℓ}
   ; Hom = CCCMap
-  ; _o_ = _・_
+  ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) }
   ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
   ; Id  = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x }
   ; isCategory = record {
@@ -263,21 +263,12 @@
      ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f}
      ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i}  → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i}
      ; associative =  λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h}
-   }} where
-      cart-refl : {A B : CCCObj {c₁} {c₂} {ℓ} } → { x : CCCMap A B } → {a b : Obj ( cat A ) } → (f : Hom ( cat A ) a b)  →  [ cat B ] FMap (cmap x) f ~ FMap (cmap x) f
-      cart-refl {A} {B} {x} {a} {b} f = [_]_~_.refl  ( IsFunctor.≈-cong (isFunctor ( cmap x ))
-            (  IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory ( cat A  )))))
-      _・_ : { A B C : CCCObj {c₁} {c₂} {ℓ} } → ( f : CCCMap B C  ) → ( g : CCCMap A B  ) → CCCMap A C  
-      _・_ {A} {B} {C} f g = record { cmap = F ; ccf = ccmap }  where
-         F : Functor (cat A) (cat C)
-         F = (cmap f) ○ ( cmap g )
-         ccmap :  CCC (cat A) → CCC (cat C)
-         ccmap ca = ccf f ( ccf g (ccc A ))
+   }} 
 
 open import discrete
 open Graph
 
-record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc v ⊔ v'  ) where
+record GMap {v v' w w' : Level} (x : Graph {v} {v'} ) (y : Graph {w} {w'} ) : Set (suc (v ⊔ w) ⊔  v' ⊔ w' ) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -286,13 +277,18 @@
 
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
 
-data _=m=_ {v v' : Level} {x y : Graph {v} {v'}} ( f g : GMap x y ) :  Set (v ⊔ v'  ) where
-     mrefl : ( vmap f ≡ vmap g ) → ( {a b : vertex x} → { e : edge x a b } → emap f e  ≅ emap g e ) → f =m= g
+data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B)
+     : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where
+  mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
+
+_=m=_ : ∀ {c₁ c₂ } {C D : Graph {c₁} {c₂} } 
+    → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁))
+_=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 
 _&_ :  {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
 f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
 
-Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (v ⊔ v')
+Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (suc ( v ⊔ v'))
 Grp {v} {v'} = record {
     Obj = Graph {v} {v'}
   ; Hom = GMap {v} {v'}
@@ -300,41 +296,36 @@
   ; _≈_ = _=m=_
   ; Id  = record { vmap = λ y → y ; emap = λ f → f }
   ; isCategory = record {
-       isEquivalence = λ {A} {B} →  ise {v} {v'} {A} {B} 
-     ; identityL = mrefl refl refl
-     ; identityR =  mrefl refl refl
+       isEquivalence = λ {A} {B} →  ise 
+     ; identityL = λ e → mrefl refl
+     ; identityR =  λ e → mrefl refl
      ; o-resp-≈ = m--resp-≈ 
-     ; associative = mrefl refl refl
+     ; associative = λ e → mrefl refl
    }}  where
-       msym : {v v' : Level} {x y : Graph {v} {v'} } { f g : GMap x y } → f =m= g → g =m= f
-       msym (mrefl refl eq ) = mrefl refl ( ≅-sym eq ) 
-       mtrans : {v v' : Level} {x y : Graph {v} {v'}} { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
-       mtrans (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( ≅-trans eq eq1 ) 
-       ise : {v v' : Level} {x y : Graph {v} {v'}} → IsEquivalence {_} {v ⊔ v'} {_} ( _=m=_ {v} {v'} {x} {y} )
+       msym : {v v' : Level} {x y : Graph {v} {v'} }  { f g : GMap x y } → f =m= g → g =m= f
+       msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where
+            lemma  : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
+            lemma (mrefl Ff≈Gf) = mrefl  (sym  Ff≈Gf)
+       mtrans : {v v' : Level} {x y : Graph {v} {v'} }  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
+       mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
+           lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f}  → [ y ] p == q → [ y ] q == r → [ y ] p == r
+           lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv  eqv₁ )
+       ise : {v v' : Level} {x y : Graph {v} {v'}}  → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_  {v} {v'}  {x} {y}) 
        ise  = record {
-          refl =  λ {x} → mrefl refl refl
+          refl =  λ f → mrefl refl
         ; sym = msym
         ; trans = mtrans
           }
-       m--resp-≈ : {v : Level} {A B C : Graph {v} } {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
-       m--resp-≈ {_} {_} {_} {_} {f} {g} {h} {i}  (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( λ {a} {b} {e} →  begin
-                  emap h (emap f e)
-               ≅⟨ ≅-cong ( λ k → emap h k ) eq  ⟩
-                  emap h (emap g e)
-               ≅⟨ eq1  ⟩
-                  emap i (emap g e)
-               ∎  )
-               where open Relation.Binary.HeterogeneousEquality.≅-Reasoning 
-       assoc-≈ : {v v' : Level} {A B C D : Graph {v} {v'} } {f : GMap C D} {g : GMap B C} {h : GMap A B} → ( f & ( g & h ) ) =m= ( (f & g ) & h )
-       assoc-≈ = mrefl refl refl
+       m--resp-≈ : {v v' : Level} {A B C : Graph {v} {v'} }  
+           {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
+       m--resp-≈ {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
+          lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
+            lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
+                [ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
+            lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl
 
 --- Forgetful functor
 
-fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grp {c₁} {c₂})
-fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
-fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
-
 ≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
       → { f f'   : Hom B a b }
       → { g g' : Hom B a' b' }
@@ -349,33 +340,29 @@
              g'
           ∎  )
   
+fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grp {c₁} {c₂})
+fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
+fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
+fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (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₂} {ℓ} ) (Grp {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
-  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
-  lemma03 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → [_]_~_ B  (FMap f ( id1 A a)) (FMap g ( id1 A a)) → FObj f a ≡ FObj g a 
-  lemma03 {A} {B} {f} {g} eq = lemma0 {A} {B} {f} {g} ( ≃-cong B eq (IsFunctor.identity (Functor.isFunctor (f)))(IsFunctor.identity (Functor.isFunctor (g)))  )
-  lemma01 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → f ≃ g  →  FObj f a ≡ FObj g a 
-  lemma01 {A} {B} {f} {g} {a}  eq = lemma03 {A} {B} {f} {g} (eq (id1 A a))
-  lemma1 : {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)
-  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 {_} {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 = 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
-  IsFunctor.≈-cong isf {a} {b} {f} {g} eq = mrefl (lemma1 {a} {b} {f} {g} eq ) (lemma2 {a} {b} {f} {g} eq (lemma1 {a} {b} {f} {g} eq ))
+  IsFunctor.identity isf {a} {b} {f} e = mrefl refl 
+  IsFunctor.distr isf f = mrefl refl
+  IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = 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 ( ≈-to-≡ (cat b) eqv )
+
 
 ---   
 ---   open ccc-from-graph