Mercurial > hg > Members > kono > Proof > category

changeset 208:a1e5d2a3d3bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 02 Sep 2013 17:13:14 +0900
parents 22811f7a04e1
children 4e138cc953f3
files equalizer.agda
diffstat 1 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- 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