#Contents# * table of contents {:toc} ## Definition ## A __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 0-truncator $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)$$ ## Properties ## ### Monoid homomorphisms ### A __monoid homomorphism__ between two monoids $A$ and $B$ consists of * A function $\phi:A \to B$ such that * The basepoint is preserved $$\phi(e_A) = e_B$$ * The binary operation is preserved $$\prod_{(a:A)} \prod_{(b:A)} \phi(\mu_A(a, b)) = \mu_B(\phi(a),\phi(b))$$ For any function $$\phi_{c_\lambda}:\left(\prod_{(a:A)} isContr(\mu(e_A,a)=a)\right) \to \left(\prod_{(b:B)} isContr(\mu(e_B,b)=b)\right)$$ the contractible left unit identity is preserved: $$\phi_{c_\lambda}({c_\lambda}_A) = {c_\lambda}_B$$ because $$\prod_{(b:B)} isContr(\mu(e_B,b)=b)$$ is contractible. Likewise, for any function $$\phi_{c_\rho}:\left(\prod_{(a:A)} isContr(\mu(a, e_A)=a)\right) \to \left(\prod_{(b:B)} isContr(\mu(b, e_B)=b)\right)$$ the contractible right unit identity is preserved: $$\phi_{c_\rho}({c_\rho}_A) = {c_\rho}_B$$ because $$\prod_{(b:B)} isContr(\mu(b,e_B)=b)$$ is contractible, and for any function $$\phi_{c_\alpha}:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} isContr(\mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3)))\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} isContr(\mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3)))\right)$$ the contractible associative identity is preserved: $$\phi_{c_\alpha}({c_\alpha}_A) = {c_\alpha}_B$$ because $$\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} isContr(\mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3)))$$ is contractible. Finally, the 0-truncator is always preserved in a function between two sets. ### Monoid isomorphisms ### A __monoid isomorphism__ between two monoids $A$ and $B$ consists of * a monoid homomorphism $f: A \to B$ * a monoid homomorphism $f^{-1}: B \to A$ that is an inverse function of $f$. ### Structure identity principle for monoids ### (...) ### Relation to $A_3$-spaces ### Since for all $a, b, c:A$, $\mu(e,a)=a$, $\mu(a,e)=a$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ 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))$$ 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))$$ to be the __left unitor__, __right unitor__, and __associator__ respectively, which means that a monoid is an [[A3-space|$A_3$-space]]. Similarly, any 0-truncated $A_3$-space or $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$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ 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))$$ are inhabited by definition of an $A_3$-space, each identity type $\mu(e,a)=a$, $\mu(a,e)=a$, and $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ 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)))$$ which along with the 0-truncator means that a 0-truncated $A_3$-space is a monoid. As monoids are $A_3$-spaces, given monoids $A$ and $B$, for any function $$\phi_\lambda:\left(\prod_{(a:A)} \mu(e_A,a)=a\right) \to \left(\prod_{(b:B)} \mu(e_B,b)=b\right)$$ the left unitor is preserved: $$\phi_\lambda(\lambda_A) = \lambda_B$$ because $$\prod_{(b:B)} \mu(e_B,b)=b$$ is contractible. Likewise, for any function $$\phi_\rho:\left(\prod_{(a:A)} \mu(a, e_A)=a\right) \to \left(\prod_{(b:B)} \mu(b, e_B)=b\right)$$ the right unitor is preserved: $$\phi_\rho(\rho_A) = \rho_B$$ because $$\prod_{(b:B)} \mu(b,e_B)=b$$ is contractible, and for any function $$\phi_\alpha:\left(\prod_{(a_1:A)} \prod_{(a_2:A)} \prod_{(a_3:A)} \mu(\mu(a_1, a_2),a_3)=\mu(a_1,\mu(a_2,a_3))\right) \to \left(\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))\right)$$ the associator is preserved: $$\phi_\alpha(\alpha_A) = \alpha_B$$ because $$\prod_{(b_1:B)} \prod_{(b_2:B)} \prod_{(b_3:B)} \mu(\mu(b_1, b_2),b_3)=\mu(b_1,\mu(b_2,b_3))$$ is contractible. This means that a monoid homomorphism is also a homomorphism of $A_3$-spaces. ## Examples ## * Every [[contractible]] magma is a monoid. * 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]] * [[group]] * [[monoidal groupoid]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)