Mercurial > hg > Members > kono > Proof > category

changeset 22:b3cb592d7b9d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some law
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jul 2013 15:15:50 +0900
parents a7b0f7ab9881
children 736df1a35807
files nat.agda
diffstat 1 files changed, 103 insertions(+), 56 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Fri Jul 12 13:39:33 2013 +0900
+++ b/nat.agda	Fri Jul 12 15:15:50 2013 +0900
@@ -3,7 +3,7 @@
 -- Monad
 -- Category A
 -- A = Category
--- Functor T : A -> A
+-- Functor T : A → A
 --T(a) = t(a)
 --T(f) = tf(f)
 
@@ -13,17 +13,17 @@
 
 --T(g f) = T(g) T(f)
 
-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 )
+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)
+--   F(a) ---→ F(b)
 --    |          |
 --    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
 --    |          |
 --    v          v
---   G(a) ----> G(b)
+--   G(a) ---→ G(b)
 --        G(f)
 
 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
@@ -45,14 +45,14 @@
 
 open NTrans
 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  )
+      → (μ : 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  )
 
 open import Category.Cat
 
--- η :   1_A -> T
--- μ :   TT -> T
+-- η :   1_A → T
+-- μ :   TT → T
 -- μ(a)η(T(a)) = a
 -- μ(a)T(η(a)) = a
 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
@@ -63,9 +63,9 @@
                  ( μ : NTrans 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 [ 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) ]
 
 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
@@ -81,40 +81,40 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { a : Obj A } ->
+                 { a : Obj A } →
                  ( M : Monad A T η μ )
-    -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
-Lemma3 = \m -> IsMonad.assoc ( isMonad m )
+    → A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
+Lemma3 = \m → IsMonad.assoc ( isMonad m )
 
 
 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
-    -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
-Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
+    → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
+Lemma4 = \a → IsCategory.identityL ( Category.isCategory a )
 
 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { a : Obj A } ->
+                 { a : Obj A } →
                  ( M : Monad A T η μ )
-    ->  A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
+    →  A [ A [ Trans μ a o Trans η ( 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 }
-                 { a : Obj A } ->
+                 { a : Obj A } →
                  ( M : Monad A T η μ )
-    ->  A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
+    →  A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+Lemma6 = \m → IsMonad.unity2 ( isMonad m )
 
 -- T = M x A
 -- nat of η
 -- g ○ f = μ(c) T(g) f
--- h ○ (g ○ f) = (h ○ g) ○ f
 -- η(b) ○ f = f
 -- f ○ η(a) = f
+-- h ○ (g ○ f) = (h ○ g) ○ f
 
 record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
                  ( T : Functor A A )
@@ -123,14 +123,15 @@
                  ( 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 )
+     -- 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 [ Trans μ c  o A [ FMap T g  o f ] ]
 
 
 
 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
-  open import Relation.Binary.Core 
+  open import Relation.Binary.Core renaming ( Trans to Trasn1 )
 
   refl-hom :   {a b : Obj A } { x : Hom A a b }  →
         A [ x ≈ x ]
@@ -141,6 +142,38 @@
         A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
   trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
 
+  -- some short cuts
+
+  car-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) →
+         A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y  o f ] ]
+  car-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+
+  cdr-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A b c ) →
+         A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f  o y ] ]
+  cdr-eq 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 } → A [ A [ id a o f ] ≈ f ]
+  idL =  IsCategory.identityL (Category.isCategory A)
+
+  idR :  {a b : Obj A } { f : Hom A a b } → A [ A [ f o id a ] ≈ f ]
+  idR =  IsCategory.identityR (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}
+                                  → A [ A [ f o A [ g o h ] ]  ≈ A [ A [ 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 }
+     → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ 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 )
+      → A [ A [ (  FMap G f ) o  ( Trans η a ) ]  ≈ A [ (Trans η b ) o  (FMap F f)  ] ]
+  nat _ η  =  IsNTrans.naturality ( isNTrans η  )
+
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
@@ -161,16 +194,16 @@
   _∎ : { 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 :  {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 ) ->
+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 ]
+                      →  A [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) 
   let open ≈-Reasoning (c) in 
      begin  
@@ -179,20 +212,17 @@
           g
      ∎
 
-lemma70 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) ->
-         A [ x ≈ y ] -> A [ A [ x o f ] ≈ A [ y  o f ] ]
-lemma70 c f eq = ( IsCategory.o-resp-≈ ( Category.isCategory c )) ( ≈-Reasoning.refl-hom c ) eq
-
 open Kleisli
-Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
+-- η(b) ○ f = f
+Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
                  ( 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) 
-                      -> A  [ join K b (Trans η b) f  ≈ f ]
+                 ( m : Monad A T η μ )
+                 ( k : Kleisli A T η μ m) 
+                      → A  [ join k b (Trans η b) f  ≈ f ]
 Lemma7 c T η b f m k = 
   let open ≈-Reasoning (c) 
       μ = mu ( monad k )
@@ -203,23 +233,40 @@
          c [ Trans μ b  o c [ FMap T ((Trans η b)) o f ] ]  
      ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
         c [ c [ Trans μ b  o  FMap T ((Trans η b)) ] o f ]
-     ≈⟨ lemma70 c f ( IsMonad.unity2 ( isMonad ( monad k )) )  ⟩
-        c [  Id {_} {_} {_} {c} (FObj T b)   o f ]
+     ≈⟨ car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) )  ⟩
+        c [  id (FObj T b)   o f ]
      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
         f
      ∎
 
-Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
-                 { T : Functor A A }
-                 { η : NTrans A A identityFunctor T }
+-- f ○ η(a) = f
+Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+                 ( T : Functor A A )
+                 ( η : NTrans A A identityFunctor T )
                  { μ : NTrans 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 f (Trans η a)  ≈ f ]
-Lemma8 k = {!!}
+                 ( a  : Obj A )  ( b : Obj A )
+                 ( f : Hom A a ( FObj T b) )
+                 ( m : Monad A T η μ )
+                 ( k : Kleisli A T η μ m) 
+                      → A  [ join k b f (Trans η a)  ≈ f ]
+Lemma8 c T η a b f m k = 
+  begin
+     join k b f (Trans η a) 
+  ≈⟨ refl-hom ⟩
+     c [ Trans μ b  o c [  FMap T f o (Trans η a) ] ]  
+  ≈⟨ cdr-eq (Trans μ b) ( IsNTrans.naturality ( isNTrans η  )) ⟩
+     c [ Trans μ b  o c [ (Trans η ( FObj T b)) o f ] ] 
+  ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
+     c [ c [ Trans μ b  o (Trans η ( FObj T b)) ] o f ] 
+  ≈⟨ car-eq f ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩
+     c [ id (FObj T b)  o f ]
+  ≈⟨  IsCategory.identityL (Category.isCategory c)  ⟩
+     f
+  ∎  where 
+      open ≈-Reasoning (c) 
+      μ = mu ( monad k )
 
+-- h ○ (g ○ f) = (h ○ g) ○ f
 Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
@@ -228,9 +275,9 @@
                  { 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 ]
+                 { 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 k = {!!}