Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 248:efa2fd0e91ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 12:55:36 +0900
parents f6e8d6d04af8
children bdeed843f8b1
comparison
equal deleted inserted replaced
247:f6e8d6d04af8 248:efa2fd0e91ee
283 A [ k (eqa f g {e} ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 283 A [ k (eqa f g {e} ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
284 ≈ k (eqa f g {e} ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ] 284 ≈ k (eqa f g {e} ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ]
285 cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin 285 cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
286 k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 286 k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
287 ≈⟨ uniqueness (eqa f g) ( begin 287 ≈⟨ uniqueness (eqa f g) ( begin
288 e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o h) 288 e o k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
289 ≈⟨ assoc ⟩ 289 ≈⟨ ek=h (eqa f g ) ⟩
290 (e o k (eqa f f {e}) (id1 A a) (f1=f1 f)) o h 290 h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] )))
291 ≈⟨ car ( ek=h (eqa f f {e})) ⟩ 291 ≈↑⟨ car h=h' ⟩
292 id1 A a o h 292 h o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] )))
293 ≈⟨ idL ⟩
294 h
295 ≈↑⟨ idR ⟩
296 h o (id1 A d )
297 ≈⟨⟩
298 h o equalizer (eqa ( f o h ) ( g o h ))
299 ∎ )⟩ 293 ∎ )⟩
300 k (eqa f f {e}) (id1 A a) (f1=f1 f) o h
301 ≈⟨ cdr h=h' ⟩
302 k (eqa f f {e}) (id1 A a) (f1=f1 f) o h'
303 ≈↑⟨ uniqueness (eqa f g) ( begin
304 e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o h')
305 ≈⟨ assoc ⟩
306 (e o k (eqa f f {e}) (id1 A a) (f1=f1 f)) o h'
307 ≈⟨ car ( ek=h (eqa f f {e})) ⟩
308 id1 A a o h'
309 ≈⟨ idL ⟩
310 h'
311 ≈↑⟨ idR ⟩
312 h' o (id1 A d )
313 ≈⟨⟩
314 h' o equalizer (eqa ( f o h' ) ( g o h' ))
315 ∎ )⟩
316 k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) 294 k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
317 ∎ 295 ∎
318 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f) ≈ 296 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f) ≈
319 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ] 297 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ]
320 cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in 298 cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in