# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376384847 -32400
# Node ID bbaaca9b21cee62754d56a9b5f881faf177ff07f
# Parent  94796ddb9570ab80f48cf0a529191b6ebee363a1
on going ...

diff -r 94796ddb9570 -r bbaaca9b21ce monoid-monad.agda
--- a/monoid-monad.agda	Tue Aug 13 18:02:45 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 18:07:27 2013 +0900
@@ -77,17 +77,17 @@
 
 open NTrans
 
-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-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-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } →  (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡  x )
+--Lemma-MM31 a = {!!}
 
 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 = {!!}
+Lemma-M-34 : { x : Carrier Mono  } -> _≈_ Mono ((_∙_ Mono (ε Mono)  x)) x 
+Lemma-M-34  {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
 
 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
 MonoidMonad = record {