Mercurial > hg > Members > kono > Proof > category

changeset 31:17b8bafebad7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add universal mapping
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 14:30:27 +0900
parents 98b8431a419b
children 7862ad3b000f
files CatReasoning.agda category.ind nat.agda universal-mapping.agda
diffstat 4 files changed, 394 insertions(+), 367 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CatReasoning.agda	Mon Jul 22 14:30:27 2013 +0900
@@ -0,0 +1,116 @@
+module CatReasoning  where 
+
+-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
+open import Category -- https://github.com/konn/category-agda
+open import Level
+open Functor
+
+
+--        F(f)
+--   F(a) ---→ F(b)
+--    |          |
+--    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
+--    |          |
+--    v          v
+--   G(a) ---→ G(b)
+--        G(f)
+
+record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
+                 ( F G : Functor D C )
+                 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+  field
+    naturality : {a b : Obj D} {f : Hom D a b} 
+      → C [ C [ (  FMap G f ) o  ( TMap a ) ]  ≈ C [ (TMap b ) o  (FMap F f)  ] ]
+
+record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
+       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+  field
+    TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
+    isNTrans : IsNTrans domain codomain F G TMap
+
+
+
+module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
+  open import Relation.Binary.Core 
+
+  _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
+  x o y = A [ x o y ]
+
+  _≈_ :  {a b : Obj A }   → Rel (Hom A a b) ℓ
+  x ≈ y = A [ x ≈ y ]
+
+  infixr 9 _o_
+  infix  4 _≈_
+
+  refl-hom :   {a b : Obj A } { x : Hom A a b }  →  x ≈ x 
+  refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
+
+  trans-hom :   {a b : Obj A } { x y z : Hom A a b }  →
+         x ≈ y →  y ≈ z  →  x ≈ z 
+  trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
+
+  -- some short cuts
+
+  car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
+          x ≈ y  → ( x o f ) ≈ ( y  o f )
+  car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+
+  cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
+          x ≈ y  →  f o x  ≈  f  o y 
+  cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
+
+  id :  (a  : Obj A ) →  Hom A a a
+  id a =  (Id {_} {_} {_} {A} a) 
+
+  idL :  {a b : Obj A } { f : Hom A b a } →  id a o f  ≈ f 
+  idL =  IsCategory.identityL (Category.isCategory A)
+
+  idR :  {a b : Obj A } { f : Hom A a b } →  f o id a  ≈ f 
+  idR =  IsCategory.identityR (Category.isCategory A)
+
+  sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
+  sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
+
+  assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
+                                  →  f o ( g o h )  ≈ ( f o g ) o h
+  assoc =  IsCategory.associative (Category.isCategory A)
+
+  distr :  (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
+     →   FMap T ( g o f  )  ≈  FMap T g o FMap T f 
+  distr T = IsFunctor.distr ( isFunctor T )
+
+  open NTrans 
+  nat : { c₁′ c₂′ ℓ′ : Level}  (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
+      →  (η : NTrans D A F G )
+      →   FMap G f  o  TMap η a   ≈ TMap η b  o  FMap F f
+  nat _ η  =  IsNTrans.naturality ( isNTrans η  )
+
+
+  infixr  2 _∎
+  infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
+  infix  1 begin_
+
+------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
+--  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  → A [ x ≈  y ] → x ≡ y
+--  ≈-to-≡ refl-hom = refl
+
+  data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
+                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
+      relTo : (x≈y : x ≈ y ) → x IsRelatedTo y
+
+  begin_ : { a b : Obj A } { x y : Hom A a b } →
+           x IsRelatedTo y → x ≈ y 
+  begin relTo x≈y = x≈y
+
+  _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
+           x ≈ y → y IsRelatedTo z → x IsRelatedTo z
+  _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
+
+  _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
+  _ ≈⟨⟩ x∼y = x∼y
+
+  _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
+  _∎ _ = relTo refl-hom
+
--- a/category.ind	Sat Jul 13 18:12:57 2013 +0900
+++ b/category.ind	Mon Jul 22 14:30:27 2013 +0900
@@ -12,28 +12,28 @@
 
 $f: a -> Ub $
 
---begin-comment:
-                           FU(b)
-                         ・   |
-                      ・      |
-              F(f) ・         |
-                ・         ε(b)
-             ・               |
-         ・      f*           v
-      F(a) -----------------> b
+----begin-comment:
+                       FU(b)
+                     ・   |
+                  ・      |
+          F(f) ・         |
+            ・         ε(b)
+         ・               |
+     ・      f*           v
+  F(a) -----------------> b
 
-                U(f*)
-     UF(a) -----------------> Ub
-       ^                    ・
-       |                 ・
-       |              ・
-    η(a)          ・  f
-       |       ・
-       |    ・    f = U(f*)η
-       |・
-       a
+            U(f*)
+ UF(a) -----------------> Ub
+   ^                    ・
+   |                 ・
+   |              ・
+η(a)          ・  f
+   |       ・
+   |    ・    f = U(f*)η
+   |・
+   a
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 \mbox{}                                      & FU(b) \arrow{d}{ε(b)}           \\
@@ -88,16 +88,16 @@
 
 because of naturality of $η$
 
---begin-comment:
-           η(a)
-   UF(a) <------- a    UF(f)η(a) = η(b)f 
-    |             |
-    |UF(f)       f|
-    v             v
-   UF(b) <------- b             
-           η(b)
+----begin-comment:
+       η(a)
+UF(a) <------- a    UF(f)η(a) = η(b)f 
+|             |
+|UF(f)       f|
+v             v
+UF(b) <------- b             
+       η(b)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UF(a) \arrow[leftarrow]{r}{η(a)} \arrow{d}{UF(f)} & a \arrow{d}{f} &  UF(f)η(a) = η(b)f \\
@@ -111,23 +111,23 @@
 
 $   Uε○ηU = 1_U $
 
---begin-comment:
-           F(f)              ε(b)
-    F(a) ---------> FU(b)  -------->  b
+----begin-comment:
+       F(f)              ε(b)
+F(a) ---------> FU(b)  -------->  b
 
-          UF(f)             U(ε(b))
-   UF(a) --------> UFU(b)  --------> U(b)
+      UF(f)             U(ε(b))
+UF(a) --------> UFU(b)  --------> U(b)
 
-          η(a)              UF(f)            U(ε(b))
-    a  --------->   UF(a) --------> UFU(b)  --------> U(b)
+      η(a)              UF(f)            U(ε(b))
+a  --------->   UF(a) --------> UFU(b)  --------> U(b)
 
-           f                η(Ub)            U(ε(b))
-    a  --------->   Ub    --------> UFU(b)  --------> U(b)
+       f                η(Ub)            U(ε(b))
+a  --------->   Ub    --------> UFU(b)  --------> U(b)
 
-                            η(Ub)            U(ε(b))  = 1
-                                  ∵   Uε○ηU = 1_U
+                        η(Ub)            U(ε(b))  = 1
+                              ∵   Uε○ηU = 1_U
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 F(a) \arrow{r}{F(f)} & FU(b) \arrow{r}{ε(b)} & b & \\
@@ -141,34 +141,34 @@
 
 naturality of $f:a->Ub$
 
---begin-comment:
+----begin-comment:
 
-          η(Ub)
-   Ub  --------->   UF(Ub) 
-    ^                ^
-    |                |
-   f|                |UF(f)
-    |     η(a)       |
-    a  --------->   UF(a) 
+      η(Ub)
+Ub  --------->   UF(Ub) 
+^                ^
+|                |
+f|                |UF(f)
+|     η(a)       |
+a  --------->   UF(a) 
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 Ub  \arrow{r}{η(Ub)} &   UF(Ub)  \\
 a \arrow{u}{f} \arrow{r}{η(a)} & UF(a) \arrow{u}[swap]{UF(f)}
 \end{tikzcd}
 
---begin-comment:
+----begin-comment:
 
-           UF(f)   
-   UF(a) ------------->UF(U(b))    UF(U(b))
-    ^                  ^             |
-    |                  |             |
+       UF(f)   
+UF(a) ------------->UF(U(b))    UF(U(b))
+^                  ^             |
+|                  |             |
 η(a)|           η(U(b))|             |U(ε(U(b)))
-    |        f         |             v
-    a  --------------->U(b)         U(b) 
+|        f         |             v
+a  --------------->U(b)         U(b) 
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UF(a) \arrow{r}{UF(f)} & UF(U(b)) & UF(U(b)) \arrow{d}{U(ε(U(b)))} & \mbox{} \\
@@ -177,17 +177,17 @@
 
 Solution of universal mapping yields naturality of $Uε○ηU = 1_U$.
 
---begin-comment:
+----begin-comment:
 
-                               F(η(a)) 
-   UF(a)               F(a) ----------> FUF(a)
-    ^                                   |
-    |                                   |
+                           F(η(a)) 
+UF(a)               F(a) ----------> FUF(a)
+^                                   |
+|                                   |
 η(a)|                                   |ε(F(a))
-    |       η(a)                        v
-    a  --------------->UF(a)            F(a)
+|       η(a)                        v
+a  --------------->UF(a)            F(a)
 
---end-comment:
+----end-comment:
 
 $εF○Fη = 1_F$.
 
@@ -209,21 +209,21 @@
 \[ ε : FU -> 1_B        \]
 \[  ε(b) = (1_{U(b)})* \]
 
---begin-comment:
-                 f*
-      F(a) -----------------> b
+----begin-comment:
+             f*
+  F(a) -----------------> b
 
-                U(f*)
-     UF(a) -----------------> Ub
-       ^                    ・
-       |                 ・
-       |              ・
-    η(a)          ・  f
-       |       ・
-       |    ・    f = U(f*)η
-       |・
-       a
---end-comment:
+            U(f*)
+ UF(a) -----------------> Ub
+   ^                    ・
+   |                 ・
+   |              ・
+η(a)          ・  f
+   |       ・
+   |    ・    f = U(f*)η
+   |・
+   a
+----end-comment:
 
 \begin{tikzcd}
 F(a) \arrow{r}{f*} & b \\
@@ -252,28 +252,28 @@
 definition of $ε$ 
 \[  ε(b) = (1_{U(b)})* \] 
 
---begin-comment:
+----begin-comment:
 
-                   FU(f*) 
-          FUF(a)------------->FU(b)      
-           ^|                   |      
-           ||ε(F(a))            |       
-    F(η(a))||                   |ε(b)=(1_U(b))*  
-           ||   (η(Ub)f)*=F(f)  |               
-           |v                   v              
-           F(a) --------------->b              
-                     f*
-                   UF(f) 
-           UF(a)------------->UFU(b)           
-            ^                  ^|  
-            |       U(f*)      ||   
-        η(a)|           η(U(b))||U(ε(b))  
-            |                  ||  
-            |                  |v  
-            a  --------------->U(b) 
-                     f
+               FU(f*) 
+      FUF(a)------------->FU(b)      
+       ^|                   |      
+       ||ε(F(a))            |       
+F(η(a))||                   |ε(b)=(1_U(b))*  
+       ||   (η(Ub)f)*=F(f)  |               
+       |v                   v              
+       F(a) --------------->b              
+                 f*
+               UF(f) 
+       UF(a)------------->UFU(b)           
+        ^                  ^|  
+        |       U(f*)      ||   
+    η(a)|           η(U(b))||U(ε(b))  
+        |                  ||  
+        |                  |v  
+        a  --------------->U(b) 
+                 f
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUF(a) \arrow{r}{FU(f*)} \arrow{d}{ε(F(a))} & FU(b) \arrow{d}{ε(b)=(1_U(b))*} & \mbox{} \\
@@ -288,19 +288,19 @@
 $ ε(F(a)) = (1_{UF(a)})* $
 
 
---begin-comment:
+----begin-comment:
 
-                                F(η(a))
-    UF(a)              F(a) --------------> FUF(a)
-     ^                                      |^
-     |                                      ||
- η(a)|    U(1_{F(a)})     1_{F(a)}   ε(F(a))||F(η(a))
-     |                                      ||
-     |                                      v|
-     a ---------------> U(F(a))            F(a)
-            η(a)
+                            F(η(a))
+UF(a)              F(a) --------------> FUF(a)
+ ^                                      |^
+ |                                      ||
+η(a)|    U(1_{F(a)})     1_{F(a)}   ε(F(a))||F(η(a))
+ |                                      ||
+ |                                      v|
+ a ---------------> U(F(a))            F(a)
+        η(a)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UF(a) \arrow{rd}{U(1_{F(a)}) } & F(a) \arrow{r}{F(η(a))} \arrow{rd}[swap]{1_{F(a)}} & FUF(a) \arrow{d}[swap]{ε(F(a))} & \mbox{} \\
@@ -321,10 +321,10 @@
 show $F(fg) = F(f)F(g)$
 
 
---begin-comment:
-      g        f
- a -----> Ub ----> UUc
---end-comment:
+----begin-comment:
+  g        f
+a -----> Ub ----> UUc
+----end-comment:
 
 \begin{tikzcd}
 a \arrow{r}{g} &  Ub \arrow{r}{f} &  UUc
@@ -349,28 +349,28 @@
 \end{eqnarray*}
 \mbox{Q.E.D.}
 
---begin-comment:
-                                    FU(f)
-                           FU(b) -------------> FUU(c)
-                         ・   |                  |
-                      ・      |                  |
-              F(g) ・         |                  |
-                ・         ε(b)            ε(Uc) |
-             ・               |                  |
-         ・      g*           v       f*         v
-      F(a) -----------------> b ---------------> c
+----begin-comment:
+                                FU(f)
+                       FU(b) -------------> FUU(c)
+                     ・   |                  |
+                  ・      |                  |
+          F(g) ・         |                  |
+            ・         ε(b)            ε(Uc) |
+         ・               |                  |
+     ・      g*           v       f*         v
+  F(a) -----------------> b ---------------> c
 
-                                   U(F(f))
-     UF(a)                  UFUb 
-       ^ ・                   ^ ・  
-       |     ・               |    ・ 
-       |        ・            |      ・
-    η(a)           ・ UFg     |         ・ UFf
-       |              ・      η(Ub)       ・ 
-       |                ・    |              ・ 
-       |       g           ・ |          f     ・
-       a  -----------------> Ub ---------------> UU(c)
---end-comment:
+                               U(F(f))
+ UF(a)                  UFUb 
+   ^ ・                   ^ ・  
+   |     ・               |    ・ 
+   |        ・            |      ・
+η(a)           ・ UFg     |         ・ UFf
+   |              ・      η(Ub)       ・ 
+   |                ・    |              ・ 
+   |       g           ・ |          f     ・
+   a  -----------------> Ub ---------------> UU(c)
+----end-comment:
 
 
 \begin{tikzcd}
@@ -385,17 +385,17 @@
 
 $  η: 1->UB $
 
---begin-comment:
+----begin-comment:
 
-     UF(a)-----------------> UFb 
-       ^      UF(f)           ^
-       |                      |
-       |                      |
-    η(a)                      η(b)
-       |                      |
-       |         f            | 
-       a  ----------------->  b
---end-comment:
+ UF(a)-----------------> UFb 
+   ^      UF(f)           ^
+   |                      |
+   |                      |
+η(a)                      η(b)
+   |                      |
+   |         f            | 
+   a  ----------------->  b
+----end-comment:
 
 \begin{tikzcd}
 UF(a) \arrow{r}[swap]{UF(f)} &  UFb  \\
@@ -426,16 +426,16 @@
 $    U(ε(b))η(U(b))U(b) = U(b)$
 
 
---begin-comment:
-            FU(f)
-   FU(b) -------------> FU(c)
-     |                  |
-     |                  |
-  ε(b)                  | ε(c)
-     |                  |
-     v       f          v
-     b ---------------> c
---end-comment:
+----begin-comment:
+        FU(f)
+FU(b) -------------> FU(c)
+ |                  |
+ |                  |
+ε(b)                  | ε(c)
+ |                  |
+ v       f          v
+ b ---------------> c
+----end-comment:
 
 \begin{tikzcd}
 FU(b) \arrow{r}{FU(f)} \arrow{d}{ε(b)} & FU(c) \arrow{d}{ε(c)}\\
@@ -447,28 +447,28 @@
 
 \[       f = Ub -> Uc \]
 
---begin-comment:
+----begin-comment:
 
-                 FU(f)              (1_U(c))*
-      F(Ub) --------------> FU(c)  ---------------> c
+             FU(f)              (1_U(c))*
+  F(Ub) --------------> FU(c)  ---------------> c
 
-                 (1_U(b))*              f
-      F(Ub) ----------------> b  -----------------> c
+             (1_U(b))*              f
+  F(Ub) ----------------> b  -----------------> c
 
-                U(1_U(b)*)             U(f)
-     UF(Ub) ----------------> Ub -----------------> U(c)
-       ||                   ・                       ||
-       ||                ・                          ||
-       ||    UFU(f)   ・            U(1_U(c)*)       ||
-     UF(Ub) ----- ・ ------>  UFUc ---------------> U(c) 
-       ^       ・             ^                      ||
-       |     ・               |                      ||
-    η(Ub) ・   1_Ub     η(Uc) |                      ||
-       |・                    |        1_Uc          ||
-       Ub ------------------> Uc -----------------> U(c)
-                U(f)
+            U(1_U(b)*)             U(f)
+ UF(Ub) ----------------> Ub -----------------> U(c)
+   ||                   ・                       ||
+   ||                ・                          ||
+   ||    UFU(f)   ・            U(1_U(c)*)       ||
+ UF(Ub) ----- ・ ------>  UFUc ---------------> U(c) 
+   ^       ・             ^                      ||
+   |     ・               |                      ||
+η(Ub) ・   1_Ub     η(Uc) |                      ||
+   |・                    |        1_Uc          ||
+   Ub ------------------> Uc -----------------> U(c)
+            U(f)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 F(Ub) \arrow{r}{(1_{U(b)})*} &  b \arrow{r}{f}  &  c  \\
@@ -478,7 +478,7 @@
 F(Ub) \arrow{r}{FU(f)} &  FU(c)  \arrow{r}{(1_{U(c)})*} &  c \\
 \end{tikzcd}
 
---begin-comment:
+----begin-comment:
 
 \begin{tikzcd}
 \mbox{} & Ub \arrow{r}{U(f)} & U(c) \\
@@ -493,7 +493,7 @@
 Ub \arrow{r}{U(f)} \arrow{u}{1_Ub} \arrow[bend left]{uu}{η(Ub)} &  Uc \arrow{u}[swap]{1_Uc} \arrow[bend right]{uu}[swap]{η(Uc)} 
 \end{tikzcd}
 
---end-comment:
+----end-comment:
 
 
 show $ε(c)FU(f)$ and $fε(b)$ are both solution of $(1_{Uc})U(f) ( = U(f)(1_{Ub}))$
@@ -522,15 +522,15 @@
 
 end of proof.
 
---begin-comment:
-                           U(f*)
-    c              U(c) <- ----------- U(b)             b   
-    ^              ^|                  |^             ^
-    |       U(ε(c))||η(U(c))    η(U(b))||U(ε(b))      |
-    |ε(c)          ||                  ||         ε(b)|
-    |              |v      UFU(f)      v|             |
-   FU(c)         UFU(c) <----------- UFU(b)           FU(b)
---end-comment:
+----begin-comment:
+                       U(f*)
+c              U(c) <- ----------- U(b)             b   
+^              ^|                  |^             ^
+|       U(ε(c))||η(U(c))    η(U(b))||U(ε(b))      |
+|ε(c)          ||                  ||         ε(b)|
+|              |v      UFU(f)      v|             |
+FU(c)         UFU(c) <----------- UFU(b)           FU(b)
+----end-comment:
 
 \begin{tikzcd}
 c       \arrow[bend left,leftarrow]{rrr}{f}
@@ -579,17 +579,17 @@
 
 \[       ε(F(a))Fη(a) = 1_F(a) \]
 
---begin-comment:
+----begin-comment:
 
-            F                U
-   UF(a) --------> FUF(a) ----------> UFUF(a)         FUF(a)
-    ^               ^|                 |^              ^|
-    |               ||                 ||              ||
-    |η(a)    F(η(a))||ε(F(a))  U(εF(a))||η(UF(a))      ||ε(F(a))
-    |               ||                 ||              ||
-    |       F       |v       U         v|              |v
-    a ------------> F(a) ------------> UF(a)           F(a)
---end-comment:
+        F                U
+UF(a) --------> FUF(a) ----------> UFUF(a)         FUF(a)
+^               ^|                 |^              ^|
+|               ||                 ||              ||
+|η(a)    F(η(a))||ε(F(a))  U(εF(a))||η(UF(a))      ||ε(F(a))
+|               ||                 ||              ||
+|       F       |v       U         v|              |v
+a ------------> F(a) ------------> UF(a)           F(a)
+----end-comment:
 
 
 \begin{tikzcd}
@@ -603,7 +603,7 @@
 a \arrow{r}{F} \arrow{u}[swap]{η(a)} & F(a) \arrow{r}{U} \arrow[bend left]{u}{F(η(a))} & UF(a) \arrow[bend right]{u}[swap]{η(UF(a))} & F(a) \arrow{u}{} & \mbox{} \\
 \end{tikzcd}
 
---begin-comment:
+----begin-comment:
                
             UUF(a) 
             ^ |   
@@ -611,7 +611,7 @@
     η(UF(a))| |U(ε(Fa))    U(ε(F(a))η(UF(a)) = 1_UF(a)
             | v              ε(F(a) = (1_UF(a))*
             UF(a) 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UUF(a)  \arrow[bend left]{d}{U(ε(Fa))} \\
@@ -621,13 +621,13 @@
 $ ε(F(a)) = (1_UF(a))* $
 
 
---begin-comment:
+----begin-comment:
     FA -------->UFA
      |          |
      | Fη(A)    | UFηA
      v          v
     FUFA ------>UFUFA
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FA    \arrow{r} \arrow{d}{Fη(A)} &     UFA \arrow{d}{UFηA} \\
@@ -655,7 +655,7 @@
 --おまけ
 
 $ εF○Fη=1_F, Uε○ηU = 1_U $ 
---begin-comment:
+----begin-comment:
 
                     U                             
        UFU(a) <--------------- FU(a)
@@ -673,7 +673,7 @@
         F(a) <----------------  (a)
                     F   
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UFU(a) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(a))} & FU(a) \arrow{d}{ε(a)} & \mbox{} \\
@@ -686,7 +686,7 @@
 
 なら、 $ FU(ε(F(a))) = εF(a) $ ?
 
---begin-comment:
+----begin-comment:
                         U                             
            UFU(F(a)) <--------------- FU(F(a))
             ^|                         |
@@ -710,7 +710,7 @@
             |v                      |
             F(a) <----------------  (a)
                         F   
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UFU(F(a)) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\
@@ -735,7 +735,7 @@
 
 $  μ○μT  = μ○Tμ $      association law
 
---begin-comment:
+----begin-comment:
          Tη                      μT
    T ---------> T^2        T^3---------> T^2
    |・          |           |            |
@@ -745,7 +745,7 @@
    v         ・ v           v            v
    T^2 -------> T          T^2 --------> T
          μ                        μ
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 T \arrow{r}{Tη} \arrow{d}[swap]{ηT} \arrow{rd}{1_T} & T^2 \arrow{d}{μ} & T^3 \arrow{r}{μT} \arrow{d}[swap]{Tμ}& T^2 \arrow{d}{μ} & \mbox{} \\
@@ -772,7 +772,7 @@
 & = &  U(ε(F(b))F(η(b)))   =   U(1_F)    \\
 \end{eqnarray*}
 
---begin-comment:
+----begin-comment:
 
             UεFUF                       εFUF                    ε(a)
      UFUFUF-------> UFUF          FUFUF-------> FUF       FU(a)---------->a 
@@ -784,7 +784,7 @@
      UFUF --------> UF             FUF --------> F        FU(b)---------> b
             UεF                           εF                    ε(b)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 UFUFUF \arrow{r}{UεFUF} \arrow{d}[swap]{UFUεF} & UFUF \arrow{d}{UεF} & FUFUF \arrow{r}{εFUF} \arrow{d}[swap]{FUεF} & FUF \arrow{d}{εF} & FU(a) \arrow{r}{ε(a)} \arrow{d}[swap]{FU(f)} & a \arrow{d}[swap]{f} & \mbox{} \\
@@ -813,7 +813,7 @@
 UεF○FUUεF & = UεF○UεFFU \\
 \end{eqnarray*}
 
---begin-comment:
+----begin-comment:
 
           FU(ε(F(a)))
  FUF(a) <-------------FUFUF(a)
@@ -824,7 +824,7 @@
    F(a) <------------- FUF(a)
             ε(F(a))
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUF(a) \arrow[leftarrow]{r}{FU(ε(F(a)))} \arrow{d}{ε(F(a))} & FUFUF(a) \arrow{d}{ε(FUF(a))} & \mbox{} \\
@@ -844,7 +844,7 @@
 $ φT(f) = fφ $
 
 
---begin-comment:
+----begin-comment:
 
            η(a)                         μ(a)                     T(f)
       a-----------> T(a)         T^2(a)--------> T(a)     T(a)---------->T(b) 
@@ -856,7 +856,7 @@
       _             a              T(a)-------->T(a)       a------------> b
                                           φ                      f   
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 a \arrow{r}{η(a)} \arrow{rd}{1_a} & T(a) \arrow{d}{φ} & T^2(a) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & T(a) \arrow{d}{φ} & T(a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & T(b) \arrow{d}{φ'} & \mbox{} \\
@@ -875,7 +875,7 @@
 
 $φ: (m,a) -> φ(m,a) = ma $
 
---begin-comment:
+----begin-comment:
 
            η(a)                         μ(a)                     T(f)
       a----------->(1,a)     (m,(m',a))-----> (mm',a)   (m,a)----------->(m,f(a))
@@ -886,7 +886,7 @@
                     v               v            v         v              v
       _            1a           (m,m'a)-------->mm'a      ma------------> mf(a)=f(ma)
                                           φ                      f   
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 a \arrow{r}{η(a)} \arrow{rd}{1_a} & (1,a) \arrow{d}{φ} & (m,(m',a)) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & (mm',a) \arrow{d}{φ} & (m,a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & (m,f(a)) \arrow{d}{φ'} & \mbox{} \\
@@ -921,7 +921,7 @@
 
 $   ηU(a,φ) = η(a), Uε(a,φ) = ε^TK^T(b) = Uε(b) $
 
---begin-comment:
+----begin-comment:
 
 
      _             Ba            _
@@ -937,7 +937,7 @@
         <---------    <--------
             F_T         U^T
 
---end-comment:
+----end-comment:
 
 
 \begin{tikzcd}
@@ -970,7 +970,7 @@
 
 naturality of $μ$
 
---begin-comment:
+----begin-comment:
 
                                                        μ(c)                  T(f)             h
 f*h     _             _                     T(c) <---------------- T^2(c) <------- T(b) <----------- a
@@ -1005,7 +1005,7 @@
 
 
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 f*h & \mbox{} & \mbox{} & T(c) \arrow[leftarrow]{r}{μ(c)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\
@@ -1034,7 +1034,7 @@
 
 $ μ(d)Tμ(d)T^2(g) = μ(d)μ(T(d))T^2(g) = μ(d)T(g)μ(c) $
 
---begin-comment:
+----begin-comment:
 
               T^2(g)
     T^3(d) <----------- T^2(c)
@@ -1045,7 +1045,7 @@
      T^2(d)<------------ T(c)
                 T(g)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 T^3(d) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) & \mbox{} \\
@@ -1113,7 +1113,7 @@
 
 
 
---begin-comment:
+----begin-comment:
 
            TT(g)
     TT <--------------TT
@@ -1123,7 +1123,7 @@
      v      T(g)      v
      T<---------------T
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 TT \arrow[leftarrow]{r}{TT(g)} \arrow{d}{μ(c)} & TT \arrow{d}{μ(b)} & \mbox{} \\
@@ -1146,7 +1146,7 @@
 
 $ η(c)g = T(g)η(b) $
 
---begin-comment:
+----begin-comment:
 
             g   
      c<---------------b
@@ -1156,7 +1156,7 @@
      v      T(g)      v
     T(b)<-------------T(b)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 c \arrow[leftarrow]{r}{g} \arrow{d}{η(c)} & b \arrow{d}{η(b)} & \mbox{} \\
@@ -1211,7 +1211,7 @@
 ε(F(c))FUF(g) & = &  F(g) ε(F(b))  \\
 \end{eqnarray*}
 
---begin-comment: 
+----begin-comment: 
 
             FU(F(g))   
   FU(F(c))<-------------FU(F(b))
@@ -1221,7 +1221,7 @@
      v        F(g)       v
    F(c)<----------------F(b)
 
---end-comment: 
+----end-comment: 
 
 \begin{tikzcd}
 FU(F(c)) \arrow[leftarrow]{r}{FU(F(g))} \arrow{d}{ε(F(c))} & FU(F(b)) \arrow{d}{ε(F(b))} & \mbox{} \\
@@ -1232,7 +1232,7 @@
 
 $   ε(F(c)) F(μ(c)) = ε(F(c)) FUε(F(c)) $
 
---begin-comment: 
+----begin-comment: 
 
             FUε(F(c))   
  FUFU(c)<---------------FUFU(F(c))
@@ -1243,7 +1243,7 @@
   FU(c)<----------------FU(F(c))
 
 
---end-comment: 
+----end-comment: 
 
 \begin{tikzcd}
 FUFU(c) \arrow[leftarrow]{r}{FUε(F(c))} \arrow{d}{εF(c))} & FUFU(F(c)) \arrow{d}{ε(F(c))} & \mbox{} \\
@@ -1293,7 +1293,7 @@
 
 -- naturality of $μ$
 
---begin-comment:
+----begin-comment:
            μ(a)
    TT(a) ---------> T(a)
       |              |
@@ -1301,7 +1301,7 @@
       |              |
       v    μ(b)       v
    TT(b) ---------> T(b)
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 TT(a) \arrow{r}{μ(a)} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\
@@ -1325,7 +1325,7 @@
 
 $μ_T(a) TTT(a) = μ_T(a) (m,(m',(m'',a))) = (m*m',(m'',a)) $
 
---begin-comment:
+----begin-comment:
                μ(TTT(a))
       TTTT(a) ----------> TTT(a)
            |               |
@@ -1333,7 +1333,7 @@
            |               |
            v   μ(TT(a))    v
        TTT(a) -----------> TT(a)
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\
@@ -1358,7 +1358,7 @@
 
 Naturality of $ε$
 
---begin-comment:
+----begin-comment:
                  ε(a)
          FU(a)  ------> a
      FU(f)|             |f
@@ -1372,7 +1372,7 @@
        FUFU(b)  -----------> FU(b)
 
                            ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a)
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FU(a)  \arrow{r}{ε(a)} \arrow{d}{FU(f)} &  a \arrow{d}{f} \\
@@ -1387,13 +1387,13 @@
 
 $  ε・ε : FUFU -> 1B$
 
---begin-comment:
+----begin-comment:
                  ε(FU(a))           ε(a)
        FUFU(a)  ---------> FU(a)   ------> a
    FUFU(f)|                |FU(f)          |f
           v      ε(FU(b))  v        ε(b)   v
        FUFU(b)  ---------> FU(b)   ------> b
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)} &   FU(a) \arrow{r}{ε(a)}\arrow{d}{FU(f)} &  a\arrow{d}{f} \\
@@ -1403,7 +1403,7 @@
 
 --Horizontal Composition  $ε○ε$
 
---begin-comment:
+----begin-comment:
           FUFU  <-----  FU   <------  B
                   FU              FU
                    |               |
@@ -1411,7 +1411,7 @@
                    v               v
                   1_B             1_B
            B   <-----    B    <------  B
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUFU  \arrow[leftarrow]{rr}  & &  FU \arrow[leftarrow]{rr}  & & B \\
@@ -1424,7 +1424,7 @@
 
 $   ε○ε : FUFU -> 1_B 1_B$
 
---begin-comment:
+----begin-comment:
                  εFU(b)
      FUFU(b)  ------------> 1_AFU(b)
        |                     |
@@ -1433,7 +1433,7 @@
        v         ε(b)        v
      FU1_B(b) ------------> 1_B1_B(b)
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & 1_A \arrow{d}{1_aε(b)} & \mbox{} \\
@@ -1442,7 +1442,7 @@
 
 that is
       
---begin-comment:
+----begin-comment:
                  εFU(b)
      FUFU(b)  ------------>  FU(b)
        |                     |
@@ -1450,7 +1450,7 @@
        |                     |
        v         ε(b)        v
      FU(b)    ------------>  b
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & FU(b) \arrow{d}{ε(b)} & \mbox{} \\
@@ -1464,10 +1464,10 @@
 
 $         ε(b) : FU(b) -> b$
 
---begin-comment:
+----begin-comment:
         U          F            ε(b)
      b ----> U(b) ----> FU(b) -------> b
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 b \arrow{r}{U} & U(b) \arrow{r}{F} & FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\
@@ -1506,7 +1506,7 @@
 
 $ Hom_A((g,h)) Hom_A((g',h')) : Home_A(a,b)  -> \{h'fg' | f \in Home_A(a,b) \} -> \{hh'fgg' | f \in Home_A(a,b) \}   $
 
---begin-comment:
+----begin-comment:
 
          g'        g
      a -----> a' -----> a''
@@ -1515,7 +1515,7 @@
          h'   v    h    v
      b<-------b' <----- b''
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 a \arrow{r}{g'} & a' \arrow{r}{g} \arrow{d}{} & a'' \arrow{d}{f} & \mbox{} \\
@@ -1564,7 +1564,7 @@
 $ f^{op}: (b : A^{op}) -> (c : A^{op} )  = f : c->b $
 
 
---begin-comment:
+----begin-comment:
 
                             t(c)     
 Hom_{A^{op}}(a,c) ------------------------->Hom_{A^{op}}(a,t(c))
@@ -1577,7 +1577,7 @@
 
 
 
---end-comment:
+----end-comment:
 
 \begin{tikzcd}
 Hom_{A^{op}}(a,c) \arrow{r}{t(c)} \arrow{d}{Home^*{A^{op}}(a,f)} & Hom_{A^{op}}(a,t(c)) & \mbox{} \\
--- a/nat.agda	Sat Jul 13 18:12:57 2013 +0900
+++ b/nat.agda	Mon Jul 22 14:30:27 2013 +0900
@@ -9,39 +9,15 @@
 
 open import Category -- https://github.com/konn/category-agda
 open import Level
-open Functor
+open import Category.HomReasoning
 
 --T(g f) = T(g) T(f)
 
+open Functor
 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
      → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
 Lemma1 = \t → IsFunctor.distr ( isFunctor t )
 
---        F(f)
---   F(a) ---→ F(b)
---    |          |
---    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
---    |          |
---    v          v
---   G(a) ---→ G(b)
---        G(f)
-
-record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
-                 ( F G : Functor D C )
-                 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
-  field
-    naturality : {a b : Obj D} {f : Hom D a b} 
-      → C [ C [ (  FMap G f ) o  ( TMap a ) ]  ≈ C [ (TMap b ) o  (FMap F f)  ] ]
---    uniqness : {d : Obj D} 
---      →  C [ TMap d  ≈ TMap d ]
-
-
-record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
-       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
-  field
-    TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
-    isNTrans : IsNTrans domain codomain F G TMap
 
 open NTrans
 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
@@ -128,106 +104,12 @@
                       ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
      join c g f = A [ TMap μ c  o A [ FMap T g  o f ] ]
 
-
-
-module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
-  open import Relation.Binary.Core 
-
-  _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
-  x o y = A [ x o y ]
-
-  _≈_ :  {a b : Obj A }   → Rel (Hom A a b) ℓ
-  x ≈ y = A [ x ≈ y ]
-
-  infixr 9 _o_
-  infix  4 _≈_
-
-  refl-hom :   {a b : Obj A } { x : Hom A a b }  →  x ≈ x 
-  refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
-
-  trans-hom :   {a b : Obj A } { x y z : Hom A a b }  →
-         x ≈ y →  y ≈ z  →  x ≈ z 
-  trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
-
-  -- some short cuts
-
-  car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
-          x ≈ y  → ( x o f ) ≈ ( y  o f )
-  car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
-
-  cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
-          x ≈ y  →  f o x  ≈  f  o y 
-  cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
-
-  id :  (a  : Obj A ) →  Hom A a a
-  id a =  (Id {_} {_} {_} {A} a) 
-
-  idL :  {a b : Obj A } { f : Hom A b a } →  id a o f  ≈ f 
-  idL =  IsCategory.identityL (Category.isCategory A)
-
-  idR :  {a b : Obj A } { f : Hom A a b } →  f o id a  ≈ f 
-  idR =  IsCategory.identityR (Category.isCategory A)
-
-  sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
-  sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
-
-  assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
-                                  →  f o ( g o h )  ≈ ( f o g ) o h
-  assoc =  IsCategory.associative (Category.isCategory A)
-
-  distr :  (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
-     →   FMap T ( g o f  )  ≈  FMap T g o FMap T f 
-  distr T = IsFunctor.distr ( isFunctor T )
-
-  nat : { c₁′ c₂′ ℓ′ : Level}  (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
-      →  (η : NTrans D A F G )
-      →   FMap G f  o  TMap η a   ≈ TMap η b  o  FMap F f
-  nat _ η  =  IsNTrans.naturality ( isNTrans η  )
-
-
-  infixr  2 _∎
-  infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
-  infix  1 begin_
-
------- If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
---  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  → A [ x ≈  y ] → x ≡ y
---  ≈-to-≡ refl-hom = refl
-
-  data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
-                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
-      relTo : (x≈y : x ≈ y ) → x IsRelatedTo y
-
-  begin_ : { a b : Obj A } { x y : Hom A a b } →
-           x IsRelatedTo y → x ≈ y 
-  begin relTo x≈y = x≈y
-
-  _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
-           x ≈ y → y IsRelatedTo z → x IsRelatedTo z
-  _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
-
-  _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
-  _ ≈⟨⟩ x∼y = x∼y
-
-  _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
-  _∎ _ = relTo refl-hom
-
 lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → 
        ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ]
 lemma12 L x y =  
    let open ≈-Reasoning ( L )  in 
       begin  L [ x o y ]  ∎
 
-Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
-                 { a : Obj A } ( b : Obj A ) →
-                 ( f : Hom A a b )
-                      →  A [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
-Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) 
-  let open ≈-Reasoning (c) in 
-     begin  
-          c [ Id {_} {_} {_} {c} b o g ]
-     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
-          g
-     ∎
 
 open Kleisli
 -- η(b) ○ f = f
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/universal-mapping.agda	Mon Jul 22 14:30:27 2013 +0900
@@ -0,0 +1,29 @@
+module universal-mapping where
+
+open import Category -- https://github.com/konn/category-agda
+open import Level
+open import Category.HomReasoning
+
+open Functor
+record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Obj A -> Obj B )
+                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
+                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+   field
+       universalMapping :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
+                     A [ A [ FMap U ( f * ) o η a' ]  ≈ f ]
+
+
+record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Obj A -> Obj B )
+                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
+                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    field
+       isUniversalMapping : IsUniversalMapping A B U F η _*
+
+
+