## Definition ## A __commutative monoid__ consists of * A type $A$, * A basepoint $e:A$ * A binary operation $\mu : A \to A \to A$ * A contractible left unit identity $$c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)$$ * A contractible right unit identity $$c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)$$ * A contractible associative identity $$c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))$$ * A contractible commutative identity $$c_\kappa:\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))$$ * A 0-truncator $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)$$ ## Examples ## * The [[integers]] are a commutative monoid. ## See also ## * [[abelian group]] * [[monoid]]