Mercurial > hg > Members > kono > Proof > category

changeset 56:83ff8d48fdca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add unitility
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jul 2013 20:47:28 +0900
parents 1716403c92c2
children c6f66c21230c
files CatReasoning.agda HomReasoning.agda cat-utility.agda nat.agda universal-mapping.agda
diffstat 5 files changed, 363 insertions(+), 199 deletions(-) [+]
line wrap: on
line diff
--- a/CatReasoning.agda	Tue Jul 23 17:34:46 2013 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-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
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/HomReasoning.agda	Wed Jul 24 20:47:28 2013 +0900
@@ -0,0 +1,129 @@
+module HomReasoning  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
+
+-- an example
+
+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
+     ∎
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cat-utility.agda	Wed Jul 24 20:47:28 2013 +0900
@@ -0,0 +1,126 @@
+module cat-utility where
+
+-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
+open import Category -- https://github.com/konn/category-agda
+open import Level
+--open import Category.HomReasoning
+open import HomReasoning
+
+open Functor
+
+id1 :   ∀{c₁ c₂ ℓ  : Level} (A : Category c₁ c₂ ℓ)  (a  : Obj A ) →  Hom A a a
+id1 A a =  (Id {_} {_} {_} {A} a)
+
+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 ]
+       uniquness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (F a') b' } → 
+                     A [ A [ FMap U g o  η a' ]  ≈ f ] → B [ f * ≈ g ]
+
+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) ) )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    infixr 11 _*
+    field
+       _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b 
+       isUniversalMapping : IsUniversalMapping A B U F η _*
+
+open NTrans
+open import Category.Cat
+record IsAdjunction  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( η : NTrans A A identityFunctor ( U ○  F ) )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+   field
+       adjoint1 :   { b' : Obj B } →
+                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ id1 A (FObj U b') ]
+       adjoint2 :   {a' : Obj A} →
+                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ id1 B (FObj F a') ]
+
+record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( η : NTrans A A identityFunctor ( U ○  F ) )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor )
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    field
+       isAdjunction : IsAdjunction A B U F η ε
+
+
+record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+                 ( T : Functor A A )
+                 ( η : NTrans A A identityFunctor T )
+                 ( μ : NTrans A A (T ○ T) T)
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+   field
+      assoc  : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
+      unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+
+record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
+       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+  eta : NTrans A A identityFunctor T
+  eta = η
+  mu : NTrans A A (T ○ T) T
+  mu = μ
+  field
+    isMonad : IsMonad A T η μ
+
+Functor*Nat :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
+    (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○  G) (F ○ H)
+Functor*Nat A {B} C F {G} {H} n = record {
+       TMap  = \a -> FMap F (TMap n a)
+       ; isNTrans = record {
+            naturality = naturality
+       }
+    } where
+         naturality : {a b : Obj A} {f : Hom A a b} 
+            → C [ C [ (FMap F ( FMap H f )) o  ( FMap F (TMap n a)) ]  ≈ C [ (FMap F (TMap n b )) o  (FMap F (FMap G f))  ] ]
+         naturality  {a} {b} {f}  = let open ≈-Reasoning (C) in
+            begin  
+               (FMap F ( FMap H f )) o  ( FMap F (TMap n a))
+            ≈⟨ sym (IsFunctor.distr ( isFunctor F)) ⟩
+               FMap F ( B [ (FMap H f)  o TMap n a ])
+            ≈⟨ IsFunctor.≈-cong (isFunctor F) ( IsNTrans.naturality ( isNTrans n)  ) ⟩
+               FMap F ( B [ (TMap n b ) o FMap G f ] )
+            ≈⟨ IsFunctor.distr ( isFunctor F) ⟩
+               (FMap F (TMap n b )) o  (FMap F (FMap G f))
+            ∎
+
+Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (C : Category c₁'' c₂'' ℓ'')
+    (F : Functor A B) -> { G H : Functor B C } -> ( n : NTrans B C G H ) -> NTrans A C (G ○  F) (H ○ F)
+Nat*Functor A B C F {G} {H} n = record {
+       TMap  = \a -> TMap n (FObj F a)
+       ; isNTrans = record {
+            naturality = naturality
+       }
+    } where
+         naturality : {a b : Obj A} {f : Hom A a b} 
+            → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
+         naturality  {a} {b} {f}  = {!!}
+
+
+
+record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
+                 ( T : Functor A A )
+                 ( η : NTrans A A identityFunctor T )
+                 ( μ : NTrans A A (T ○ T) T )
+                 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+     monad : Monad A T η μ 
+     monad = M
+     -- g ○ f = μ(c) T(g) f
+     join : { a b : Obj A } → ( c : Obj A ) →
+                      ( 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 ] ]
+
--- a/nat.agda	Tue Jul 23 17:34:46 2013 +0900
+++ b/nat.agda	Wed Jul 24 20:47:28 2013 +0900
@@ -9,7 +9,9 @@
 
 open import Category -- https://github.com/konn/category-agda
 open import Level
-open import Category.HomReasoning
+--open import Category.HomReasoning
+open import HomReasoning
+open import cat-utility
 
 --T(g f) = T(g) T(f)
 
@@ -33,24 +35,6 @@
 -- μ(a)T(η(a)) = a
 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
 
-record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T)
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-   field
-      assoc  : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-      unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-      unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-
-record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
-       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-  eta : NTrans A A identityFunctor T
-  eta = η
-  mu : NTrans A A (T ○ T) T
-  mu = μ
-  field
-    isMonad : IsMonad A T η μ
 
 open Monad
 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
@@ -92,17 +76,6 @@
 -- f ○ η(a) = f
 -- h ○ (g ○ f) = (h ○ g) ○ f
 
-record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T )
-                 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-     monad : Monad A T η μ 
-     monad = M
-     -- g ○ f = μ(c) T(g) f
-     join : { a b : Obj A } → ( c : Obj A ) →
-                      ( 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 ] ]
 
 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 ] ]
@@ -110,19 +83,18 @@
    let open ≈-Reasoning ( L )  in 
       begin  L [ x o y ]  ∎
 
-
 open Kleisli
 -- η(b) ○ f = f
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
-                 ( T : Functor A A )
+                 { T : Functor A A }
                  ( η : NTrans A A identityFunctor T )
                  { μ : NTrans A A (T ○ T) T }
                  { a : Obj A } ( b : Obj A ) 
                  ( f : Hom A a ( FObj T b) )
                  ( m : Monad A T η μ )
-                 ( k : Kleisli A T η μ m) 
+                 { k : Kleisli A T η μ m}
                       → A  [ join k b (TMap η b) f  ≈ f ]
-Lemma7 c T η b f m k = 
+Lemma7 c {T} η b f m {k} = 
   let open ≈-Reasoning (c) 
       μ = mu ( monad k )
   in 
@@ -167,17 +139,17 @@
 
 -- h ○ (g ○ f) = (h ○ g) ○ f
 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T )
-                 ( a b c d : Obj A )
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { a b c d : Obj A }
                  ( f : Hom A a ( FObj T b) )
                  ( g : Hom A b ( FObj T c) ) 
                  ( h : Hom A c ( FObj T d) )
                  ( m : Monad A T η μ )
-                 ( k : Kleisli A T η μ m)
+                 { k : Kleisli A T η μ m}
                       → A  [ join k d h (join k c g f)  ≈ join k d ( join k d h g) f ]
-Lemma9 A T η μ a b c d f g h m k = 
+Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 
   begin 
      join k d h (join k c g f)  
    ≈⟨⟩
@@ -231,7 +203,41 @@
      join k d ( join k d h g) f 
   ∎ where open ≈-Reasoning (A) 
 
+-- Kleisli-join : {!!}
+-- Kleisli-join = {!!}
 
+-- Kleisli-id : {!!}
+-- Kleisli-id = {!!}
+
+-- Lemma10 : {!!}
+-- Lemma10 = {!!}
+
+-- open import Relation.Binary.Core
+
+-- isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+--                  { T : Functor A A }
+--                  { η : NTrans A A identityFunctor T }
+--                  { μ : NTrans A A (T ○ T) T }
+--                  ( m : Monad A T η μ )
+--                  { k : Kleisli A T η μ m} ->
+--          IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
+-- isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
+--                     ; identityL =   {!!}
+--                     ; identityR =   {!!}
+--                     ; o-resp-≈ =    {!!}
+--                     ; associative = {!!}
+--                     }
+--      where
+--          KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
+--                  { η : NTrans A A identityFunctor T }
+--                  { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) -> {!!}
+--          KidL = {!!}
+--          KidR : {!!}
+--          KidR = {!!}
+--          Ko-resp : {!!}
+--          Ko-resp = {!!}
+--          Kassoc : {!!}
+--          Kassoc = {!!}
 
 -- Kleisli :
 -- Kleisli = record { Hom = 
@@ -249,3 +255,20 @@
 --                                        ; associative = associative
 --                                        }
 --                  }
+
+open Adjunction
+
+-- ( \b -> FMap U ( TMap ε ( FObj F b))  )
+Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 { U : Functor B A }
+                 { F : Functor A B }
+                 { η : NTrans A A identityFunctor ( U ○  F ) }
+                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
+      Adjunction A B U F η ε  → Monad A (U ○  F) η {!!}
+Adj2Monad A B {U} {F} {η} {ε} adj = record {
+         isMonad = record {
+                    assoc = {!!};
+                    unity1 = {!!};
+                    unity2 = {!!}
+              }
+      } 
--- a/universal-mapping.agda	Tue Jul 23 17:34:46 2013 +0900
+++ b/universal-mapping.agda	Wed Jul 24 20:47:28 2013 +0900
@@ -1,8 +1,10 @@
 module universal-mapping where
 
+-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
 open import Category -- https://github.com/konn/category-agda
 open import Level
-open import Category.HomReasoning
+open import HomReasoning
 
 open Functor
 
@@ -11,24 +13,24 @@
 
 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 )
+                 ( 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') } -> 
+       universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
                      A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-       uniquness :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (F a') b' } -> 
-                     A [ A [ FMap U g o  η a' ]  ≈ f ] -> B [ f * ≈ g ]
+       uniquness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (F a') b' } → 
+                     A [ A [ FMap U g o  η a' ]  ≈ f ] → B [ f * ≈ g ]
 
 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) ) )
+                 ( F : Obj A → Obj B )
+                 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
     infixr 11 _*
     field
-       _* :  { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b 
+       _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b 
        isUniversalMapping : IsUniversalMapping A B U F η _*
 
 open NTrans
@@ -40,9 +42,9 @@
                  ( ε : NTrans B B  ( F ○  U ) identityFunctor )
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
-       adjoint1 :   { b' : Obj B } ->
+       adjoint1 :   { b' : Obj B } →
                      A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ id1 A (FObj U b') ]
-       adjoint2 :   {a' : Obj A} ->
+       adjoint2 :   {a' : Obj A} →
                      B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ id1 B (FObj F a') ]
 
 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
@@ -62,22 +64,22 @@
 open Adjunction
 open UniversalMapping
 
-Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  { U : Functor B A }
                  { F : Functor A B }
                  { η : NTrans A A identityFunctor ( U ○  F ) }
-                 { ε : NTrans B B  ( F ○  U ) identityFunctor } ->
-      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) 
-Lemma1 A B {U} {F} {η} {ε} adj = record {
+                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
+      Adjunction A B U F η ε  → UniversalMapping A B U (FObj F) (TMap η) 
+Adj2UM A B {U} {F} {η} {ε} adj = record {
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
                     uniquness = uniqness
               }
       } where
-         solution :  { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
+         solution :  { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) →  Hom B (FObj F a ) b 
          solution  {_} {b} f = B [ TMap ε b o FMap F f ]
-         universalMapping :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> 
+         universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
                      A [ A [ FMap U ( solution f) o TMap η a' ]  ≈ f ]
          universalMapping {a} {b} {f} = 
            let open ≈-Reasoning (A) in
@@ -98,12 +100,12 @@
               ≈⟨  idL  ⟩
                   f
               ∎
-         lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) -> ( g :  Hom B (FObj F a) b) ->
-                A [ A [ FMap U g o  TMap η a ]  ≈ f ] ->
+         lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g :  Hom B (FObj F a) b) →
+                A [ A [ FMap U g o  TMap η a ]  ≈ f ] →
                 B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] 
          lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
-         uniqness :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (FObj F a') b'} -> 
-                     A [ A [ FMap U g o  TMap η a' ]  ≈ f ] -> B [ solution f  ≈ g ]
+         uniqness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (FObj F a') b'} → 
+                     A [ A [ FMap U g o  TMap η a' ]  ≈ f ] → B [ solution f  ≈ g ]
          uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
               begin 
                   solution f 
@@ -138,17 +140,17 @@
 
 FunctorF : {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) ) } ->
-       UniversalMapping A B U F η   -> Functor A B
+                 { F : Obj A → Obj B }
+                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
+       UniversalMapping A B U F η   → Functor A B
 FunctorF A B {U} {F} {η} um = record {
               FObj = F;
               FMap = myFMap ;
               isFunctor = myIsFunctor
        } where
-    myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b)
+    myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b)
     myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ]) 
-    lemma-id1 :  {a : Obj A} ->  A [ A [ FMap U (id1 B (F a))  o  η a ]  ≈ (A [ (η a) o (id1 A a) ]) ]
+    lemma-id1 :  {a : Obj A} →  A [ A [ FMap U (id1 B (F a))  o  η a ]  ≈ (A [ (η a) o (id1 A a) ]) ]
     lemma-id1 {a} = let open ≈-Reasoning (A) in
        begin
            FMap U (id1 B (F a))  o  η a 
@@ -210,9 +212,9 @@
 --
 nat-η : {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) ) } ->
-       (um : UniversalMapping A B U F η )  -> 
+                 { F : Obj A → Obj B }
+                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
+       (um : UniversalMapping A B U F η )  → 
            NTrans  A A identityFunctor ( U ○ FunctorF A B um )
 nat-η A B {U} {F} {η} um = record {
              TMap = η ; isNTrans = myIsNTrans
@@ -234,18 +236,18 @@
 
 nat-ε : {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) ) } ->
-       (um : UniversalMapping A B U F η )  -> 
+                 { F : Obj A → Obj B }
+                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
+       (um : UniversalMapping A B U F η )  → 
            NTrans B B ( FunctorF A B um ○ U) identityFunctor 
 nat-ε A B {U} {F} {η} um = record {
              TMap = ε ; isNTrans = myIsNTrans
        } where
     F' : Functor A B
     F' = FunctorF A B um
-    ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b
+    ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b
     ε b = (_* um) ( id1 A (FObj U b))
-    lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) -> 
+    lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) → 
              A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] )  o η (FObj U a) ]
                  ≈ A [ FMap U f o id1 A (FObj U a) ] ]
     lemma-nat1 a b f = let open ≈-Reasoning (A) in
@@ -266,7 +268,7 @@
        ≈⟨ sym idR ⟩
           FMap U f o id (FObj U a) 
        ∎
-    lemma-nat2 : (a b : Obj B) (f : Hom B a b ) -> A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
+    lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
                                                         ≈ A [ FMap U f o id1 A (FObj U a) ] ]
     lemma-nat2 a b f = let open ≈-Reasoning (A) in
        begin
@@ -305,9 +307,9 @@
 
 UMAdjunction : {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) ) ) ->
-       (um : UniversalMapping A B U F' η' )  -> 
+                 ( F' : Obj A → Obj B )
+                 ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) →
+       (um : UniversalMapping A B U F' η' )  → 
               Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B  um)
 UMAdjunction A B U F' η' um = record {
            isAdjunction = record {
@@ -321,7 +323,7 @@
           η = nat-η A B um
           ε : NTrans B B  ( F ○  U ) identityFunctor 
           ε = nat-ε A B um
-          adjoint1 :   { b : Obj B } ->
+          adjoint1 :   { b : Obj B } →
                      A [ A [ ( FMap U ( TMap ε b ))  o ( TMap η ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
           adjoint1 {b} = let open ≈-Reasoning (A) in
              begin
@@ -331,7 +333,7 @@
              ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um )  ⟩
                id (FObj U b) 
              ∎
-          lemma-adj1 : (a : Obj A) -> 
+          lemma-adj1 : (a : Obj A) → 
              A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ] 
                ≈ (η' a) ]
           lemma-adj1 a =  let open ≈-Reasoning (A) in
@@ -350,7 +352,7 @@
              ≈⟨ idL ⟩
                η' a
              ∎
-          lemma-adj2 : (a : Obj A) -> A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈  η' a ]
+          lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈  η' a ]
           lemma-adj2 a = let open ≈-Reasoning (A) in
              begin
                FMap U (id1 B (FObj F a)) o η' a 
@@ -359,7 +361,7 @@
              ≈⟨ idL ⟩
                η' a 
              ∎
-          adjoint2 :   {a : Obj A} ->
+          adjoint2 :   {a : Obj A} →
                      B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]
           adjoint2 {a} = let open ≈-Reasoning (B) in
              begin