# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378698936 -32400
# Node ID efa2fd0e91eedeccb65027f937817b93a78f68dc
# Parent  f6e8d6d04af80f158e67a86b02f6456078821426
fix

diff -r f6e8d6d04af8 -r efa2fd0e91ee equalizer.agda
--- a/equalizer.agda	Mon Sep 09 12:47:53 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 12:55:36 2013 +0900
@@ -285,34 +285,12 @@
      cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
                  k (eqa f g ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
              ≈⟨ uniqueness (eqa f g) ( begin
-                 e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o  h)
-             ≈⟨ assoc  ⟩
-                 (e o  k (eqa f f {e}) (id1 A a) (f1=f1 f)) o  h
-             ≈⟨ car ( ek=h (eqa f f {e})) ⟩
-                 id1 A a  o h
-             ≈⟨ idL ⟩
-                 h
-             ≈↑⟨ idR ⟩
-                 h o (id1 A d ) 
-             ≈⟨⟩
-                 h o equalizer (eqa ( f o h ) ( g o h )) 
+                 e o k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
+             ≈⟨ ek=h (eqa f g ) ⟩
+                 h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
+             ≈↑⟨ car h=h'  ⟩
+                 h o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] )))
              ∎ )⟩    
-                 k (eqa f f {e}) (id1 A a) (f1=f1 f) o  h
-             ≈⟨ cdr h=h'  ⟩
-                 k (eqa f f {e}) (id1 A a) (f1=f1 f) o  h'
-             ≈↑⟨ uniqueness (eqa f g)  ( begin
-                 e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o  h')
-             ≈⟨ assoc  ⟩
-                 (e o  k (eqa f f {e}) (id1 A a) (f1=f1 f)) o  h'
-             ≈⟨ car ( ek=h (eqa f f {e})) ⟩
-                 id1 A a  o h'
-             ≈⟨ idL ⟩
-                 h'
-             ≈↑⟨ idR ⟩
-                 h' o (id1 A d )
-             ≈⟨⟩
-                 h' o equalizer (eqa ( f o h' ) ( g o h' ))
-             ∎ )⟩
                  k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
              ∎
      cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f)  ≈