21 lines
578 B
Agda
21 lines
578 B
Agda
open import Category.Core
|
||
open Category
|
||
|
||
open import Algebra using (Monoid)
|
||
open import Data.Unit using (⊤; tt)
|
||
|
||
module Category.Instances.Monoid {c ℓ} (M : Monoid c ℓ) where
|
||
|
||
open Monoid M renaming (Carrier to S; _≈_ to _M≈_; assoc to Massoc)
|
||
|
||
MonoidCat : Category
|
||
MonoidCat .Obj = ⊤
|
||
MonoidCat .Hom tt tt = S
|
||
MonoidCat ._≈_ = _M≈_
|
||
MonoidCat ._∘_ = _∙_
|
||
MonoidCat .𝟙 = ε
|
||
MonoidCat .assoc f g h = sym (Massoc f g h)
|
||
MonoidCat .identity-ˡ = identityˡ
|
||
MonoidCat .identity-ʳ = identityʳ
|
||
MonoidCat .equiv = isEquivalence
|
||
MonoidCat .≈-resp-∘ = ∙-cong
|