22 lines
578 B
Agda
22 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
|