### changeset 826:d1569e80fe0bgraph-to-ccc

fix comment
author Shinji KONO Thu, 09 May 2019 08:34:27 +0900 8f41ad966eaa 054eecbb5189 CCCGraph.agda 1 files changed, 24 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
```--- a/CCCGraph.agda	Fri May 03 17:11:33 2019 +0900
+++ b/CCCGraph.agda	Thu May 09 08:34:27 2019 +0900
@@ -17,7 +17,9 @@

open import Category.Sets

+------------------------------------------------------
-- Sets is a CCC
+------------------------------------------------------

postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

@@ -96,6 +98,10 @@

module ccc-from-graph where

+------------------------------------------------------
+--  CCC generated from a graph
+------------------------------------------------------
+
open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
open import graph
open graphtocat
@@ -132,40 +138,6 @@
iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x )
iso-right (elm x) = elmeq

---   record one {v : Level} {S : Set v} : Set (suc v) where
---      field
---         elm : S
---
---   iso→ : {v : Level} {S : Set v} → one {v} {S} → One {Level.zero} → S
---   iso→ x OneObj = one.elm x
---   iso← : {v : Level} {S : Set v} → one {v} {S} → S → One {Level.zero}
---   iso← x y = OneObj
---
---   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso→ x ( iso← x a ) ≡ a
---   iso-left x a =  {!!}
---
---   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x OneObj ) ≡ OneObj
---   iso-right x =  refl
-
-   record one' {v : Level} {S : Set v} : Set (suc v) where
-     field
-        elm' : S
-        iso→' : One {Level.zero} → S
-        iso←' : S → One {Level.zero}
-        iso-left' : iso→' ( iso←' elm' ) ≡ elm'
-        iso-right' : iso←' ( iso→' OneObj ) ≡ OneObj
-
-   tmp : {v : Level} {S : Set v} → one {v} {S}  → one' {v} {S}
-   tmp x = record {
-         elm' = iso→ x
-       ; iso→' = λ _ → iso→ x
-       ; iso←' = λ _ → OneObj
-       ; iso-left' = refl
-       ; iso-right' = refl
-     }
-
-
-
record SM {v : Level} : Set (suc v)  where
field
graph : Graph  {v} {v}
@@ -221,6 +193,10 @@
IsFunctor.≈-cong isf refl = refl
IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )

+------------------------------------------------------
+--  Cart     Category of CCC and CCC preserving Functor
+------------------------------------------------------
+
---
---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap
---
@@ -265,6 +241,10 @@
; 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}
}}

+------------------------------------------------------
+--  Grph     Category of Graph and Graph mapping
+------------------------------------------------------
+
open import graph
open Graph

@@ -288,8 +268,8 @@
_&_ :  {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') (suc ( v ⊔ v'))
-Grp {v} {v'} = record {
+Grph : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (suc ( v ⊔ v'))
+Grph {v} {v'} = record {
Obj = Graph {v} {v'}
; Hom = GMap {v} {v'}
; _o_ = _&_
@@ -324,7 +304,9 @@
[ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl

---- Forgetful functor
+------------------------------------------------------
+--- CCC → Grph  Forgetful functor
+------------------------------------------------------

≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
→ { f f'   : Hom B a b }
@@ -340,19 +322,19 @@
g'
∎  )

-fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grp {c₁} {c₂})
+fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {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 : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {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₂})
+    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {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
-  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
+  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
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 (
@@ -372,7 +354,7 @@
---   SM.sobj (sm  g) = {!!}
---   SM.smap (sm  g) = {!!}
---
----   HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v})
+---   HX : {v : Level } ( x : Obj (Grph {v}) ) → Obj (Grph {v})
---   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
---
---   ```