open import Algebra.Monoid

open import Cat.Prelude

module Cat.Instances.Delooping where

Given a monoid MM, we build a pointed precategory B(M)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 = mm.identity
  r .Precategory._∘_ = mm._⋆_
  r .idr _ = mm.idr
  r .idl _ = mm.idl
  r .assoc _ _ _ = mm.associative

In addition to providing a concise description of sets with MM-actions (functors B(M)SetB(M) \to \set), the delooping category of a monoid lets us reuse the category solver to solve monoid associativity/identity problems:

module _ (M : Monoid ) where private
  module M = Monoid-on (M .snd)
    a b c d : M .fst

  test : ((a M.⋆ b) M.⋆ (c M.⋆ d))
        ((a M.⋆ (M.identity M.⋆ (b M.⋆ M.identity))) M.⋆ (c M.⋆ d))
  test = solve-monoid M