--- a/equalizer.agda	Tue Sep 03 02:38:23 2013 +0900
+++ b/equalizer.agda	Tue Sep 03 04:29:07 2013 +0900
@@ -23,10 +23,10 @@
 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
       e : Hom A c a 
-      ef=eg : A [ A [ f  o  e ] ≈ A [ g  o e ] ]
+      ef=eg : A [ A [ f o e ] ≈ A [ g o e ] ]
       k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-      ke=h : {d : Obj A}  → ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  A [ A [ e  o k {d} h eq ] ≈ h ]
-      uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  (eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] ) →  {k' : Hom A d c } → 
+      ek=h : {d : Obj A}  → ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  A [ A [ e  o k {d} h eq ] ≈ h ]
+      uniqueness : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } → 
               A [ A [ e  o k' ] ≈ h ] → A [ k {d} h eq  ≈ k' ]
    equalizer : Hom A c a
    equalizer = e
@@ -40,7 +40,7 @@
       b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]) ] ]
       b3 :  A [ A [ α f f o δ {a} {b} {a} f ] ≈ id1 A a ]
       -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
-      b4 :  {d : Obj A } {k : Hom A d c} → A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g o k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ k ]    -- k
+      b4 :  {d : Obj A } {k : Hom A d c} → A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g o k ] ) o δ (A [ f o A [ α f g o  k ] ] ) ] ≈ k ]  
    --  A [ α f g o β f g h ] ≈ h
    β : { d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A d a ) → Hom A d c
    β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 
@@ -48,6 +48,17 @@
 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 {
@@ -57,7 +68,7 @@
       b1 = ef=eg (eqa f g) ;
       b2 = lemma-equ5 ;
       b3 = lemma-equ3 ;
-      b4 = {!!} 
+      b4 = lemma-equ6 
  } where
      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
@@ -65,7 +76,7 @@
      lemma-equ3 = let open ≈-Reasoning (A) in
              begin  
                   e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
-             ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩
+             ≈⟨ ek=h (eqa f f )  ⟩
                   id1 A a
              ∎
      lemma-equ4 :  {a b c d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → 
@@ -85,12 +96,39 @@
                     ≈ A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ]
      lemma-equ5 {d} {h} = let open ≈-Reasoning (A) in
              begin
-                    e (eqa f g) o k (eqa f g) (h o e (eqa (f o h) (g o h))) (lemma-equ4 f g h) 
-             ≈⟨ ke=h (eqa f g) (lemma-equ4 f g h) ⟩
+                    e (eqa f g) o k (eqa f g) (h o e (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h) 
+             ≈⟨ ek=h (eqa f g)  ⟩
                     h o e (eqa (f o h ) ( g o h ))
              ∎
+     lemma-equ6 : {d : Obj A} {k₁ : Hom A d c} → A [ 
+          A [ k (eqa f g) (A [ A [ e (eqa f g) o k₁ ] o e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ g o A [ e (eqa f g) o k₁ ] ])) ])
+                     (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o k₁ ])) o 
+              k (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ f o A [ e (eqa f g) o k₁ ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o k₁ ] ])) ]
+              ≈ k₁ ]
+     lemma-equ6 {d} {k₁} = let open ≈-Reasoning (A) in 
+             begin
+                     ( k (eqa f g) (( ( e (eqa f g) o k₁ ) o e (eqa (( f o ( e (eqa f g) o k₁ ) )) (( g o ( e (eqa f g) o k₁ ) ))) ))
+                            (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o k₁ ))) o
+                       k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) )
+             ≈⟨ car ( uniqueness (eqa f g) ( begin
+                   e (eqa f g) o  k₁ 
+                ≈⟨ {!!} ⟩
+                   (e (eqa f g) o k₁) o e (eqa (f o e (eqa f g) o k₁) (g o e (eqa f g) o k₁))
+             ∎ ))  ⟩
+                    k₁ o  k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) 
+             ≈⟨ cdr ( uniqueness (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) ( begin
+                  e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁)) o id1 A d
+                ≈⟨ {!!} ⟩
+                 id1 A d
+             ∎ ))  ⟩
+                    k₁  o  id1 A d
+             ≈⟨ idR ⟩
+                    k₁
+             ∎
 
 
 
 
 
+
+