# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556673405 -32400
# Node ID 658daaa74df340a8966b5312be4f38cff890d416
# Parent  b27b231c2d5465cb3aa46e268d68f18100110c56
...

diff -r b27b231c2d54 -r 658daaa74df3 CCCGraph.agda
--- a/CCCGraph.agda	Sun Apr 28 16:03:42 2019 +0900
+++ b/CCCGraph.agda	Wed May 01 10:16:45 2019 +0900
@@ -240,44 +240,64 @@
 record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
      cmap : Functor (cat A ) (cat B )
-     ccf : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
+     ccf :  CCC (cat A) → CCC (cat B)
+
+open import Category.Cat
+
+open  CCCMap
+open import Relation.Binary.Core
 
----   
----   Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
----   Cart {c₁} {c₂} {ℓ} = record {
----       Obj = CCCObj {c₁} {c₂} {ℓ}
----     ; Hom = CCCMap
----     ; _o_ = {!!}
----     ; _≈_ = {!!}
----     ; Id  = {!!}
----     ; isCategory = record {
----          identityL = {!!}
----        ; identityR = {!!}
----        ; o-resp-≈ = {!!}
----        ; associative = {!!}
----      }}
+Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
+Cart {c₁} {c₂} {ℓ} = record {
+    Obj = CCCObj {c₁} {c₂} {ℓ}
+  ; Hom = CCCMap
+  ; _o_ = _・_
+  ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
+  ; Id  = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x }
+  ; isCategory = record {
+     isEquivalence = λ {A} {B} → record {
+          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
+   }} 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 : Level} (x y : Graph {v} ) : Set (suc v) where
+record GMap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+  field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
 
----   Grp : {v : Level} → Category (suc v) v v
----   Grp {v} = record {
----       Obj = Graph {v} 
----     ; Hom = {!!}
----     ; _o_ = {!!}
----     ; _≈_ = {!!}
----     ; Id  = {!!}
----     ; isCategory = record {
----          identityL = {!!}
----        ; identityR = {!!}
----        ; o-resp-≈ = {!!}
----        ; associative = {!!}
----      }}
----   
+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 → {!!}
+  ; Id  = record { vmap = λ y → y ; emap = λ f → f }
+  ; isCategory = record {
+       identityL = {!!}
+     ; identityR = {!!}
+     ; o-resp-≈ = {!!}
+     ; associative = {!!}
+   }}
+
 ---   UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁})
 ---   UX = {!!}
 ---