Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 223:8b3aeba14b5e

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 Thu, 05 Sep 2013 04:35:22 +0900
parents 0bc85361b7d0
children a9d311cea336
comparison
equal deleted inserted replaced
222:0bc85361b7d0 223:8b3aeba14b5e
344 e eqa o h' 344 e eqa o h'
345 ∎ ) ⟩ 345 ∎ ) ⟩
346 k' 346 k'
347 ∎ 347 ∎
348 348
349 iso-rev : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) → Hom A a c
350 iso-rev {a} {b} {c} {f} {g} eq eqa = k eqa (id1 A a) (f1=g1 eq)
351
352 equalizer-iso-pair : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) →
353 A [ A [ e eqa o iso-rev eq eqa ] ≈ id1 A a ]
354 equalizer-iso-pair {a} {b} {c} {f} {g} eq eqa = ek=h eqa
355
349 -- Equalizer is unique up to iso 356 -- Equalizer is unique up to iso
350 357
351 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) 358 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
352 → Hom A c c' --- != id1 A c 359 → Hom A c c' --- != id1 A c
353 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa) 360 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)