Mercurial > hg > Members > kono > Proof > category

changeset 149:2f68a9e0167b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2013 12:04:50 +0900
parents 6e80e1aaa8b9
children 5dc6f3f43507
files monoid-monad.agda
diffstat 1 files changed, 41 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Thu Aug 15 11:45:24 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 15 12:04:50 2013 +0900
@@ -1,13 +1,13 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Algebra
 open import Level
-module monoid-monad {c c₁ c₂ ℓ : Level}   where
+open import Category.Sets
+module monoid-monad {c : Level} where
 
 open import Algebra.Structures
 open import HomReasoning
 open import cat-utility
 open import Category.Cat
-open import Category.Sets
 open import Data.Product
 open import Relation.Binary.Core
 open import Relation.Binary
@@ -28,13 +28,14 @@
 postulate Mono : ≡-Monoid c
 open ≡-Monoid
 
+A = Sets {c}
 
 -- T : A → (M x A)
 
-T : Functor (Sets {c}) (Sets {c})
+T : Functor A A
 T = record {
-        FObj = \a → (Carrier Mono) × a
-        ; FMap = \f → map ( \x → x ) f
+        FObj = λ a → (Carrier Mono) × a
+        ; FMap = λ f → map ( λ x → x ) f
         ; isFunctor = record {
              identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
              ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
@@ -47,10 +48,10 @@
 
 open Functor
 
-Lemma-MM1 :  {a b : Obj Sets} {f : Hom Sets a b} →
-        Sets [ Sets [ FMap T f o (λ x → ε Mono , x) ] ≈
-        Sets [ (λ x → ε Mono , x) o f ] ]
-Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in 
+Lemma-MM1 :  {a b : Obj A} {f : Hom A a b} →
+        A [ A [ FMap T f o (λ x → ε Mono , x) ] ≈
+        A [ (λ x → ε Mono , x) o f ] ]
+Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in 
         begin
              FMap T f o (λ x → ε Mono , x)
         ≈⟨⟩
@@ -58,34 +59,34 @@
         ∎
 
 -- a → (ε,a)
-η : NTrans  (Sets {c}) (Sets {c}) identityFunctor T
+η : NTrans  A A identityFunctor T
 η = record {
-       TMap = \a → \(x : a) → ( ε Mono , x ) ;
+       TMap = λ a → λ(x : a) → ( ε Mono , x ) ;
        isNTrans = record {
-            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+            commute = Lemma-MM1
        }
   }
 
 -- (m,(m',a)) → (m*m,a)
 
-muMap : (a : Obj Sets  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
+muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )
 
-Lemma-MM2 :  {a b : Obj Sets} {f : Hom Sets a b} →
-        Sets [ Sets [ FMap T f o (λ x → muMap a x) ] ≈
-        Sets [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
-Lemma-MM2 {a} {b} {f} =  let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in                                                       
+Lemma-MM2 :  {a b : Obj A} {f : Hom A a b} →
+        A [ A [ FMap T f o (λ x → muMap a x) ] ≈
+        A [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
+Lemma-MM2 {a} {b} {f} =  let open ≈-Reasoning A renaming ( _o_ to _*_ ) in                                                       
         begin
              FMap T f o (λ x → muMap a x)
         ≈⟨⟩
              (λ x → muMap b x) o FMap (T ○ T) f
         ∎
 
-μ : NTrans  (Sets {c}) (Sets {c}) ( T ○ T ) T
+μ : NTrans  A A ( T ○ T ) T
 μ = record {
-       TMap = \a → \x  → muMap a x ; 
+       TMap = λ a → λ x  → muMap a x ; 
        isNTrans = record {
-            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+            commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f}
        }
   }
 
@@ -94,35 +95,31 @@
 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡ x )
 Lemma-MM33 =  _≡_.refl
 
-Lemma-MM34 : ∀{ x : Carrier Mono  } -> ( (Mono ∙ ε Mono) x ≡ x  )
+Lemma-MM34 : ∀{ x : Carrier Mono  } → ( (Mono ∙ ε Mono) x ≡ x  )
 Lemma-MM34  {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x )
 
-Lemma-MM35 : ∀{ x : Carrier Mono  } -> ((Mono ∙ x) (ε Mono))  ≡ x
+Lemma-MM35 : ∀{ x : Carrier Mono  } → ((Mono ∙ x) (ε Mono))  ≡ x
 Lemma-MM35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid Mono )) ) x
 
-Lemma-MM36 : ∀{ x y z : Carrier Mono } -> ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
+Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
 Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
 
--- We cannot prove this ...
--- Lemma-MM38 :  ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> (( λ x -> f x)  ≡ (λ x -> g x) )
--- Lemma-MM38 {x} {f} {g} eq  = {!!}
+-- Functional Extensionarity  (We cannot prove this in Agda / Coq, just assumming )
+postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
 
--- Functional Extensionarity 
-postulate Lemma-MM39 : {f g : Carrier Mono -> Carrier Mono } -> (∀ {x} -> (f x ≡ g x))  -> ( f ≡ g ) 
-
-postulate Lemma-MM40 :   {f g : Carrier Mono -> Carrier Mono -> Carrier Mono -> Carrier Mono } -> 
-               (∀{x y z} -> f x y z ≡ g x y z )  -> ( f ≡ g ) 
+postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } → 
+               (∀{x y z} → f x y z ≡ g x y z )  → ( f ≡ g ) 
 
-Lemma-MM9  : ( \(x : Carrier Mono) -> ( Mono ∙ ε Mono ) x )  ≡ ( \(x : Carrier Mono) -> x ) 
-Lemma-MM9  = Lemma-MM39 Lemma-MM34
+Lemma-MM9  : ( λ(x : Carrier Mono) → ( Mono ∙ ε Mono ) x )  ≡ ( λ(x : Carrier Mono) → x ) 
+Lemma-MM9  = Extensionarity Lemma-MM34
 
-Lemma-MM10 : ( \x ->   ((Mono ∙ x) (ε Mono)))  ≡ ( \x -> x ) 
-Lemma-MM10 = Lemma-MM39 Lemma-MM35
+Lemma-MM10 : ( λ x →   ((Mono ∙ x) (ε Mono)))  ≡ ( λ x → x ) 
+Lemma-MM10 = Extensionarity Lemma-MM35
 
-Lemma-MM11 : (\x y z -> ((Mono ∙ (Mono ∙ x) y) z))  ≡ (\x y z -> ( _∙_ Mono  x (_∙_ Mono y z ) ))
-Lemma-MM11 = Lemma-MM40 Lemma-MM36 
+Lemma-MM11 : (λ x y z → ((Mono ∙ (Mono ∙ x) y) z))  ≡ (λ x y z → ( _∙_ Mono  x (_∙_ Mono y z ) ))
+Lemma-MM11 = Extensionarity3 Lemma-MM36 
 
-MonoidMonad : Monad (Sets {c}) T η μ 
+MonoidMonad : Monad A T η μ 
 MonoidMonad = record {
        isMonad = record {
            unity1 = Lemma-MM3 ;
@@ -130,14 +127,13 @@
            assoc  = Lemma-MM5 
        }  
    } where
-       A = Sets {c} 
        Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-       Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
+       Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨  cong ( \f -> ( \x ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
+                ≈⟨  cong ( λ f → ( λ x →  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                     ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )
@@ -145,12 +141,12 @@
                      Id {_} {_} {_} {A} (FObj T a)
                 ∎
        Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-       Lemma-MM4 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
+       Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
                 begin
                      TMap μ a o (FMap T (TMap η a ))
                 ≈⟨⟩
                     ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x )
-                ≈⟨  cong ( \f -> ( \x ->  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
+                ≈⟨  cong ( λ f → ( λ x →  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
                     ( λ x → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )
@@ -158,12 +154,12 @@
                      Id {_} {_} {_} {A} (FObj T a)
                 ∎
        Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-       Lemma-MM5 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
+       Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
                 begin
                       TMap μ a o TMap μ ( FObj T a ) 
                 ≈⟨⟩
                       ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
-                ≈⟨ cong ( \f -> ( \x -> 
+                ≈⟨ cong ( λ f → ( λ x → 
                          (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ,  proj₂ (proj₂ (proj₂ x)) )
                          )) Lemma-MM11  ⟩
                       ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))