Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 257:99751fb809e0

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 Sat, 14 Sep 2013 11:21:42 +0900
parents 80dfdeb3e4e7
children 281b8962abbe
comparison
equal deleted inserted replaced
256:80dfdeb3e4e7 257:99751fb809e0
96 equalizer eqa o i 96 equalizer eqa o i
97 ≈⟨ ei=ej ⟩ 97 ≈⟨ ei=ej ⟩
98 equalizer eqa o j 98 equalizer eqa o j
99 ∎ )⟩ 99 ∎ )⟩
100 k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) ) 100 k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) )
101 ≈⟨ uniqueness eqa refl-hom ⟩ 101 ≈⟨ uniqueness eqa ( begin
102 equalizer eqa o j
103 ≈⟨⟩
104 equalizer eqa o j
105 ∎ )⟩
102 j 106 j
103 ∎ 107 ∎
104 108
105 -------------------------------- 109 --------------------------------
106 -- 110 --