Mercurial > hg > Members > kono > Proof > category

changeset 141:4a362cf32a74

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Aug 2013 16:16:01 +0900
parents aea890b0f8bc
children 94796ddb9570
files monoid-monad.agda
diffstat 1 files changed, 33 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Tue Aug 13 12:55:08 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 16:16:01 2013 +0900
@@ -73,3 +73,36 @@
             commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
        }
   }
+
+open NTrans
+
+Lemma-MM31 : ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) ≡ ( λ x → x )
+Lemma-MM31 = ?
+
+MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
+MonoidMonad = record {
+       isMonad = record {
+           unity1 =  \{a} -> Lemma-MM3 {a} ;
+           unity2 = Lemma-MM4 ;
+           assoc = Lemma-MM5 
+       }  
+   } where
+       A = Sets {c ⊔ c₁ ⊔ 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
+                begin
+                     TMap μ a o TMap η ( FObj T a )
+                ≈⟨⟩
+                    ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
+                ≈⟨ Lemma-MM31 ⟩
+                    ( λ x → x )
+                ≈⟨⟩
+                     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 = {!!}
+       Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
+       Lemma-MM5 = {!!}
+
+
+