--- a/equalizer.agda	Thu Sep 05 04:35:22 2013 +0900
+++ b/equalizer.agda	Thu Sep 05 11:39:06 2013 +0900
@@ -49,16 +49,29 @@
 open EqEqualizer
 
 
-f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ]  ]
-f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq )
+f1=g1 : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → (h : Hom A c a) →  A [ A [ f o h ] ≈ A [ g o h ]  ]
+f1=g1 eq h = let open ≈-Reasoning (A) in (resp refl-hom eq )
+
+f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } →
+       (eq : A [ A [ f  o e ] ≈ A [ g  o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e  o h ]  ] ]
+f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in 
+             begin
+                  f o ( e  o h )
+             ≈⟨ assoc  ⟩
+                  (f o  e ) o h 
+             ≈⟨ car eq  ⟩
+                  (g o  e ) o h 
+             ≈↑⟨ assoc  ⟩
+                  g o ( e  o h )
+             ∎
 
 
 equalizer-eq-k  : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {a} f g) → 
       A [ e eqa ≈ id1 A a ] →
-      A [ k eqa (id1 A a) (f1=g1 eq) ≈ id1 A a ] 
+      A [ k eqa (id1 A a) (f1=g1 eq (id1 A a)) ≈ id1 A a ] 
 equalizer-eq-k {a} {b} {f} {g} eq eqa e=1 =  let open ≈-Reasoning (A) in
              begin
-                   k eqa (id1 A a) (f1=g1 eq)     
+                   k eqa (id1 A a) (f1=g1 eq (id1 A a))     
              ≈⟨ uniqueness eqa ( begin
                     e eqa o id1 A a
                  ≈⟨ idR ⟩
@@ -70,7 +83,7 @@
              ∎
 
 equalizer-eq-e  : { a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {a} f g) → (eq : A [ f ≈ g ] ) → 
-      A [ k eqa (id1 A a) (f1=g1 eq) ≈ id1 A a ] →
+      A [ k eqa (id1 A a) (f1=g1 eq (id1 A a)) ≈ id1 A a ] →
       A [ e eqa ≈ id1 A a ] 
 equalizer-eq-e {a} {b} {f} {g} eqa eq k=1 =  let open ≈-Reasoning (A) in
              begin
@@ -78,7 +91,7 @@
              ≈↑⟨ idR ⟩
                    e eqa  o id1 A a
              ≈↑⟨ cdr k=1 ⟩
-                   e eqa  o k eqa (id1 A a) (f1=g1 eq)
+                   e eqa  o k eqa (id1 A a) (f1=g1 eq (id1 A a))
              ≈⟨ ek=h eqa ⟩
                    id1 A a
              ∎
@@ -347,11 +360,11 @@
              ∎
 
 iso-rev  : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) →  Hom A a c
-iso-rev {a} {b} {c} {f} {g} eq eqa = k  eqa (id1 A a) (f1=g1 eq)
+iso-rev {a} {b} {c} {f} {g} eq eqa = k  eqa (id1 A a) (f1=g1 eq (id1 A a))
 
-equalizer-iso-pair  : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) → 
+equalizer-iso-pair  : { a b c : Obj A } {f g : Hom A a b } → {eq : A [ f ≈ g ] } → ( eqa : Equalizer A {c} f g) → 
          A [ A [ e eqa o iso-rev eq eqa  ]  ≈ id1 A a ] 
-equalizer-iso-pair  {a} {b} {c} {f} {g} eq eqa  = ek=h eqa
+equalizer-iso-pair  {a} {b} {c} {f} {g} {eq} eqa  = ek=h eqa
 
 -- Equalizer is unique up to iso
 
@@ -359,27 +372,19 @@
       → Hom A c c'   --- != id1 A c
 equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)
 
-f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } →
-       (eq : A [ A [ f  o e ] ≈ A [ g  o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e  o h ]  ] ]
-f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in 
-             begin
-                  f o ( e  o h )
-             ≈⟨ assoc  ⟩
-                  (f o  e ) o h 
-             ≈⟨ car eq  ⟩
-                  (g o  e ) o h 
-             ≈↑⟨ assoc  ⟩
-                  g o ( e  o h )
-             ∎
-
 --
 --        
 --           e eqa f g        f
 --         c ----------> a ------->b
 --
 equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      { h : Hom A a c } →  ( equalizer-iso-pair {a} {b} {c'} (eefeg eqa) )
+       → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)  ] ≈ id1 A c ]
+equalizer-iso-eq = ?
+
+equalizer-iso-eq' : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
       { h : Hom A a c } →  A [ A [ h o e eqa ] ≈ id1 A c ] → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)  ] ≈ id1 A c ]
-equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {h} rev =  let open ≈-Reasoning (A) in
+equalizer-iso-eq' {c} {c'} {f} {g} eqa eqa' {h} rev =  let open ≈-Reasoning (A) in
              begin
                  k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e  eqa ) (fe=ge eqa)
              ≈↑⟨ idL ⟩