Homotopy Type Theory monoid > history (Rev #10)

Contents

Definition

A monoid consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A contractible left unit identity
    c λ: (a:G)isContr(μ(e,a)=a)c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)
  • A contractible right unit identity
    c ρ: (a:G)isContr(μ(a,e)=a)c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)
  • A contractible associative identity
    c α: (a:G) (b:G) (c:G)isContr(μ(μ(a,b),c)=μ(a,μ(b,c)))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
    τ 0: (a:A) (b:A)isProp(a=b)\tau_0: \prod_{(a:A)} \prod_{(b:A)} isProp(a=b)

Properties

Monoid homomorphisms

A monoid homomorphism between two monoids AA and BB consists of

  • A function ϕ:AB\phi:A \to B such that
    • The basepoint is preserved
      ϕ(e A)=e B\phi(e_A) = e_B
    • The binary operation is preserved
      (a:A) (b:A)ϕ(μ A(a,b))=μ B(ϕ(a),ϕ(b))\prod_{(a:A)} \prod_{(b:A)} \phi(\mu_A(a, b)) = \mu_B(\phi(a),\phi(b))

For any function

ϕ c λ:( (a:A)isContr(μ(e A,a)=a))( (b:B)isContr(μ(e B,b)=b))\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:

ϕ c λ(c λ A)=c λ B\phi_{c_\lambda}({c_\lambda}_A) = {c_\lambda}_B

because

(b:B)isContr(μ(e B,b)=b)\prod_{(b:B)} isContr(\mu(e_B,b)=b)

is contractible. Likewise, for any function

ϕ c ρ:( (a:A)isContr(μ(a,e A)=a))( (b:B)isContr(μ(b,e B)=b))\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:

ϕ c ρ(c ρ A)=c ρ B\phi_{c_\rho}({c_\rho}_A) = {c_\rho}_B

because

(b:B)isContr(μ(b,e B)=b)\prod_{(b:B)} isContr(\mu(b,e_B)=b)

is contractible, and for any function

ϕ c α:( (a 1:A) (a 2:A) (a 3:A)isContr(μ(μ(a 1,a 2),a 3)=μ(a 1,μ(a 2,a 3))))( (b 1:B) (b 2:B) (b 3:B)isContr(μ(μ(b 1,b 2),b 3)=μ(b 1,μ(b 2,b 3))))\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:

ϕ c α(c α A)=c α B\phi_{c_\alpha}({c_\alpha}_A) = {c_\alpha}_B

because

(b 1:B) (b 2:B) (b 3:B)isContr(μ(μ(b 1,b 2),b 3)=μ(b 1,μ(b 2,b 3)))\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 AA and BB consists of

  • a monoid homomorphism f:ABf: A \to B
  • a monoid homomorphism f 1:BAf^{-1}: B \to A that is an inverse function of ff.

Structure identity principle for monoids

(…)

Relation to A 3A_3-spaces

Since for all a,b,c:Aa, b, c:A, μ(e,a)=a\mu(e,a)=a, μ(a,e)=a\mu(a,e)=a, and μ(μ(a,b),c)=μ(a,μ(b,c))\mu(\mu(a, b),c)=\mu(a,\mu(b,c)) are contractible, the types

(a:A)μ(e,a)=a\prod_{(a:A)} \mu(e,a)=a
(a:A)μ(a,e)=a\prod_{(a:A)} \mu(a,e)=a
(a:A) (b:A) (c:A)μ(μ(a,b),c)=μ(a,μ(b,c))\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

λ: (a:A)μ(e,a)=a\lambda:\prod_{(a:A)} \mu(e,a)=a
ρ: (a:A)μ(a,e)=a\rho:\prod_{(a:A)} \mu(a,e)=a
α: (a:A) (b:A) (c:A)μ(μ(a,b),c)=μ(a,μ(b,c))\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 $A_3$-space.

Similarly, any 0-truncated A 3A_3-space or A 3A_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:Aa, b, c:A, the identity types μ(e,a)=a\mu(e,a)=a, μ(a,e)=a\mu(a,e)=a, and μ(μ(a,b),c)=μ(a,μ(b,c))\mu(\mu(a, b),c)=\mu(a,\mu(b,c)) are propositions. Since the dependent product types

(a:A)μ(e,a)=a\prod_{(a:A)} \mu(e,a)=a
(a:A)μ(a,e)=a\prod_{(a:A)} \mu(a,e)=a
(a:A) (b:A) (c:A)μ(μ(a,b),c)=μ(a,μ(b,c))\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 3A_3-space, each identity type μ(e,a)=a\mu(e,a)=a, μ(a,e)=a\mu(a,e)=a, and μ(μ(a,b),c)=μ(a,μ(b,c))\mu(\mu(a, b),c)=\mu(a,\mu(b,c)) is an inhabited proposition, which makes it contractible. Thus,

(a:A)isContr(μ(e,a)=a)\prod_{(a:A)} isContr(\mu(e,a)=a)
(a:A)isContr(μ(a,e)=a)\prod_{(a:A)} isContr(\mu(a,e)=a)
(a:A) (b:A) (c:A)isContr(μ(μ(a,b),c)=μ(a,μ(b,c)))\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 3A_3-space is a monoid.

As monoids are A 3A_3-spaces, given monoids AA and BB, for any function

ϕ λ:( (a:A)μ(e A,a)=a)( (b:B)μ(e B,b)=b)\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:

ϕ λ(λ A)=λ B\phi_\lambda(\lambda_A) = \lambda_B

because

(b:B)μ(e B,b)=b\prod_{(b:B)} \mu(e_B,b)=b

is contractible. Likewise, for any function

ϕ ρ:( (a:A)μ(a,e A)=a)( (b:B)μ(b,e B)=b)\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:

ϕ ρ(ρ A)=ρ B\phi_\rho(\rho_A) = \rho_B

because

(b:B)μ(b,e B)=b\prod_{(b:B)} \mu(b,e_B)=b

is contractible, and for any function

ϕ α:( (a 1:A) (a 2:A) (a 3:A)μ(μ(a 1,a 2),a 3)=μ(a 1,μ(a 2,a 3)))( (b 1:B) (b 2:B) (b 3:B)μ(μ(b 1,b 2),b 3)=μ(b 1,μ(b 2,b 3)))\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:

ϕ α(α A)=α B\phi_\alpha(\alpha_A) = \alpha_B

because

(b 1:B) (b 2:B) (b 3:B)μ(μ(b 1,b 2),b 3)=μ(b 1,μ(b 2,b 3))\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 3A_3-spaces.

Examples

  • Every contractible magma is a monoid.

  • The integers are a monoid.

  • Given a set AA, the type of endofunctions AAA \to A has the structure of an monoid, with basepoint id Aid_A, operation function composition.

See also

References

Revision on February 27, 2022 at 00:47:27 by Anonymous?. See the history of this page for a list of all contributions to it.