Mercurial > hg > Members > kono > Proof > category

changeset 259:c442322d22b3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add figure
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 17 Sep 2013 11:27:57 +0900
parents 281b8962abbe
children a87d3ea9efe4
files equalizer.agda
diffstat 1 files changed, 19 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 16 17:26:42 2013 +0900
+++ b/equalizer.agda	Tue Sep 17 11:27:57 2013 +0900
@@ -86,6 +86,13 @@
 --
 --     e i = e j → i = j
 --
+--           e eqa f g        f
+--         c ----------> a ------->b
+--        ^^
+--        ||
+--       i||j
+--        ||
+--         d
 
 monoic : { c a b d : Obj A } {f g : Hom A a b } → {e : Hom A c a } ( eqa : Equalizer A e f g) 
       →  { i j : Hom A d c }
@@ -109,7 +116,7 @@
 --------------------------------
 --
 --
---   An isomorphic arrow c' to c makes another equalizer
+--   Isomorphic arrows from c' to c makes another equalizer
 --
 --           e eqa f g        f
 --         c ----------> a ------->b
@@ -177,7 +184,17 @@
 --     h : c → c'  h' : c' → c
 --     e' = h   o e
 --     e  = h'  o e'
---         we assume equalizer on fe,ge and fe',ge'
+--
+--
+--
+--           e eqa f g        f
+--         c ---------->a ------->b
+--         ^            ^     g
+--         |            |
+--         |k = id c'   |
+--         v            |
+--         c'-----------+
+--           e eqa' f g
 
 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } →  {e : Hom A c a } { e' : Hom A c' a }
        ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )