# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378109594 -32400
# Node ID a1e5d2a3d3bdccd1176778952c03604ab5a853ba
# Parent  22811f7a04e1d6302d47017af012df1fd338ba71
fix

diff -r 22811f7a04e1 -r a1e5d2a3d3bd equalizer.agda
--- a/equalizer.agda	Mon Sep 02 16:54:02 2013 +0900
+++ b/equalizer.agda	Mon Sep 02 17:13:14 2013 +0900
@@ -2,12 +2,12 @@
 --
 --  Equalizer
 --
---         f'            f
+--         e             f
 --    c  --------> a ----------> b
---    |        .     ---------->
+--    ^        .     ---------->
 --    |      .            g
---    |h   .                
---    v  .  g'            
+--    |k   .                
+--    |  . h              
 --    d 
 --
 --                        Shinji KONO <kono@ie.u-ryukyu.ac.jp>
@@ -23,11 +23,11 @@
 
 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' ]
+      equalizer : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) →  Hom A d c 
+      equalize : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) →
+           A [ A [ A [ f  o  e ] o equalizer e h ]  ≈ A [ g  o h ] ]
+      uniqueness : {c d : Obj A} (e : Hom  A c a) (h : Hom A d a) ( k : Hom A d c ) → 
+           A [ A [ A [ f  o  e ] o k ]  ≈ A [ g  o h ] ] → A [ equalizer e h  ≈ k ]
 
 record EqEqualizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A} (f g : Hom A a b) : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
    field