module Cat.Instances.Delooping where
Given a monoid , we build a pointed precategory , where the endomorphism monoid of the point recovers .
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