Definition

A monoid is a set $M$ with an element $e:M$ and a function $\alpha:M \to (M \to M)$ such that

• $\alpha(1) = \mathrm{id}_M$

• for all $a:M$, $\alpha(a)(1) = a$

• for all $a:M$, $b:M$, and $c:M$, $(\alpha(a) \circ \alpha(b))(c) = \alpha(a)(\alpha(b)(c))$

We define the binary operation $\mu:M \times M \to M$ as

Examples

• The integers are a monoid.

• Given a set $A$, the type of endofunctions $A \to A$ has the structure of an monoid, with basepoint $id_A$, operation function composition.

See also

• commutative monoid
• group
• action

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)