Homotopy Type Theory monoid > history (Rev #6)

Definition

A monoid or A 3A_3-algebra in sets consists of

  • A type AA,
  • A basepoint e:Ae:A
  • A binary operation μ:AAA\mu : A \to A \to A
  • A left unitor
    λ: (a:A)μ(e,a)=a\lambda:\prod_{(a:A)} \mu(e,a)=a
  • A right unitor
    ρ: (a:A)μ(a,e)=a\rho:\prod_{(a:A)} \mu(a,e)=a
  • An asssociator
    α: (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))
  • A 0-truncator
    τ 0: (a:A) (b:A) (c:a=b) (d:a=b) (x:c=d) (y:c=d)x=y\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

Homomorphisms of monoids

A homomorphism of monoids 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 monoid AA, the 0-truncator means that the identity types between any two terms of AA are propositions, and thus 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 propositions, and thus contractible because they are inhabited by definition of a monoid.

As a result, 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 homomorphism of monoids is also a homomorphism of A 3A_3-spaces. Finally, the 0-truncator is always preserved in a function between two sets.

Examples

  • 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 13, 2022 at 20:01:38 by Anonymous?. See the history of this page for a list of all contributions to it.