## 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)$$ ## Properties ## ### Relation to commutative $A_3$-spaces ### Since for all $a, b, c:A$, $\mu(e,a)=a$, $\mu(a,e)=a$, $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$, and $\mu(a, b)=\mu(b, a)$ are [[contractible]], the types $$\prod_{(a:A)} \mu(e,a)=a$$ $$\prod_{(a:A)} \mu(a,e)=a$$ $$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ $$\prod_{(a:A)} \prod_{(b:A)} \mu(a, b)=\mu(b, a)$$ are contractible and thus pointed, and thus one could choose any point $$\lambda:\prod_{(a:A)} \mu(e,a)=a$$ $$\rho:\prod_{(a:A)} \mu(a,e)=a$$ $$\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ $$\kappa:\prod_{(a:A)} \prod_{(b:A)} \mu(a, b)=\mu(b, a)$$ to be the __left unitor__, __right unitor__, __associator__, and __commutator__ respectively, which means that a commutative monoid is a [[commutative A3-space|commutative $A_3$-space]]. Similarly, any 0-truncated commutative $A_3$-space or commutative $A_3$-algebra in sets is a monoid, as any identity type between any two terms of a set are propositions, and thus for every $a, b, c:A$, the identity types $\mu(e,a)=a$, $\mu(a,e)=a$, $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$, and $\mu(a, b)=\mu(b, a)$ are [[proposition]]s. Since the dependent product types $$\prod_{(a:A)} \mu(e,a)=a$$ $$\prod_{(a:A)} \mu(a,e)=a$$ $$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ $$\prod_{(a:A)} \prod_{(b:A)} \mu(a, b)=\mu(b, a)$$ are inhabited by definition of a commutative $A_3$-space, each identity type $\mu(e,a)=a$, $\mu(a,e)=a$, $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$, and $\mu(a, b)=\mu(b, a)$ is an inhabited proposition, which makes it contractible. Thus, $$\prod_{(a:A)} isContr(\mu(e,a)=a)$$ $$\prod_{(a:A)} isContr(\mu(a,e)=a)$$ $$\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))$$ $$\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))$$ which along with the 0-truncator means that a 0-truncated commutative $A_3$-space is a commutative monoid. ## Examples ## * Every [[contractible]] magma is a commutative monoid. * The [[integers]] are a commutative monoid. ## See also ## * [[Higher algebra]] * [[abelian group]] * [[commutative A3-space]] * [[monoid]] * [[N-algebra]]