module Cat.Instances.Delooping where

Given a monoid MM, we build a pointed precategory BM\mathbf{B} M, where the endomorphism monoid of the point recovers MM.

B : ∀ {ℓ} {M : Type ℓ} → Monoid-on M → Precategory lzero ℓ
B {M = M} mm = r where
  module mm = Monoid-on mm
  open Precategory

  r : Precategory _ _
  r .Ob = ⊤
  r .Hom _ _ = M
  r .Hom-set _ _ = mm.has-is-set
  r .Precategory.id = mm.identity
  r .Precategory._∘_ = mm._⋆_
  r .idr _ = mm.idr
  r .idl _ = mm.idl
  r .assoc _ _ _ = mm.associative