open import Algebra.Monoid

open import Cat.Prelude

open import Data.List

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 .Precategory.id = mm.identity
  r .Precategory._∘_ = mm._⋆_
  r .idr _ = mm.idr
  r .idl _ = mm.idl
  r .assoc _ _ _ = mm.associative