# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378710909 -32400
# Node ID e0835b8dd51b3f077cf919b9931547b6b158e2cc
# Parent  40947f08bab62a52c476c25e8c23e092c5051a12
comment

diff -r 40947f08bab6 -r e0835b8dd51b equalizer.agda
--- a/equalizer.agda	Mon Sep 09 16:03:14 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 16:15:09 2013 +0900
@@ -209,6 +209,9 @@
                  e'
               ∎
 
+--    e←e' e'←e = e
+--    e'←e e←e = e'  is enough for isomorphism but we want to prove l o r = id also.
+
 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 )
       →  ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ])  (A [ g o e' ]) )
       →  A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ]  ≈ id1 A c' ]