# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556691414 -32400
# Node ID fbbc9c03bfed9d431b20c491e9e44a194a22d273
# Parent  658daaa74df340a8966b5312be4f38cff890d416
Grp and Cart

diff -r 658daaa74df3 -r fbbc9c03bfed CCCGraph.agda
--- a/CCCGraph.agda	Wed May 01 10:16:45 2019 +0900
+++ b/CCCGraph.agda	Wed May 01 15:16:54 2019 +0900
@@ -102,7 +102,7 @@
 
    open Graph
 
-   data Objs (G : Graph ) : Set where    -- formula
+   data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where    -- formula
       atom : (vertex G) → Objs G
       ⊤ : Objs G
       _∧_ : Objs G → Objs G → Objs G
@@ -168,7 +168,7 @@
 
    record SM {v : Level} : Set (suc v)  where
       field
-        graph : Graph  {v}
+        graph : Graph  {v} {v}
         sobj : vertex graph → Set
         smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
 
@@ -259,10 +259,10 @@
           refl = λ {f} →  let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} 
         ; sym = λ {f} {g}  → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} 
         ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h}  }
-     ; identityL = let open ≈-Reasoning (CAT) in idL {_} {_} {_} {_} {_}
-     ; identityR = let open ≈-Reasoning (CAT) in idR
-     ; o-resp-≈ = IsCategory.o-resp-≈ ( Category.isCategory CAT) 
-     ; associative = let open ≈-Reasoning (CAT) in assoc
+     ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_}
+     ; 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 ))
@@ -277,29 +277,73 @@
 open import discrete
 open Graph
 
-record GMap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc v ⊔ v'  ) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
 
 open GMap
 
-Grp : {v : Level} → Category (suc v) (suc v) v
-Grp {v} = record {
-    Obj = Graph {v} 
-  ; Hom = GMap {v}
-  ; _o_ = λ f g → record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
-  ; _≈_ = λ {a} {b} f g → {!!}
+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
+
+_&_ :  {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'} = record {
+    Obj = Graph {v} {v'}
+  ; Hom = GMap {v} {v'}
+  ; _o_ = _&_
+  ; _≈_ = _=m=_
   ; Id  = record { vmap = λ y → y ; emap = λ f → f }
   ; isCategory = record {
-       identityL = {!!}
-     ; identityR = {!!}
-     ; o-resp-≈ = {!!}
-     ; associative = {!!}
-   }}
+       isEquivalence = λ {A} {B} →  ise {v} {v'} {A} {B} 
+     ; identityL = mrefl refl refl
+     ; identityR =  mrefl refl refl
+     ; o-resp-≈ = m--resp-≈ 
+     ; associative = mrefl refl 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} )
+       ise  = record {
+          refl =  λ {x} → mrefl refl 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
 
----   UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁})
----   UX = {!!}
+--- 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) }
+
+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
+  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 eq = mrefl {!!} {!!}
+
 ---   
 ---   open ccc-from-graph
 ---   
diff -r 658daaa74df3 -r fbbc9c03bfed discrete.agda
--- a/discrete.agda	Wed May 01 10:16:45 2019 +0900
+++ b/discrete.agda	Wed May 01 15:16:54 2019 +0900
@@ -6,24 +6,24 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
-record Graph  { v : Level } : Set (suc v) where
+record Graph  { v v' : Level } : Set (suc v ⊔ suc v' ) where
   field
     vertex : Set v
-    edge : vertex  → vertex → Set v
+    edge : vertex  → vertex → Set v'
 
 module graphtocat where
 
   open import Relation.Binary.PropositionalEquality 
 
-  data Chain { v : Level } ( g : Graph {v} ) : ( a b : Graph.vertex g ) → Set v where
+  data Chain { v v' : Level } ( g : Graph {v} {v'} ) : ( a b : Graph.vertex g ) → Set (v ⊔ v' ) where
        id : ( a : Graph.vertex g ) → Chain g a a
        next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain g a b → Chain g a c
 
-  _・_ :  {v : Level} { G : Graph {v} } {a b c : Graph.vertex G } (f : Chain G b c ) → (g : Chain G a b) → Chain G a c
+  _・_ :  {v v' : Level} { G : Graph {v} {v'} } {a b c : Graph.vertex G } (f : Chain G b c ) → (g : Chain G a b) → Chain G a c
   id _ ・ f = f
   (next x f) ・ g = next x ( f ・ g )
 
-  GraphtoCat : {v : Level} (G : Graph {v} )  →  Category  v v v
+  GraphtoCat : {v v' : Level} (G : Graph {v} {v'} )  →  Category  v (v ⊔ v') (v ⊔ v')
   GraphtoCat G = record {
             Obj  = Graph.vertex G ;
             Hom = λ a b →  Chain G a b ;