# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557358467 -32400
# Node ID d1569e80fe0bd0e306a63140853beda22f729b9f
# Parent  8f41ad966eaaedc9683d1d9d919d623c769efb24
fix comment

diff -r 8f41ad966eaa -r d1569e80fe0b CCCGraph.agda
--- 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 } )
 ---   
 ---