Session 13: Monoids
Definition: Monoid (p. 166)
A category with exactly one object is called a monoid.
The corresponding mathlib definition is CategoryTheory.SingleObj, which is an abbreviation for Quiver.SingleObj. We print both below for reference.
@[reducible] def CategoryTheory.SingleObj.{u_1} : Type u_1 → Type :=
Quiver.SingleObj#print SingleObj
@[reducible] def CategoryTheory.SingleObj.{u_1} : Type u_1 → Type :=
Quiver.SingleObjdef Quiver.SingleObj.{u_1} : Type u_1 → Type :=
fun x ↦ Unit#print Quiver.SingleObj
def Quiver.SingleObj.{u_1} : Type u_1 → Type :=
fun x ↦ Unit