Mercurial > hg > Members > kono > Proof > category

changeset 145:57df6cb8f253

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 Wed, 14 Aug 2013 22:45:50 +0900
parents 0948df8c88b8
children 945f26ed12d5
files monoid-monad.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Wed Aug 14 10:26:45 2013 +0900
+++ b/monoid-monad.agda	Wed Aug 14 22:45:50 2013 +0900
@@ -99,6 +99,9 @@
 ≡-to≈ : { f g : Carrier Mono } -> f ≡ g -> _≈_ Mono f g
 ≡-to≈  _≡_.refl = IsEquivalence.refl (IsMonoid.isEquivalence (isMonoid Mono ) )
 
+Lemma-M-37 : { a x y : Set } ( f g : Set -> Carrier Mono ) -> ( _≈_ Mono ( f a ) ( g a) ) ->  ( f x , y ) ≡ ( g x , y )
+Lemma-M-37 f g eq =  ?
+
 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
 MonoidMonad = record {
        isMonad = record {
@@ -141,7 +144,7 @@
                 ≈⟨⟩
                       ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
                 -- ≈⟨ (\x ->  Lemma-M-36 ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ⟩
-                ≈⟨ ? ⟩
+                ≈⟨ {!!} ⟩
                       ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨⟩
                       TMap μ a o FMap T (TMap μ a)