Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 143:bbaaca9b21ce

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:07:27 +0900
parents 94796ddb9570
children 0948df8c88b8
comparison
equal deleted inserted replaced
142:94796ddb9570 143:bbaaca9b21ce
75 } 75 }
76 } 76 }
77 77
78 open NTrans 78 open NTrans
79 79
80 Lemma-MM32 : ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x ) ≡ ( λ x → g x ) ) 80 --Lemma-MM32 : ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x ) ≡ ( λ x → g x ) )
81 Lemma-MM32 eq = cong ( \f -> \x -> f x ) eq 81 --Lemma-MM32 eq = cong ( \f -> \x -> f x ) eq
82
83 --Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } → (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡ x )
84 --Lemma-MM31 a = {!!}
82 85
83 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) 86 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x )
84 Lemma-MM33 = _≡_.refl 87 Lemma-MM33 = _≡_.refl
85 88
86 Lemma-M-34 : ( x : Carrier Mono ) -> _≈_ Mono ((_∙_ Mono (ε Mono) x)) x 89 Lemma-M-34 : { x : Carrier Mono } -> _≈_ Mono ((_∙_ Mono (ε Mono) x)) x
87 Lemma-M-34 = proj₁ ( IsMonoid.identity ( isMonoid Mono ) ) 90 Lemma-M-34 {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
88
89 Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } → (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡ x )
90 Lemma-MM31 a = {!!}
91 91
92 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 92 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ
93 MonoidMonad = record { 93 MonoidMonad = record {
94 isMonad = record { 94 isMonad = record {
95 unity1 = \{a} -> Lemma-MM3 {a} ; 95 unity1 = \{a} -> Lemma-MM3 {a} ;