--- a/equalizer.agda	Tue Sep 03 04:29:07 2013 +0900
+++ b/equalizer.agda	Tue Sep 03 13:29:21 2013 +0900
@@ -48,21 +48,11 @@
 open Equalizer
 open EqEqualizer
 
-ff-equal : {a b  : Obj A} (f : Hom A a b)  → (eqa : Equalizer A  f f )  → A [ e eqa  ≈  id1 A a ]
-ff-equal {a} {b} f eqa =  let open ≈-Reasoning (A) in
-             begin
-                  e eqa  
-             ≈↑⟨ ek=h eqa ⟩
-                  e eqa o k eqa (e eqa) refl-hom
-             ≈⟨  {!!}  ⟩
-                  id1 A a
-             ∎
-
 
 lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b)  → 
          ( {a b c : Obj A} → (f g : Hom A a b)  → Equalizer A {c} f g ) → EqEqualizer A {c} f g
 lemma-equ1  A {a} {b} {c} f g eqa = record {
-      α = λ f g →  e (eqa f g ) ; -- Hom A c  a
+      α = λ f g →  e (eqa f g ) ; -- Hom A c a
       γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
       δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
       b1 = ef=eg (eqa f g) ;
@@ -70,6 +60,53 @@
       b3 = lemma-equ3 ;
       b4 = lemma-equ6 
  } where
+     --
+     --           e eqa f g        f
+     --         c ----------> a ------->b
+     --         ^                  g     
+     --         |                           
+     --         |k₁  = e eqa (f o (e (eqa f g))) (g o (e (eqa f g))))
+     --         |        
+     --         d
+     --         
+     --         
+     --               e  o id1 ≈  e  →   k e  ≈ id
+     ff-equal4 : A [ A [ e (eqa f g ) o (e (eqa (A [ f o  e (eqa f g) ] ) (A [ g o e (eqa f g) ] ))) ]  ≈ 
+                         e (eqa f g ) 
+                   ] → 
+          A [ k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ≈  e (eqa (A [ f o  e (eqa f g) ] ) (A [ g o e (eqa f g) ] )) ]
+     ff-equal4 eq =  uniqueness (eqa f g) eq 
+
+     ff-equal3 : A [ e (eqa (A [ f o  e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈  k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ]
+     ff-equal3 = let open ≈-Reasoning (A) in
+             begin
+                  e (eqa (A [ f o  e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) 
+             ≈↑⟨ uniqueness (eqa f g) {!!} ⟩
+                  k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) 
+             ∎
+     ff-equal2 :  A [ k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g)) ≈  id1 A a ]
+     ff-equal2 =  let open ≈-Reasoning (A) in
+             begin
+                  k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g))
+             ≈⟨ uniqueness (eqa f g) idR ⟩
+                 id1 A a
+             ∎
+     ff-equal1 :  A [ e (eqa (A [ f o  e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈  id1 A a ]
+     ff-equal1  =  let open ≈-Reasoning (A) in
+             begin
+                 e (eqa (f o e (eqa f g) ) (g o e (eqa f g) ))
+             ≈⟨ {!!} ⟩
+                 id1 A a
+             ∎
+     ff-equal :  {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ f o A [ e (eqa f g) o k₁ ] ] ) ) ≈  id1 A d ]
+     ff-equal {d} {k₁} =  let open ≈-Reasoning (A) in
+             begin
+                 e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁))
+             ≈⟨ {!!} ⟩
+                 id1 A d
+             ∎
+     fg-equal :  {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ g o A [ e (eqa f g) o k₁ ] ] ) ) ≈  id1 A d ]
+     fg-equal = {!!}
      lemma-equ2 : {a b : Obj A} (f : Hom A a b)  → A [ A [ f o id1 A a ]  ≈ A [ f o id1 A a ] ]
      lemma-equ2 f =   let open ≈-Reasoning (A) in refl-hom
      lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]