Mercurial > hg > Members > kono > Proof > category

changeset 897:5a074b2c7a46

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Apr 2020 23:11:12 +0900
parents 8146234fc326
children d1bd473b4efb
files CCCGraph.agda graph.agda
diffstat 2 files changed, 57 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon Apr 13 18:40:16 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 27 23:11:12 2020 +0900
@@ -103,7 +103,7 @@
 --
 
 open import graph
-module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
+module ccc-from-graph {c₁  c₂ ℓ : Level} (G : Graph {c₁} {c₂} {ℓ})  where
    open import  Relation.Binary.PropositionalEquality hiding ( [_] )
    open import  Relation.Binary.Core 
    open Graph
@@ -183,7 +183,7 @@
    tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
    tr f x y  = graphtocat.next f (x y) 
    
-   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂)
+   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
    fobj  (atom x) = ( y : vertex G ) → C y x
    fobj ⊤ = One
    fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
@@ -205,7 +205,7 @@
 --    Sets is CCC, so we have a cartesian closed category generated by a graph
 --       as a sub category of Sets
 
-   CS :  Functor PL (Sets {c₁ ⊔ c₂})
+   CS :  Functor PL (Sets {c₁ ⊔ c₂ ⊔ ℓ})
    FObj CS a  = fobj  a
    FMap CS {a} {b} f = fmap  {a} {b} f
    isFunctor CS = isf where
@@ -226,7 +226,7 @@
 
    open import subcat
 
-   CSC = FCat PL (Sets {c₁ ⊔ c₂}) CS
+   CSC = FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) CS
 
    cc1 : CCC CSC       -- SCS is CCC
    cc1 = record {
@@ -315,7 +315,7 @@
 open import graph
 open Graph
 
-record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (suc (v ⊔ 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)
@@ -324,20 +324,20 @@
 
 -- open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
 
-data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B)
+data [_]_==_ {c₁ c₂ ℓ} (C : Graph {c₁} {c₂} {ℓ}) {A B : vertex C} (f : edge C A B)
      : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where
   mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
 
-_=m=_ : ∀ {c₁ c₂ } {C D : Graph {c₁} {c₂} } 
+_=m=_ : ∀ {c₁ c₂ ℓ} {C D : Graph {c₁} {c₂} {ℓ}} 
     → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁))
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 
-_&_ :  {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
+_&_ :  {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 ) }
 
-Grph : {v v' : Level} → Category (suc (v ⊔ v')) (suc (v ⊔ v')) (suc ( v ⊔ v'))
-Grph {v} {v'} = record {
-    Obj = Graph {v} {v'}
+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_ = _&_
   ; _≈_ = _=m=_
@@ -349,23 +349,23 @@
      ; o-resp-≈ = m--resp-≈ 
      ; associative = λ e → mrefl refl
    }}  where
-       msym : {v v' : Level} {x y : Graph {v} {v'} }  { f g : GMap x y } → f =m= g → g =m= f
+       msym : {v v' : Level} {x y : Graph {v} {v'} {ℓ}}  { f g : GMap x y } → f =m= g → g =m= f
        msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where
             lemma  : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
             lemma (mrefl Ff≈Gf) = mrefl  (sym  Ff≈Gf)
-       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 : {v v' : Level} {x y : Graph {v} {v'} {ℓ}}  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
        mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
            lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f}  → [ y ] p == q → [ y ] q == r → [ y ] p == r
            lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv  eqv₁ )
-       ise : {v v' : Level} {x y : Graph {v} {v'}}  → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_  {v} {v'}  {x} {y}) 
+       ise : {v v' : Level} {x y : Graph {v} {v'}}  → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_  {v} {v'}  {ℓ} {x} {y}) 
        ise  = record {
           refl =  λ f → mrefl refl
         ; sym = msym
-        ; trans = mtrans
+        ; trans = {!!} -- mtrans
           }
-       m--resp-≈ : {v v' : Level} {A B C : Graph {v} {v'} }  
+       m--resp-≈ : {v v' ℓ : Level} {A B C : Graph {v} {v'}{ℓ} }  
            {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
-       m--resp-≈ {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
+       m--resp-≈ {_} {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
           lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
             lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
                 [ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
@@ -389,7 +389,7 @@
              g'
           ∎  )
   
-fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {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 (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
 fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
--- a/graph.agda	Mon Apr 13 18:40:16 2020 +0900
+++ b/graph.agda	Mon Apr 27 23:11:12 2020 +0900
@@ -6,32 +6,34 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
-record Graph  { v v' : Level } : Set (suc v ⊔ suc v' ) where
+record Graph  { v v' ℓ : Level } : Set (suc (v ⊔ v' ⊔ ℓ)) where
   field
     vertex : Set v
     edge : vertex  → vertex → Set v'
+    _≅_ : {A B : vertex} → Rel (edge A B) ℓ 
+    isEq : {A B : vertex} → IsEquivalence {v'} {ℓ} {edge A B} _≅_
 
 module graphtocat where
 
   open import Relation.Binary.PropositionalEquality 
 
-  data Chain { v v' : Level } ( g : Graph {v} {v'} ) : ( a b : Graph.vertex g ) → Set (v ⊔ 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 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
+  _・_ :  {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 v' : Level} (G : Graph {v} {v'} )  →  Category  v (v ⊔ v') (v ⊔ v')
-  GraphtoCat G = record {
+  GraphtoCat : {v v' ℓ : Level} (G : Graph {v} {v'} {ℓ} )  →  Category  v (v ⊔ v' ⊔ ℓ) (v ⊔ v' ⊔ ℓ)
+  GraphtoCat {v} {v'} {ℓ } G = record {
             Obj  = Graph.vertex G ;
             Hom = λ a b →  Chain G a b ;
             _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x  ≡ y ;
+            _≈_ =  λ x y → x == y ;
             Id  =  λ{a} → id a ;
             isCategory  = record {
-                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+                    isEquivalence =  record {refl = ==-refl ; trans = ==-trans ; sym = ==-sym } ;
                     identityL  = identityL; 
                     identityR  = identityR ; 
                     o-resp-≈  = o-resp-≈  ; 
@@ -41,19 +43,37 @@
                open Chain
                obj = Graph.vertex G
                hom = Graph.edge G
+               data _==_ : {a b : Graph.vertex G} → (x y : Chain G a b ) → Set (v ⊔ v' ⊔ ℓ) where
+                  ==-id : {a : Graph.vertex G }  → ( id a ) == (id a )
+                  ==-next : {a b c : Graph.vertex G } {x y : Graph.edge G b c } { f g : Chain G a b} → Graph._≅_ G x y  → f == g → next x f == next y g
 
-               identityL : {A B : Graph.vertex G} {f : Chain G A B} → (id B ・ f) ≡ f
-               identityL = refl
-               identityR : {A B : Graph.vertex G} {f : Chain G A B} → (f ・ id A) ≡ f
-               identityR {a} {_} {id a} = refl
-               identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
+               ==-refl :  {a b : Graph.vertex G} → {x  : Chain G a b } → x == x
+               ==-refl {_} {_} {id a} = ==-id
+               ==-refl {_} {_} {next x f} = ==-next (IsEquivalence.refl (Graph.isEq G)) (==-refl {_} {_} {f})
+
+               ==-sym :  {a b : Graph.vertex G} → {x y  : Chain G a b } → x == y → y == x
+               ==-sym  {a} {a} {id a} {id a} ==-refl = ==-refl
+               ==-sym (==-next x y=x) = ==-next (IsEquivalence.sym (Graph.isEq G) x) (==-sym y=x)
+
+               ==-trans :  {a b : Graph.vertex G} → {x y z : Chain G a b } → x == y → y == z → x == z
+               ==-trans {a} {a} {id a} {id a} {id a} ==-id ==-id = ==-id
+               ==-trans {a} {b} (==-next x x=y) (==-next y y=z) = ==-next (IsEquivalence.trans (Graph.isEq G) x y ) (==-trans x=y y=z)
+
+               identityL : {A B : Graph.vertex G} {f : Chain G A B} → (id B ・ f) == f
+               identityL = ==-refl
+               identityR : {A B : Graph.vertex G} {f : Chain G A B} → (f ・ id A) == f
+               identityR {a} {_} {id a} = ==-id
+               identityR {a} {b} {next {a} {c} {b} x f}  = ==-next (IsEquivalence.refl (Graph.isEq G)) identityR
                o-resp-≈  : {A B C : Graph.vertex G} {f g : Chain G A B} {h i : Chain G B C} →
-                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-               o-resp-≈  refl refl = refl
+                            f == g → h == i → (h ・ f) == (i ・ g)
+               o-resp-≈ ==-id ==-id = ==-id
+               o-resp-≈ ==-id (==-next x h=i) = ==-next x (==-trans identityR (==-trans h=i (==-sym identityR )))
+               o-resp-≈ (==-next x f=g) ==-id = ==-next x f=g
+               o-resp-≈ (==-next x f=g) (==-next x₁ h=i) = ==-next x₁ (o-resp-≈ (==-next x f=g) h=i)
                associative : {a b c d : Graph.vertex G} (f : Chain G c d) (g : Chain G b c) (h : Chain G a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
-               associative (id a) g h = refl
-               associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
+                            (f ・ (g ・ h)) == ((f ・ g) ・ h)
+               associative (id a) g h = ==-refl
+               associative (next x f) g h = ==-next (IsEquivalence.refl (Graph.isEq G)) (associative f g h)
 
 
 
@@ -79,7 +99,7 @@
    arrow-g :  TwoHom t0 t1
 
 TwoCat' : Category  Level.zero Level.zero Level.zero
-TwoCat'  = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } )
+TwoCat'  = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom ; _≅_ = _≡_; isEq = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} } )
    where open graphtocat
 
 _×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
@@ -151,7 +171,7 @@
 open import Data.Empty
 
 DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
-DiscreteCat'  S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ →  ⊥  ) } )
+DiscreteCat'  S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ →  ⊥  ); _≅_ = _≡_; isEq = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} } )
    where open graphtocat 
 
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)