Mercurial > hg > Members > kono > Proof > category

diff 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
line wrap: on
line diff
--- a/equalizer.agda	Sat Sep 14 11:20:18 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 11:21:42 2013 +0900
@@ -98,7 +98,11 @@
                    equalizer eqa  o j
               ∎ )⟩
                  k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) )
-              ≈⟨ uniqueness eqa refl-hom ⟩
+              ≈⟨ uniqueness eqa ( begin
+                   equalizer eqa o j
+              ≈⟨⟩
+                   equalizer eqa o j
+              ∎ )⟩
                  j
               ∎