module Cat.Instances.Delooping where

The delooping of a monoid🔗

Given a monoid we build a pointed, connected precategory where the endomorphism monoid of the point recovers 

module _ {â„“} {M : Type â„“} (mm : Monoid-on M) where
  module mm = Monoid-on mm

  B : Precategory lzero â„“
  B .Ob = ⊤
  B .Hom _ _ = M
  B .Hom-set _ _ = mm.has-is-set
  B .Precategory.id = mm.identity
  B .Precategory._∘_ = mm._⋆_
  B .idr _ = mm.idr
  B .idl _ = mm.idl
  B .assoc _ _ _ = mm.associative

  B-is-connected : is-connected-cat B
  B-is-connected .point      = inc tt
  B-is-connected .zigzag _ _ = inc []