## Definition ## A __monoid__ consists of * A type $A$, * A basepoint $e:A$ * A binary operation $\mu : A \to A \to A$ * A left unitor $$\lambda:\prod_{(a:A)} \mu(e,a)=a$$ * A right unitor $$\rho:\prod_{(a:A)} \mu(a,e)=a$$ * An asssociator $$\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ * A 0-truncator $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y$$ ## 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 ## * [[Synthetic homotopy theory]] * [[A3-space]] * [[commutative monoid]] * [[monoidal groupoid]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)