--- a/equalizer.agda	Mon Sep 02 00:12:32 2013 +0900
+++ b/equalizer.agda	Mon Sep 02 16:54:02 2013 +0900
@@ -21,7 +21,7 @@
 open import HomReasoning
 open import cat-utility
 
-record Equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
       equalizer : {c d : Obj A} (f' : Hom  A c a) (g' : Hom A d a) →  Hom A c d 
       equalize : {c d : Obj A} (f' : Hom  A c a) (g' : Hom A d a) →
@@ -29,14 +29,27 @@
       uniqueness : {c d : Obj A} (f' : Hom  A c a) (g' : Hom A d a) ( e : Hom A c d ) → 
            A [ A [ f  o  f' ]  ≈ A [  A [ g  o g' ] o e ] ] → A [ e  ≈ equalizer f' g' ]
 
-record EqEqualizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
-      α : {d a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  Hom A d a
-      γ : {d c : Obj A}  → (f : Hom A c b) → (g : Hom A c b ) → (h : Hom A d c ) →  Hom A d c 
-      δ : {a b : Obj A}  → (f : Hom A a b) → Hom A a a 
-      β : {c a b d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  (h : Hom A c d ) → Hom A c a
-      b1 :  {c : Obj A} → A [ A [ f  o α {c} f g ] ≈ A [ g  o α {c} f g ] ]
-      b2 :  {c d : Obj A } → {h : Hom A d a } → A [ A [ α f g o γ f g h ] ≈ A [ h  o α  (A [ f o h ]) (A [ g o h ]) ] ]
-      b3 :  A [ A [ α f f o δ f ] ≈ id1 A a ]
-      b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
-      b5 :  {c d : Obj A } → {h : Hom A d a } → A [ β f g h ≈  A [ γ f g h o δ (A [ f o h ]) ] ]
+      α : {e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) →  Hom A e a
+      γ : {c d e a b : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c e 
+      δ : {e a b : Obj A}  → (f : Hom A a b) → Hom A a e 
+      b1 :  {e : Obj A} → A [ A [ f  o α {e} f g ] ≈ A [ g  o α {e} f g ] ]
+      b2 :  {c d : Obj A } → {h : Hom A d a } → A [ A [ α {c} f g o γ {c} f g h ] ≈ A [ h  o α  (A [ f o h ]) (A [ g o h ]) ] ]
+      b3 :  {e : Obj A} → A [ A [ α {e} f f o δ {e} f ] ≈ id1 A a ]
+      -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
+      b4 :  {c d : Obj A } {k : Hom A c a} → A [ A [ γ f g ( A [ α f g o  k ] ) o δ {c} (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 e
+   β {d} f g h =  A [ γ f g h o δ {d} (A [ f o h ]) ] 
+
+lemma-equ1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b)  → Equalizer A f g → EqEqualizer A f g
+lemma-equ1  A {a} {b} f g eqa = record {
+      α = {!!} ;
+      γ = {!!} ;
+      δ = {!!} ;
+      b1 = {!!} ;
+      b2 = {!!} ;
+      b3 = {!!} ;
+      b4 = {!!} 
+ }