Mercurial > hg > Members > kono > Proof > category

comparison discrete.agda @ 799:82a8c1ab4ef5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 11:30:34 +0900
parents 340708e8d54f
children 984d20c10c87
comparison
equal deleted inserted replaced
798:6e6c7ad8ea1c 799:82a8c1ab4ef5
5 5
6 open import Relation.Binary.Core 6 open import Relation.Binary.Core
7 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) 7 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
8 8
9 9
10 data TwoObject {c₁ : Level} : Set c₁ where 10
11 module graphtocat where
12
13 data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
14 id : ( a : obj ) → Arrow a a
15 mono : { a b : obj } → hom a b → Arrow a b
16 connected : {a b : obj } → {c : obj} → hom b c → Arrow {obj} {hom} a b → Arrow a c
17
18 _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
19 id a + id .a = id a
20 id b + mono x = mono x
21 id a + connected x y = connected x y
22 mono x + id a = mono x
23 mono x + mono y = connected x (mono y)
24 mono x + connected y z = connected x ( connected y z )
25 connected x y + z = connected x ( y + z )
26
27 assoc-+ : { obj : Set } { hom : obj → obj → Set } {a b c d : obj }
28 (f : (Arrow {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) →
29 ( f + (g + h)) ≡ ((f + g) + h )
30 assoc-+ (id a) (id .a) (id .a) = refl
31 assoc-+ (id a) (id .a) (mono x) = refl
32 assoc-+ (id a) (id .a) (connected h h₁) = refl
33 assoc-+ (id a) (mono x) (id a₁) = refl
34 assoc-+ (id a) (mono x) (mono x₁) = refl
35 assoc-+ (id a) (mono x) (connected h h₁) = refl
36 assoc-+ (id a) (connected g h) _ = refl
37 assoc-+ (mono x) (id a) (id .a) = refl
38 assoc-+ (mono x) (id a) (mono x₁) = refl
39 assoc-+ (mono x) (id a) (connected h h₁) = refl
40 assoc-+ (mono x) (mono x₁) (id a) = refl
41 assoc-+ (mono x) (mono x₁) (mono x₂) = refl
42 assoc-+ (mono x) (mono x₁) (connected h h₁) = refl
43 assoc-+ (mono x) (connected g g₁) _ = refl
44 assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y )
45
46 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
47
48 GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) → Category Level.zero Level.zero Level.zero
49 GraphtoCat obj hom = record {
50 Obj = obj ;
51 Hom = λ a b → Arrow a b ;
52 _o_ = λ{a} {b} {c} x y → _+_ x y ;
53 _≈_ = λ x y → x ≡ y ;
54 Id = λ{a} → id a ;
55 isCategory = record {
56 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
57 identityL = λ{a b f} → identityL {a} {b} {f} ;
58 identityR = λ{a b f} → identityR {a} {b} {f} ;
59 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
60 associative = λ{a b c d f g h } → assoc-+ f g h
61 }
62 } where
63 identityL : {A B : obj } {f : ( Arrow A B) } → ((id B) + f) ≡ f
64 identityL {_} {_} {id a} = refl
65 identityL {_} {_} {mono x} = refl
66 identityL {_} {_} {connected x f} = refl
67 identityR : {A B : obj } {f : ( Arrow {obj} {hom} A B) } → ( f + id A ) ≡ f
68 identityR {_} {_} {id a} = refl
69 identityR {_} {_} {mono x} = refl
70 identityR {_} {_} {connected x f} = cong (λ k → connected x k) ( identityR {_} {_} {f} )
71 o-resp-≈ : {A B C : obj } {f g : ( Arrow A B)} {h i : ( Arrow B C)} →
72 f ≡ g → h ≡ i → ( h + f ) ≡ ( i + g )
73 o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
74
75
76 data TwoObject : Set where
11 t0 : TwoObject 77 t0 : TwoObject
12 t1 : TwoObject 78 t1 : TwoObject
13 79
14 --- 80 ---
15 --- two objects category ( for limit to equalizer proof ) 81 --- two objects category ( for limit to equalizer proof )
20 --- -----→ 86 --- -----→
21 --- g 87 --- g
22 -- 88 --
23 -- missing arrows are constrainted by TwoHom data 89 -- missing arrows are constrainted by TwoHom data
24 90
25 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where 91 data TwoHom : TwoObject → TwoObject → Set where
26 id-t0 : TwoHom t0 t0 92 id-t0 : TwoHom t0 t0
27 id-t1 : TwoHom t1 t1 93 id-t1 : TwoHom t1 t1
28 arrow-f : TwoHom t0 t1 94 arrow-f : TwoHom t0 t1
29 arrow-g : TwoHom t0 t1 95 arrow-g : TwoHom t0 t1
30 96
31 97 TwoCat' : Category Level.zero Level.zero Level.zero
32 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c 98 TwoCat' = GraphtoCat TwoObject TwoHom
33 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f 99 where open graphtocat
34 _×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g 100
35 _×_ {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 101 _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c
36 _×_ {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f 102 _×_ {t0} {t1} {t1} id-t1 arrow-f = arrow-f
37 _×_ {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g 103 _×_ {t0} {t1} {t1} id-t1 arrow-g = arrow-g
38 _×_ {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 104 _×_ {t1} {t1} {t1} id-t1 id-t1 = id-t1
105 _×_ {t0} {t0} {t1} arrow-f id-t0 = arrow-f
106 _×_ {t0} {t0} {t1} arrow-g id-t0 = arrow-g
107 _×_ {t0} {t0} {t0} id-t0 id-t0 = id-t0
108
39 109
40 open TwoHom 110 open TwoHom
41 111
42 -- f g h 112 -- f g h
43 -- d <- c <- b <- a 113 -- d <- c <- b <- a
44 -- 114 --
45 -- It can be proved without TwoHom constraints 115 -- It can be proved without TwoHom constraints
46 116
47 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } 117 assoc-× : {a b c d : TwoObject }
48 {f : (TwoHom {c₁} {c₂ } c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} → 118 {f : (TwoHom c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
49 ( f × (g × h)) ≡ ((f × g) × h ) 119 ( f × (g × h)) ≡ ((f × g) × h )
50 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl 120 assoc-× {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
51 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl 121 assoc-× {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
52 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl 122 assoc-× {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
53 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl 123 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
54 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl 124 assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
55 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl 125 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
56 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl 126 assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
57 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl 127 assoc-× {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl
58 128
59 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) 129 TwoId : (a : TwoObject ) → (TwoHom a a )
60 TwoId {_} {_} t0 = id-t0 130 TwoId t0 = id-t0
61 TwoId {_} {_} t1 = id-t1 131 TwoId t1 = id-t1
62 132
63 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) 133 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
64 134
65 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ 135 TwoCat : Category Level.zero Level.zero Level.zero
66 TwoCat {c₁} {c₂} = record { 136 TwoCat = record {
67 Obj = TwoObject ; 137 Obj = TwoObject ;
68 Hom = λ a b → TwoHom a b ; 138 Hom = λ a b → TwoHom a b ;
69 _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
70 _≈_ = λ x y → x ≡ y ; 139 _≈_ = λ x y → x ≡ y ;
71 Id = λ{a} → TwoId a ; 140 Id = λ{a} → TwoId a ;
72 isCategory = record { 141 isCategory = record {
73 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; 142 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
74 identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ; 143 identityL = λ{a b f} → identityL {a} {b} {f} ;
75 identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ; 144 identityR = λ{a b f} → identityR {a} {b} {f} ;
76 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; 145 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
77 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} 146 associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h}
78 } 147 }
79 } where 148 } where
80 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f 149 identityL : {A B : TwoObject } {f : ( TwoHom A B) } → ((TwoId B) × f) ≡ f
81 identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl 150 identityL {t1} {t1} { id-t1 } = refl
82 identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl 151 identityL {t0} {t0} { id-t0 } = refl
83 identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl 152 identityL {t0} {t1} { arrow-f } = refl
84 identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl 153 identityL {t0} {t1} { arrow-g } = refl
85 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f 154 identityR : {A B : TwoObject } {f : ( TwoHom A B) } → ( f × TwoId A ) ≡ f
86 identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl 155 identityR {t1} {t1} { id-t1 } = refl
87 identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl 156 identityR {t0} {t0} { id-t0 } = refl
88 identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl 157 identityR {t0} {t1} { arrow-f } = refl
89 identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl 158 identityR {t0} {t1} { arrow-g } = refl
90 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → 159 o-resp-≈ : {A B C : TwoObject } {f g : ( TwoHom A B)} {h i : ( TwoHom B C)} →
91 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) 160 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
92 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl 161 o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl
93 162
94 163
95 -- Category with no arrow but identity 164 -- Category with no arrow but identity
165
166
167 open import Data.Empty
168
169 DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero
170 DiscreteCat' S = GraphtoCat S ( λ _ _ → ⊥ )
171 where open graphtocat
96 172
97 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 173 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)
98 : Set c₁ where 174 : Set c₁ where
99 field 175 field
100 discrete : a ≡ b -- if f : a → b then a ≡ b 176 discrete : a ≡ b -- if f : a → b then a ≡ b