Mercurial > hg > Members > kono > Proof > category

changeset 5:16572013c362

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kleisli Proposition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Jul 2013 14:56:23 +0900
parents 05087d3aeac0
children b1fd8d8689a9
files nat.agda
diffstat 1 files changed, 63 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 06 08:50:32 2013 +0900
+++ b/nat.agda	Sat Jul 06 14:56:23 2013 +0900
@@ -26,28 +26,28 @@
 --   G(a) ----> G(b)
 --        G(f)
 
-record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
+record IsNNAT {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
                  ( F G : Functor D C )
-                 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
+                 (NAT : (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  ( Trans a ) ]  ≈ C [ (Trans b ) o  (FMap F f)  ] ]
+      → C [ C [ (  FMap G f ) o  ( NAT a ) ]  ≈ C [ (NAT b ) o  (FMap F f)  ] ]
 --    uniqness : {d : Obj D} 
---      →  C [ Trans d  ≈ Trans d ]
+--      →  C [ NAT d  ≈ NAT d ]
 
 
-record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
+record NNAT {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
-    Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
-    isNTrans : IsNTrans domain codomain F G Trans
+    NAT :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
+    isNNAT : IsNNAT domain codomain F G NAT
 
-open NTrans
+open NNAT
 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
-      -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b }
-      -> A [ A [  FMap G f o Trans μ a ]  ≈ A [ Trans μ b o  FMap F f ] ]
-Lemma2 = \n -> IsNTrans.naturality ( isNTrans  n  )
+      -> (μ : NNAT A A F G) -> {a b : Obj A} { f : Hom A a b }
+      -> A [ A [  FMap G f o NAT μ a ]  ≈ A [ NAT μ b o  FMap F f ] ]
+Lemma2 = \n -> IsNNAT.naturality ( isNNAT  n  )
 
 open import Category.Cat
 
@@ -59,15 +59,15 @@
 
 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
                  ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T)
+                 ( η : NNAT A A identityFunctor T )
+                 ( μ : NNAT A A (T ○ T) T)
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-      assoc  : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
-      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      assoc  : {a : Obj A} -> A [ A [ NAT μ a o NAT μ ( FObj T a ) ] ≈  A [  NAT μ a o FMap T (NAT μ a) ] ]
+      unity1 : {a : Obj A} -> A [ A [ NAT μ a o NAT η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      unity2 : {a : Obj A} -> A [ A [ NAT μ a o (FMap T (NAT η 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)
+record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NNAT A A identityFunctor T) (μ : NNAT A A (T ○ T) T)
        : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
     isMonad : IsMonad A T η μ
@@ -75,11 +75,11 @@
 open Monad
 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT A A (T ○ T) T }
                  { a : Obj A } ->
                  ( M : Monad A T η μ )
-    -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
+    -> A [ A [  NAT μ a o NAT μ ( FObj T a ) ] ≈  A [  NAT μ a o FMap T (NAT μ a) ] ]
 Lemma3 = \m -> IsMonad.assoc ( isMonad m )
 
 
@@ -89,74 +89,79 @@
 
 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT A A (T ○ T) T }
                  { a : Obj A } ->
                  ( M : Monad A T η μ )
-    ->  A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+    ->  A [ A [ NAT μ a o NAT η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
 Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
 
 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT A A (T ○ T) T }
                  { a : Obj A } ->
                  ( M : Monad A T η μ )
-    ->  A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+    ->  A [ A [ NAT μ a o (FMap T (NAT η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
 Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
 
 -- T = M x A
-
--- open import Data.Product -- renaming (_×_ to _*_)
-
--- MonoidalMonad : 
--- MonoidalMonad = record { Obj = M × A 
---                  ; Hom = _⟶_
---                  ; Id = IdProd
---                  ; _o_ = _∘_
---                  ; _≈_ = _≈_
---                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
---                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
---                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
---                                                                 }
---                                        ; identityL = identityL
---                                        ; identityR = identityR
---                                        ; o-resp-≈ = o-resp-≈
---                                        ; associative = associative
---                                        }
---                  }
-
-
 -- nat of η
-
-
 -- g ○ f = μ(c) T(g) f
 -- h ○ (g ○ f) = (h ○ g) ○ f
-
 -- η(b) ○ f = f
 -- f ○ η(a) = 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 )
+                 ( η : NNAT A A identityFunctor T )
+                 ( μ : NNAT A A (T ○ T) T )
                  ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+     monad : Monad A T η μ 
+     monad = M
      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 [ Trans μ c  o A [ FMap T g  o f ] ]
+     join c g f = A [ NAT μ c  o A [ FMap T g  o f ] ]
+
+open import Relation.Binary
+open import Relation.Binary.Core
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
-                 { μ : NTrans A A (T ○ T) T }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT A A (T ○ T) T }
+                 { a b : Obj A } 
+                 { f : Hom A a ( FObj T b) } 
+                 { M : Monad A T η μ } 
+                 ( K : Kleisli A T η μ M) 
+                      -> A  [ join K b (NAT η b) f  ≈ f ]
+Lemma7 m = {!!}
+
+Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
+                 { T : Functor A A }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT A A (T ○ T) T }
                  { a b : Obj A } 
                  { f : Hom A a ( FObj T b) } 
                  { M : Monad A T η μ } 
                  ( K : Kleisli A T η μ M) 
-                      -> A  [ join ? ? ?  ≈ f ]
-Lemma7 = \m -> {!!}
+                      -> A  [ join K b f (NAT η a)  ≈ f ]
+Lemma8 m = {!!}
+
+Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
+                 { T : Functor A A }
+                 { η : NNAT A A identityFunctor T }
+                 { μ : NNAT 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) 
+                      -> A  [ join K d h (join K c g f)  ≈ join K d ( join K d h g) f ]
+Lemma9 m = {!!}
+