Mercurial > hg > Members > kono > Proof > category

changeset 142:94796ddb9570

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 18:02:45 +0900
parents 4a362cf32a74
children bbaaca9b21ce
files monoid-monad.agda
diffstat 1 files changed, 13 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Tue Aug 13 16:16:01 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 18:02:45 2013 +0900
@@ -4,6 +4,7 @@
 open import Level
 module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ}  where
 
+open import Algebra.Structures
 open import HomReasoning
 open import cat-utility
 open import Category.Cat
@@ -76,8 +77,17 @@
 
 open NTrans
 
-Lemma-MM31 : ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) ≡ ( λ x → x )
-Lemma-MM31 = ?
+Lemma-MM32 :  ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x )  ≡ ( λ x → g x ) )
+Lemma-MM32 eq = cong ( \f -> \x -> f x  ) eq
+
+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-M-34 : ( x : Carrier Mono  ) -> _≈_ Mono ((_∙_ Mono (ε Mono)  x)) x 
+Lemma-M-34  = proj₁ ( IsMonoid.identity ( isMonoid Mono ) )
+
+Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } →  (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡  x )
+Lemma-MM31 a = {!!}
 
 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
 MonoidMonad = record {
@@ -94,7 +104,7 @@
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨ Lemma-MM31 ⟩
+                ≈⟨ {!!} ⟩
                     ( λ x → x )
                 ≈⟨⟩
                      Id {_} {_} {_} {A} (FObj T a)