Homotopy Type Theory A3-space > history (Rev #10)


Sometimes we can equip a type with a certain structure, called an A 3A_3-algebra structure, allowing us to derive some nice properties about the type and 0-truncate it to form monoids.


An A 3A_3-space or A 3A_3-algebra in homotopy types or H-monoid 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))

Homomorphisms of A 3A_3-spaces

A homomorphism of A 3A_3-spaces between two A 3A_3-spaces 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))
  • A 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)

such that the left unitor is preserved:

ϕ λ(λ A)=λ B\phi_\lambda(\lambda_A) = \lambda_B
  • A 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)

such that the right unitor is preserved:

ϕ ρ(ρ A)=ρ B\phi_\rho(\rho_A) = \rho_B
  • A 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)

such that the associator is preserved:

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


  • The integers are an A 3A_3-space.

  • Every loop space is naturally an A 3A_3-space with path concatenation as the operation. In fact every loop space is a group.

  • The type of endofunctions AAA \to A has the structure of an A 3A_3-space, with basepoint id Aid_A, operation function composition.

  • A monoid is a 0-truncated A 3A_3-space.

See also

On the nlab

Classically, an A3-space is a homotopy type equipped with the structure of a monoid in the homotopy category (only).

Revision on April 26, 2022 at 03:06:39 by Anonymous?. See the history of this page for a list of all contributions to it.