### changeset 818:bc244fc604c8

...
author Shinji KONO Sun, 28 Apr 2019 13:02:36 +0900 177162990879 b27b231c2d54 CCCGraph.agda 1 files changed, 29 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
```--- a/CCCGraph.agda	Sun Apr 28 12:37:34 2019 +0900
+++ b/CCCGraph.agda	Sun Apr 28 13:02:36 2019 +0900
@@ -172,17 +172,27 @@
IsFunctor.≈-cong isf refl = refl
IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )

----   record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
----     field
----       cat : Category c₁ c₂ ℓ
----       ccc : CCC cat
----
----   open CCCObj
----
----   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)
+---
+---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap
+---
+---     CCC ( SC (CS G)) Sets   have to be proved
+---  SM can be eliminated if we have
+---    sobj (a : vertex g ) → {a}              a set have only a
+---    smap (a b : vertex g ) → {a} → {b}
+
+
+record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+   field
+     cat : Category c₁ c₂ ℓ
+     ccc : CCC cat
+
+open CCCObj
+
+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)
+
---
---   Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
---   Cart {c₁} {c₂} {ℓ} = record {
@@ -197,14 +207,14 @@
---        ; o-resp-≈ = {!!}
---        ; associative = {!!}
---      }}
----
----   open import discrete
----   open Graph
----
----   record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
----      vmap : vertex x → vertex y
----      emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
----
+
+open import discrete
+open Graph
+
+record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+   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} ```