#Contents# * table of contents {:toc} ## 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 $$\mu(a, b) \coloneqq \alpha(a)(b)$$ ## 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, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)