Mercurial > hg > Members > kono > Proof > category
changeset 143:bbaaca9b21ce
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Aug 2013 18:07:27 +0900 |
| parents | 94796ddb9570 |
| children | 0948df8c88b8 |
| files | monoid-monad.agda |
| diffstat | 1 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- 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 {