Mercurial > hg > Members > kono > Proof > category

comparison discrete.agda @ 457:0ba86e29f492

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit-to and discrete clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 18:30:58 +0900
parents 4d97955ea419
children fd79b6d9f350
comparison
equal deleted inserted replaced
456:4d97955ea419 457:0ba86e29f492
2 open import Level 2 open import Level
3 3
4 module discrete where 4 module discrete where
5 5
6 open import Relation.Binary.Core 6 open import Relation.Binary.Core
7 open import Relation.Nullary
8 open import Data.Empty
9 open import Data.Unit
10 open import Data.Maybe
11 open import cat-utility
12 open import HomReasoning
13
14 open Functor
15 7
16 data TwoObject {c₁ : Level} : Set c₁ where 8 data TwoObject {c₁ : Level} : Set c₁ where
17 t0 : TwoObject 9 t0 : TwoObject
18 t1 : TwoObject 10 t1 : TwoObject
19 11
23 --- f 15 --- f
24 --- -----→ 16 --- -----→
25 --- 0 1 17 --- 0 1
26 --- -----→ 18 --- -----→
27 --- g 19 --- g
20 --
21 -- missing arrows are constrainted by TwoHom data
28 22
29 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where 23 data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where
30 id-t0 : TwoHom t0 t0 24 id-t0 : TwoHom t0 t0
31 id-t1 : TwoHom t1 t1 25 id-t1 : TwoHom t1 t1
32 arrow-f : TwoHom t0 t1 26 arrow-f : TwoHom t0 t1
55 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } 49 assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} }
56 {f : (TwoHom {c₁} {c₂ } c d )} → 50 {f : (TwoHom {c₁} {c₂ } c d )} →
57 {g : (TwoHom {c₁} {c₂ } b c )} → 51 {g : (TwoHom {c₁} {c₂ } b c )} →
58 {h : (TwoHom {c₁} {c₂ } a b )} → 52 {h : (TwoHom {c₁} {c₂ } a b )} →
59 ( f × (g × h)) ≡ ((f × g) × h ) 53 ( f × (g × h)) ≡ ((f × g) × h )
60 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h 54 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl
61 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl 55 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl
62 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl 56 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl
63 assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl 57 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl
64 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl 58 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl
65 assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl 59 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl
66 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl 60 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl
67 assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl 61 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl
68 assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl
69 62
70 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) 63 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a )
71 TwoId {_} {_} t0 = id-t0 64 TwoId {_} {_} t0 = id-t0
72 TwoId {_} {_} t1 = id-t1 65 TwoId {_} {_} t1 = id-t1
73 66
74 open import Relation.Binary
75 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) 67 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
76 68
77 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ 69 TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂
78 TwoCat {c₁} {c₂} = record { 70 TwoCat {c₁} {c₂} = record {
79 Obj = TwoObject {c₁} ; 71 Obj = TwoObject {c₁} ;
88 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; 80 o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
89 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} 81 associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h}
90 } 82 }
91 } where 83 } where
92 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f 84 identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f
93 identityL {c₁} {c₂} {a} {b} {f} with f 85 identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl
94 identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl 86 identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl
95 identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl 87 identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl
96 identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl 88 identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl
97 identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl
98 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f 89 identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f
99 identityR {c₁} {c₂} {_} {_} {f} with f 90 identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl
100 identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl 91 identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl
101 identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl 92 identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl
102 identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl 93 identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl
103 identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl
104 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → 94 o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} →
105 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) 95 f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g )
106 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = 96 o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i =
107 let open ≡-Reasoning in begin 97 let open ≡-Reasoning in begin
108 ( h × f ) 98 ( h × f )
114 comp (i) (g) 104 comp (i) (g)
115 ≡⟨ refl ⟩ 105 ≡⟨ refl ⟩
116 ( i × g ) 106 ( i × g )
117 ∎ 107 ∎
118 108
119 indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A
120 indexFunctor {c₁} {c₂} {ℓ} A a b f g = record {
121 FObj = λ a → fobj a
122 ; FMap = λ {a} {b} f → fmap {a} {b} f
123 ; isFunctor = record {
124 identity = λ{x} → identity x
125 ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g}
126 ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f}
127 }
128 } where
129 T = TwoCat {c₁} {c₂}
130 fobj : Obj T → Obj A
131 fobj t0 = a
132 fobj t1 = b
133 fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y)
134 fmap {t0} {t0} id-t0 = id1 A a
135 fmap {t1} {t1} id-t1 = id1 A b
136 fmap {t0} {t1} arrow-f = f
137 fmap {t0} {t1} arrow-g = g
138 ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ]
139 ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom
140 identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ]
141 identity t0 = let open ≈-Reasoning A in refl-hom
142 identity t1 = let open ≈-Reasoning A in refl-hom
143 distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
144 A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ]
145 distr1 {a} {b} {c} {f} {g} with f | g
146 distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL
147 distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin
148 id1 A b
149 ≈↑⟨ idL ⟩
150 id1 A b o id1 A b
151 ∎
152 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin
153 fmap (comp arrow-f id-t0)
154 ≈⟨⟩
155 fmap arrow-f
156 ≈↑⟨ idR ⟩
157 fmap arrow-f o id1 A a
158 ∎
159 distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin
160 fmap (comp arrow-g id-t0)
161 ≈⟨⟩
162 fmap arrow-g
163 ≈↑⟨ idR ⟩
164 fmap arrow-g o id1 A a
165 ∎
166 distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin
167 fmap (comp id-t1 arrow-f)
168 ≈⟨⟩
169 fmap arrow-f
170 ≈↑⟨ idL ⟩
171 id1 A b o fmap arrow-f
172 ∎
173 distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin
174 fmap (comp id-t1 arrow-g)
175 ≈⟨⟩
176 fmap arrow-g
177 ≈↑⟨ idL ⟩
178 id1 A b o fmap arrow-g
179 ∎
180
181 --- Equalizer
182 --- f
183 --- e -----→
184 --- c -----→ a b
185 --- ^ / -----→
186 --- |k h g
187 --- | /
188 --- | / ^
189 --- | / |
190 --- |/ | Γ
191 --- d _ |
192 --- |\ |
193 --- \ K af
194 --- \ -----→
195 --- \ t0 t1
196 --- -----→
197 --- ag
198 ---
199 ---
200
201 open Complete
202 open Limit
203 open NTrans
204
205 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) ->
206 Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
207 equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = ? -- TMap (limit-u comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0
208
209 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
210 (comp : Complete A (TwoCat {c₁} {c₂} ) )
211 → {a b : Obj A} (f g : Hom A a b )
212 → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] )
213 → IsEqualizer A (equlimit A f g comp ) f g
214 lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record {
215 fe=ge = fe=ge
216 ; k = λ {d} h fh=gh → k {d} h fh=gh
217 ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
218 ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
219 } where
220 I = TwoCat {c₁} {c₂}
221 Γ : Functor I A
222 Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
223 c = limit-c comp Γ
224 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
225 nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
226 nmap x d h with x
227 ... | t0 = h
228 ... | t1 = A [ f o h ]
229 commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ]
230 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
231 commute1 {x} {y} {f'} d h fh=gh with f'
232 commute1 {t0} {t1} {f'} d h fh=gh | arrow-f = let open ≈-Reasoning A in begin
233 f o h
234 ≈↑⟨ idR ⟩
235 (f o h ) o id1 A d
236 ∎
237 commute1 {t0} {t1} {f'} d h fh=gh | arrow-g = let open ≈-Reasoning A in begin
238 g o h
239 ≈↑⟨ fh=gh ⟩
240 f o h
241 ≈↑⟨ idR ⟩
242 (f o h ) o id1 A d
243 ∎
244 commute1 {t0} {t0} {f'} d h fh=gh | id-t0 = let open ≈-Reasoning A in begin
245 id1 A a o h
246 ≈⟨ idL ⟩
247 h
248 ≈↑⟨ idR ⟩
249 h o id1 A d
250 ∎
251 commute1 {t1} {t1} {f'} d h fh=gh | id-t1 = let open ≈-Reasoning A in begin
252 id1 A b o ( f o h )
253 ≈⟨ idL ⟩
254 f o h
255 ≈↑⟨ idR ⟩
256 ( f o h ) o id1 A d
257 ∎
258 nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
259 nat1 d h fh=gh = record {
260 TMap = λ x → nmap x d h ;
261 isNTrans = record {
262 commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
263 }
264 }
265 e = equlimit A f g comp
266 eqlim = isLimit comp Γ (nat1 c e fe=ge )
267 k {d} h fh=gh = limit eqlim d (nat1 d h fh=gh )
268 ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ]
269 ek=h d h fh=gh = let open ≈-Reasoning A in begin
270 e o k h fh=gh
271 ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0} ⟩
272 h
273 ∎
274 uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c )
275 ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] →
276 A [ A [ TMap (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ]
277 uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
278 (nmap t0 c e ) o k'
279 ≈⟨⟩
280 e o k'
281 ≈⟨ ek'=h ⟩
282 h
283 ≈⟨⟩
284 nmap t0 d h
285 ∎
286 uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin
287 (nmap t1 c e ) o k'
288 ≈⟨⟩
289 (f o e ) o k'
290 ≈↑⟨ assoc ⟩
291 f o ( e o k' )
292 ≈⟨ cdr ek'=h ⟩
293 f o h
294 ≈⟨⟩
295 TMap (nat1 d h fh=gh) t1
296 ∎
297 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
298 ( k' : Hom A d c )
299 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
300 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin
301 k h fh=gh
302 ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
303 k'
304 ∎
305