Mercurial > hg > Members > kono > Proof > category

diff nat.agda @ 130:5f331dfc000b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove Kleisli record
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Aug 2013 22:05:41 +0900
parents e763efd30868
children
line wrap: on
line diff
--- a/nat.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/nat.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -24,9 +24,7 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } 
-                 { K : Kleisli A T η μ M } where
-
+                 { M : Monad A T η μ }  where
 
 --T(g f) = T(g) T(f)
 
@@ -40,7 +38,7 @@
 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 TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
-Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )
+Lemma2 = \n → IsNTrans.commute ( isNTrans  n  )
 
 -- Laws of Monad
 --
@@ -92,19 +90,18 @@
 -- f ○ η(a) = f               -- right id  (Lemma8)
 -- h ○ (g ○ f) = (h ○ g) ○ f  -- assocation law (Lemma9)
 
-open Kleisli
 -- η(b) ○ f = f
 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
-                      → A  [ join K (TMap η b) f  ≈ f ]
+                      → A  [ join M (TMap η b) f  ≈ f ]
 Lemma7 {_} {b} f = 
   let open ≈-Reasoning (A) in 
      begin  
-         join K (TMap η b) f 
+         join M (TMap η b) f 
      ≈⟨ refl-hom ⟩
          A [ TMap μ b  o A [ FMap T ((TMap η b)) o f ] ]  
      ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
         A [ A [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
-     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) )  ⟩
+     ≈⟨ car ( IsMonad.unity2 ( isMonad M) )  ⟩
         A [  id (FObj T b)   o f ]
      ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
         f
@@ -113,17 +110,17 @@
 -- f ○ η(a) = f
 Lemma8 : { a  : Obj A }  { b : Obj A }
                  ( f : Hom A a ( FObj T b) )
-                      → A  [ join K f (TMap η a)  ≈ f ]
+                      → A  [ join M f (TMap η a)  ≈ f ]
 Lemma8 {a} {b} f = 
   begin
-     join K f (TMap η a) 
+     join M f (TMap η a) 
   ≈⟨ refl-hom ⟩
      A [ TMap μ b  o A [  FMap T f o (TMap η a) ] ]  
   ≈⟨ cdr  ( nat η ) ⟩
      A [ TMap μ b  o A [ (TMap η ( FObj T b)) o f ] ] 
   ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
      A [ A [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
-  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad K )) ) ⟩
+  ≈⟨ car ( IsMonad.unity1 ( isMonad M) ) ⟩
      A [ id (FObj T b)  o f ]
   ≈⟨  IsCategory.identityL (Category.isCategory A)  ⟩
      f
@@ -135,12 +132,12 @@
                  ( h : Hom A c ( FObj T d) )
                  ( g : Hom A b ( FObj T c) ) 
                  ( f : Hom A a ( FObj T b) )
-                      → A  [ join K h (join K g f)  ≈ join K ( join K h g) f ]
+                      → A  [ join M h (join M g f)  ≈ join M ( join M h g) f ]
 Lemma9 {a} {b} {c} {d} h g f = 
   begin 
-     join K h (join K g f)  
+     join M h (join M g f)  
    ≈⟨⟩
-     join K h (                  ( TMap μ c o ( FMap T g o f ) ) )
+     join M h (                  ( TMap μ c o ( FMap T g o f ) ) )
    ≈⟨ refl-hom ⟩
      ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
    ≈⟨ cdr ( cdr ( assoc )) ⟩
@@ -185,25 +182,25 @@
    ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
      ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
    ≈⟨ refl-hom ⟩
-     join K ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
+     join M ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
    ≈⟨ refl-hom ⟩
-     join K ( join K h g) f 
+     join M ( join M h g) f 
   ∎ where open ≈-Reasoning (A) 
 
 --
 --  o-resp in Kleisli Category ( for Functor definitions )
 --
 Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
-                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join K h f) ≈ (join K i g) ]
+                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
 Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
    begin 
-       join K h f
+       join M h f
    ≈⟨⟩
        TMap μ c  o ( FMap T h  o f )
    ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
        TMap μ c  o ( FMap T i  o g )
    ≈⟨⟩
-       join K i g
+       join M i g
    ∎
 
 --
@@ -228,7 +225,7 @@
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
 _*_ : { a b c : Obj A } → ( KHom b c) → (  KHom a b) → KHom a c 
-_*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
+_*_ {a} {b} {c} g f = record { KMap = join M {a} {b} {c} (KMap g) (KMap f) }
 
 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id 
 isKleisliCategory  = record  { isEquivalence =  isEquivalence 
@@ -384,7 +381,7 @@
           ≈⟨ sym assoc ⟩
              TMap μ c  o ( (FMap T  (TMap η c o g))  o  (TMap η b o f) )
           ≈⟨⟩
-             join K (TMap η c o g)  (TMap η b o f) 
+             join M (TMap η c o g)  (TMap η b o f) 
           ≈⟨⟩
              KMap  ( ffmap g * ffmap f )
           ∎
@@ -424,9 +421,9 @@
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
-       naturality1 :  {a b : Obj A} {f : Hom A a b}
+       commute1 :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ (  FMap ( U_T ○ F_T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           begin
               ( FMap ( U_T ○ F_T ) f ) o  ( TMap η a )
           ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩
@@ -435,16 +432,16 @@
               TMap η b o f
           ∎ 
        isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
-       isNTrans1 = record { naturality = naturality1 } 
+       isNTrans1 = record { commute = commute1 } 
 
 tmap-ε : (a : Obj A) -> KHom (FObj T a) a
 tmap-ε a = record { KMap = id1 A (FObj T a) }
 
 nat-ε : NTrans KleisliCategory KleisliCategory  ( F_T ○ U_T ) identityFunctor
 nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where
-       naturality1 : {a b : Obj A} {f : KHom a b}
+       commute1 : {a b : Obj A} {f : KHom a b}
             →  (f * ( tmap-ε a ) ) ⋍   (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ) )
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin
               KMap (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ))
           ≈⟨⟩
@@ -475,7 +472,7 @@
               KMap (f * ( tmap-ε a ))
           ∎ )
        isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
-       isNTrans1 = record { naturality = naturality1 } 
+       isNTrans1 = record { commute = commute1 } 
 
 --
 -- μ = U_T ε U_F
@@ -485,9 +482,9 @@
 
 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T )
 nat-μ = record { TMap = tmap-μ ; isNTrans = isNTrans1 } where
-        naturality1 : {a b : Obj A} {f : Hom A a b}
+        commute1 : {a b : Obj A} {f : Hom A a b}
              →  A [ A [ (FMap (U_T ○ F_T) f) o  ( tmap-μ a) ]  ≈ A [ ( tmap-μ b ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  ] ]
-        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin
              ( tmap-μ b ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  
           ≈⟨⟩
@@ -502,7 +499,7 @@
              (FMap (U_T ○ F_T) f) o  ( tmap-μ a) 
           ∎ )
         isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ
-        isNTrans1 = record { naturality = naturality1 } 
+        isNTrans1 = record { commute = commute1 } 
 
 Lemma12 : {x : Obj A } -> A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma12 {x} = let open ≈-Reasoning (A) in