Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 241:9e4dc349831e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comments
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 12:34:35 +0900
parents 964e258e08fb
children 5d1ecfec6f41
comparison
equal deleted inserted replaced
240:964e258e08fb 241:9e4dc349831e
150 150
151 151
152 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a } 152 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a }
153 ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) 153 ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g )
154 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 154 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
155 → Hom A c c' 155 → Hom A c c' -- should be e' = c-sio-l o e
156 c-iso-l {c} {c'} eqa eqa' keqa = equalizer keqa 156 c-iso-l {c} {c'} eqa eqa' keqa = equalizer keqa
157 157
158 c-iso-r : { 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 ) 158 c-iso-r : { 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 )
159 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 159 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
160 → Hom A c' c 160 → Hom A c' c -- e = c-sio-r o e'
161 c-iso-r {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 161 c-iso-r {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
162 162
163 -- e' f 163 -- e' f
164 -- c'----------> a ------->b f e j = g e j 164 -- c'----------> a ------->b f e j = g e j
165 -- ^ g 165 -- ^ g
170 -- 170 --
171 -- h j e f = h j e g → h = 'j e f 171 -- h j e f = h j e g → h = 'j e f
172 -- h = j e f -> j = j' 172 -- h = j e f -> j = j'
173 -- 173 --
174 174
175 -- e = c-iso-l o e' is assumed by equalizer's degree of freedom
175 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 ) 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 )
176 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 177 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
177 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ] 178 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ]
178 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 179 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
179 c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa 180 c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa
184 ∎ 185 ∎
185 186
186 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 ) 187 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 )
187 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) 188 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) )
188 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) 189 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) )
189 → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- refl 190 -- e' = c-iso-r o e is assumed by equalizer's degree of freedom
191 → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- implicit assumption , which should be refl
190 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] 192 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ]
191 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin 193 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin
192 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa 194 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
193 ≈⟨⟩ 195 ≈⟨⟩
194 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) 196 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa )
218 220
219 ---- 221 ----
220 -- 222 --
221 -- An equalizer satisfies Burroni equations 223 -- An equalizer satisfies Burroni equations
222 -- 224 --
223 -- b4 is not yet done 225 -- congs are not yet done
224 ---- 226 ----
225 227
226 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → 228 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) →
227 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) 229 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
228 → Burroni A {c} {a} {b} f g e 230 → Burroni A {c} {a} {b} f g e
300 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) ) 302 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) )
301 ≈⟨ car ((uniqueness (eqa f g) ( begin 303 ≈⟨ car ((uniqueness (eqa f g) ( begin
302 equalizer (eqa f g) o j 304 equalizer (eqa f g) o j
303 ≈↑⟨ idR ⟩ 305 ≈↑⟨ idR ⟩
304 (equalizer (eqa f g) o j ) o id1 A d 306 (equalizer (eqa f g) o j ) o id1 A d
305 ≈⟨⟩ 307 ≈⟨⟩ -- here we decide e (fej) (gej)' is id1 A d
306 ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j))) 308 ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j)))
307 ∎ ))) ⟩ 309 ∎ ))) ⟩
308 j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) 310 j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) )))
309 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin 311 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin
310 equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d 312 equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d
311 ≈⟨ idR ⟩ 313 ≈⟨ idR ⟩
312 equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j)) 314 equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j))
313 ≈⟨⟩ 315 ≈⟨⟩ -- here we decide e (fej) (fej)' is id1 A d
314 id1 A d 316 id1 A d
315 ∎ ))) ⟩ 317 ∎ ))) ⟩
316 j o id1 A d 318 j o id1 A d
317 ≈⟨ idR ⟩ 319 ≈⟨ idR ⟩
318 j 320 j