--- a/equalizer.agda	Tue Sep 17 11:27:57 2013 +0900
+++ b/equalizer.agda	Fri Sep 20 15:39:50 2013 +0900
@@ -20,15 +20,16 @@
 open import HomReasoning
 open import cat-utility
 
-record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
-   field
-      fe=ge : 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
-      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
+-- in cat-utility
+-- record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+--    field
+--       fe=ge : 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
+--       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
 
 
 --