Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 252:e0835b8dd51b

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:15:09 +0900
parents 40947f08bab6
children 24e83b8b81be
comparison
equal deleted inserted replaced
251:40947f08bab6 252:e0835b8dd51b
206 ≈⟨ cdr ( ek=h keqa ) ⟩ 206 ≈⟨ cdr ( ek=h keqa ) ⟩
207 e' o id1 A c' 207 e' o id1 A c'
208 ≈⟨ idR ⟩ 208 ≈⟨ idR ⟩
209 e' 209 e'
210 ∎ 210 ∎
211
212 -- e←e' e'←e = e
213 -- e'←e e←e = e' is enough for isomorphism but we want to prove l o r = id also.
211 214
212 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 ) 215 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 )
213 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 216 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
214 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ] 217 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ]
215 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 218 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin