Mercurial > hg > Members > kono > Proof > category

changeset 177:63f6157a6a19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 25 Aug 2013 11:10:35 +0900
parents ae1a4f7e5203
children 6626a7cd9129
files universal-mapping.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Sun Aug 25 09:44:00 2013 +0900
+++ b/universal-mapping.agda	Sun Aug 25 11:10:35 2013 +0900
@@ -340,14 +340,14 @@
 
 --  Assuming 
 --     naturality of left (Φ)
---     f' = k* f   k*: Hom A F(a) k,
+--     k = Hom A b b' ; f' = k o f                        h Hom A a' a  ; f' = f o h
 --                        left                                               left
---    f : Hom A F(a)   b --------> f* : Hom B a U(b)      f : Hom A F(a')b --------> f* : Hom B a' U(b)
+--    f : Hom A F(a)   b --------> f* : Hom B a U(b)      f' : Hom A F(a')b -------> f'* : Hom B a' U(b)
 --       |                               |                     |                               |
 --       |k*                             |U(k*)                |F(h*)                          |h*
 --       v                               v                     v                               v
---    f': Hom A F(a)   b'--------> f* : Hom B a U(b')     f': Hom A F(a)  b --------> f* : Hom B a U(b)
---                        left
+--    f': Hom A F(a)   b'-------> f'* : Hom B a U(b')     f: Hom A F(a)  b ---------> f* : Hom B a U(b)
+--                        left                                               left
 
 record UnityOfOppsite  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )