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