--- a/equalizer.agda	Wed Sep 04 14:51:36 2013 +0900
+++ b/equalizer.agda	Wed Sep 04 17:36:32 2013 +0900
@@ -54,6 +54,45 @@
       → Hom A c c'   --- != id1 A c
 equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa)
 
+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 ) → {eff : Equalizer A {c} f f} 
+      → A [ A [ equalizer-iso eqa eqa' o  equalizer-iso eqa' eqa ] ≈  id1 A c' ]
+equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {eff} =  let open ≈-Reasoning (A) in
+             begin
+                 equalizer-iso eqa eqa' o  equalizer-iso eqa' eqa 
+             ≈⟨⟩
+                 k eqa' (e eqa) (ef=eg eqa)  o k eqa (e eqa') (ef=eg eqa')
+             ≈⟨ car (uniqueness eqa' {!!}) ⟩
+                 {!!} o k eqa (e eqa') (ef=eg eqa')
+             ≈⟨ {!!} ⟩
+                 id1 A c'
+             ∎
+
+-- ke = e' k'e' = e  → k k' = 1 , k' k = 1
+--     ke  = e'
+--     k'ke  = k'e' = e   kk' = 1
+
+--     x e = e -> x = id?
+
+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 )
+
+
+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 ] 
+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)     
+             ≈⟨ uniqueness eqa ( begin
+                    e eqa o id1 A a
+                 ≈⟨ idR ⟩
+                    e eqa 
+                 ≈⟨ e=1 ⟩
+                    id1 A a
+             ∎ )⟩
+                   id1 A a
+             ∎
+
 --           e eqa f g        f
 --         c ----------> a ------->b
 --         ^ ---> d --->