--- a/equalizer.agda	Wed Sep 11 20:26:48 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 10:04:18 2013 +0900
@@ -96,17 +96,16 @@
 equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a } 
                 (h-1 : Hom A c' c ) → (h : Hom A c c' ) →
                 A [ A [ h o h-1 ]  ≈ id1 A c' ] → A [ A [ h-1  o h ]  ≈ id1 A c ] →
-                 ( fe=ge' : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [  e  o h-1 ] ] ] )
                 ( eqa : Equalizer A e f g ) 
            → Equalizer A (A [ e  o h-1  ] ) f g
-equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} h-1 h  hh-1=1 h-1h=1  fe=ge' eqa =  record {
+equalizer+iso  {a} {b} {c} {c'} {f} {g} {e} h-1 h  hh-1=1 h-1h=1  eqa =  record {
       fe=ge = fe=ge1 ;
       k = λ j eq → A [ h o k eqa j eq ] ;
       ek=h = ek=h1 ;
       uniqueness = uniqueness1
   } where
       fe=ge1 :  A [ A [ f o  A [ e  o h-1  ]  ]  ≈ A [ g o  A [ e  o h-1  ]  ] ]
-      fe=ge1 = fe=ge'
+      fe=ge1 = f1=gh ( fe=ge eqa )
       ek=h1 :   {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} →
                 A [ A [  A [ e  o h-1  ]  o A [ h o k eqa j eq ] ] ≈ j ]
       ek=h1 {d} {j} {eq} =  let open ≈-Reasoning (A) in
@@ -249,7 +248,8 @@
                    ∎ )⟩
                      k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) )
               ∎ )⟩
-                 equalizer keqa'  o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩
+                 equalizer keqa'  o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) 
+              ≈⟨ ek=h keqa' ⟩
                  id c
               ∎
 
@@ -258,7 +258,7 @@
 --------------------------------
 ----
 --
--- An equalizer satisfies Burroni equations
+-- Existence of equalizer satisfies Burroni equations
 --
 ----
 
@@ -351,9 +351,10 @@
 
      lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
               A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 
-                 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
-                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
-              k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
+                              equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
+                     (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) 
+                 o k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) 
+                     (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
               ≈ j ]
      lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
              begin