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

Idea

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

Definition

An $A_3$-space or $A_3$-algebra in homotopy types or H-monoid consists of

• A type $A$,
• A basepoint $e:A$
• A binary operation $\mu : A \to A \to A$
• A left unitor
  $$\lambda:\prod_{(a:A)} \mu(e,a)=a$$
• A right unitor
  $$\rho:\prod_{(a:A)} \mu(a,e)=a$$
• An asssociator
  $$\alpha:\prod_{(a:A)} \prod_{(b:A)} \prod_{(c:A)} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$

Homomorphisms of $A_3$-spaces

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

• A function

such that the left unitor is preserved:

• A function

such that the right unitor is preserved:

• A function

such that the associator is preserved:

Examples

• The integers are an $A_3$-space.

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

• The type of endofunctions $A \to A$ has the structure of an $A_3$-space, with basepoint $id_A$, operation function composition.

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

See also

• Synthetic homotopy theory
• H-space
• commutative A3-space
• grouplike A3-space
• monoid

On the nlab

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