Mercurial > hg > Members > kono > Proof > category
changeset 140:aea890b0f8bc
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Aug 2013 12:55:08 +0900 |
| parents | 17f45f909770 |
| children | 4a362cf32a74 |
| files | monoid-monad.agda |
| diffstat | 1 files changed, 1 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/monoid-monad.agda Tue Aug 13 12:47:37 2013 +0900 +++ b/monoid-monad.agda Tue Aug 13 12:55:08 2013 +0900 @@ -2,7 +2,7 @@ open import Category.Monoid open import Algebra open import Level -module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ } where +module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ} where open import HomReasoning open import cat-utility @@ -12,10 +12,6 @@ open import Relation.Binary.Core open import Relation.Binary - -MC : Category (suc zero) c (suc (ℓ ⊔ c)) -MC = MONOID Mono - open Monoid -- T : A → (M x A)