Mercurial > hg > Members > kono > Proof > category

changeset 256:80dfdeb3e4e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simpler proof
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Sep 2013 11:20:18 +0900
parents 7e7b2c38dee1
children 99751fb809e0
files equalizer.agda
diffstat 1 files changed, 1 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Sat Sep 14 11:19:12 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 11:20:18 2013 +0900
@@ -98,13 +98,7 @@
                    equalizer eqa  o j
               ∎ )⟩
                  k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) )
-              ≈⟨ uniqueness eqa ( begin
-                   equalizer eqa o ( id c o j )
-              ≈⟨ cdr idL ⟩
-                   equalizer eqa o j
-              ∎ )⟩
-                 id c o j
-              ≈⟨ idL ⟩
+              ≈⟨ uniqueness eqa refl-hom ⟩
                  j
               ∎