--- a/equalizer.agda	Tue Sep 03 01:25:21 2013 +0900
+++ b/equalizer.agda	Tue Sep 03 02:38:23 2013 +0900
@@ -26,24 +26,24 @@
       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 } → A [ A [ e  o k' ] ≈ h ] →
-                       A [ k {d} h eq  ≈ k' ]
+      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
 
 record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field
       α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  Hom A c a
-      γ : {a b d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A c d
+      γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c
       δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c 
       b1 : A [ A [ f  o α {a} {b} {a}  f g ] ≈ A [ g  o α f g ] ]
-      b2 :  {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 ]) ] ]
+      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 [ γ f g ( A [ α f g o  k ] ) o δ (A [ f o A [ α f g o  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
    --  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 a d
---   β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {d} f g h o δ (A [ f o 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 ]) ] 
 
 open Equalizer
 open EqEqualizer
@@ -52,7 +52,7 @@
          ( {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
-      γ = λ {a} {b} {d} f g h → ( k (eqa f g ) ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) ) ;  -- Hom A c d
+      γ = λ {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) ;
       b2 = lemma-equ5 ;
@@ -68,9 +68,9 @@
              ≈⟨ ke=h (eqa f f ) (lemma-equ2 f) ⟩
                   id1 A a
              ∎
-     lemma-equ4 :  {a b d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → 
+     lemma-equ4 :  {a b c d : Obj A}  → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → 
                       A [ A [ f o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ]
-     lemma-equ4 {a} {b} {d} f g h  = let open ≈-Reasoning (A) in
+     lemma-equ4 {a} {b} {c} {d} f g h  = let open ≈-Reasoning (A) in
              begin
                    f o ( h o e (eqa (f o h) ( g o h )))
              ≈⟨ assoc ⟩
@@ -81,7 +81,7 @@
                    g o ( h o e (eqa (f o h) ( g o h )))
              ∎
      lemma-equ5 :  {d : Obj A} {h : Hom A d a} → A [ 
-                      A [ e (eqa f g) o k (eqa f g) (A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 f g h) ]
+                      A [ e (eqa f g) o k (eqa f g) (A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
                     ≈ A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ]
      lemma-equ5 {d} {h} = let open ≈-Reasoning (A) in
              begin