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

Idea

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.

Definition

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))

Examples

  • 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 February 4, 2022 at 06:00:30 by Anonymous?. See the history of this page for a list of all contributions to it.