Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 251:40947f08bab6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 16:03:14 +0900
parents a1e2228c2a6b
children e0835b8dd51b
comparison
equal deleted inserted replaced
250:a1e2228c2a6b 251:40947f08bab6
29 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] 29 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ]
30 equalizer : Hom A c a 30 equalizer : Hom A c a
31 equalizer = e 31 equalizer = e
32 32
33 -- 33 --
34 -- Flat Equational Definition of Equalizer 34 -- Burroni's Flat Equational Definition of Equalizer
35 -- 35 --
36 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 36 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
37 field 37 field
38 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (e : Hom A c a ) → Hom A c a 38 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (e : Hom A c a ) → Hom A c a
39 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c 39 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
77 (g o e ) o h 77 (g o e ) o h
78 ≈↑⟨ assoc ⟩ 78 ≈↑⟨ assoc ⟩
79 g o ( e o h ) 79 g o ( e o h )
80 ∎ 80 ∎
81 81
82 --------------------------------
82 -- 83 --
83 -- 84 --
84 -- An isomorphic arrow c' to c makes another equalizer 85 -- An isomorphic arrow c' to c makes another equalizer
85 -- 86 --
86 -- e eqa f g f 87 -- e eqa f g f
141 id1 A c' o j 142 id1 A c' o j
142 ≈⟨ idL ⟩ 143 ≈⟨ idL ⟩
143 j 144 j
144 ∎ 145 ∎
145 146
147 --------------------------------
146 -- 148 --
147 -- If we have two equalizers on c and c', there are isomorphic pair h, h' 149 -- If we have two equalizers on c and c', there are isomorphic pair h, h'
148 -- 150 --
149 -- h : c → c' h' : c' → c 151 -- h : c → c' h' : c' → c
150 -- e' = h o e 152 -- e' = h o e
171 -- 173 --
172 -- h j e f = h j e g → h = 'j e f 174 -- h j e f = h j e g → h = 'j e f
173 -- h = j e f -> j = j' 175 -- h = j e f -> j = j'
174 -- 176 --
175 177
176 c-iso→' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) 178 e←e' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g )
177 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 179 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
178 → A [ A [ e' o c-iso-l eqa eqa' keqa ] ≈ e ] 180 → A [ A [ e' o c-iso-l eqa eqa' keqa ] ≈ e ]
179 c-iso→' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 181 e←e' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
180 e' o c-iso-l eqa eqa' keqa 182 e' o c-iso-l eqa eqa' keqa
181 ≈⟨⟩ 183 ≈⟨⟩
182 e' o k eqa' e (fe=ge eqa) 184 e' o k eqa' e (fe=ge eqa)
183 ≈⟨⟩ 185 ≈⟨⟩
184 equalizer eqa' o k eqa' e (fe=ge eqa) 186 equalizer eqa' o k eqa' e (fe=ge eqa)
185 ≈⟨ ek=h eqa' ⟩ 187 ≈⟨ ek=h eqa' ⟩
186 e 188 e
187 ∎ 189 ∎
188 190
189 c-iso←' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) 191 e'←e : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g )
190 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 192 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
191 → A [ A [ e o c-iso-r eqa eqa' keqa ] ≈ e' ] 193 → A [ A [ e o c-iso-r eqa eqa' keqa ] ≈ e' ]
192 c-iso←' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 194 e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
193 e o c-iso-r eqa eqa' keqa 195 e o c-iso-r eqa eqa' keqa
194 ≈⟨⟩ 196 ≈⟨⟩
195 e o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 197 e o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
196 ≈↑⟨ car (ek=h eqa' ) ⟩ 198 ≈↑⟨ car (ek=h eqa' ) ⟩
197 ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 199 ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
230 equalizer keqa' o k eqa' e (fe=ge eqa ) 232 equalizer keqa' o k eqa' e (fe=ge eqa )
231 ≈⟨ cdr ( begin 233 ≈⟨ cdr ( begin
232 k eqa' e (fe=ge eqa ) 234 k eqa' e (fe=ge eqa )
233 ≈⟨ uniqueness eqa' ( begin 235 ≈⟨ uniqueness eqa' ( begin
234 e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) 236 e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
235 ≈↑⟨ car (c-iso←' eqa eqa' keqa ) ⟩ 237 ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩
236 ( e o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) 238 ( e o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))
237 ≈↑⟨ assoc ⟩ 239 ≈↑⟨ assoc ⟩
238 e o ( equalizer keqa' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))) 240 e o ( equalizer keqa' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)))
239 ≈⟨ cdr ( ek=h keqa' ) ⟩ 241 ≈⟨ cdr ( ek=h keqa' ) ⟩
240 e o id1 A c 242 e o id1 A c
247 id1 A c 249 id1 A c
248 ∎ 250 ∎
249 251
250 252
251 253
254 --------------------------------
252 ---- 255 ----
253 -- 256 --
254 -- An equalizer satisfies Burroni equations 257 -- An equalizer satisfies Burroni equations
255 -- 258 --
256 ---- 259 ----
371 j o id1 A d 374 j o id1 A d
372 ≈⟨ idR ⟩ 375 ≈⟨ idR ⟩
373 j 376 j
374 ∎ 377 ∎
375 378
379 --------------------------------
380 --
381 -- Bourroni equations gives an Equalizer
382 --
376 383
377 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a ) 384 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a )
378 → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g e) f g 385 → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g e) f g
379 lemma-equ2 {a} {b} {c} f g e bur = record { 386 lemma-equ2 {a} {b} {c} f g e bur = record {
380 fe=ge = fe=ge1 ; 387 fe=ge = fe=ge1 ;