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

Definition

An $A_3$-space or H-monoid consists of

• A type $A$,
• A basepoint $e:A$
• A binary operation $\mu : A \to A \to A$
• for every $a:A$, equalities $\mu(e,a)=a$ and $\mu(a,e)=a$
• for every $a:A$, $b:A$, $c:A$, an equality $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$

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

On the nlab

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