--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/equalizer.agda	Sun Sep 01 22:10:39 2013 +0900
@@ -0,0 +1,30 @@
+---
+--
+--  Equalizer
+--
+--         f'            f
+--    c  --------> a ----------> b
+--    |        .     ---------->
+--    |      .            g
+--    |h   .                
+--    v  .  g'            
+--    d 
+--
+--                        Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+----
+
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+open import Category.Sets
+module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+
+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
+   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) →
+           A [ A [ f  o  f' ]  ≈ A [  A [ g  o g' ] o equalizer f' g' ] ]
+      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' ]