Homotopy Type Theory H-space (Rev #7)

Idea

Sometimes we can equip a type with a certain structure, called a H-space, allowing us to derive some nice properties about the type or even construct fibrations

Definition

A H-Space 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$

Properties

Let $A$ be a connected? H-space. Then for every $a:A$, the maps? $\mu(a,-),\mu(-,a):A \to A$ are equivalences?.

Examples

• There is a H-space structure on the circle. See Lemma 8.5.8 of the HoTT book. (TODO: Write out construction).

• Every loop space is naturally a H-space with path concatenation as the operation. In fact every loop space is a group?.

• The type of maps? $A \to A$ has the structure of a H-space, with basepoint $id_A$, operation function composition.

On the nlab

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

References

HoTT book

category: homotopy theory

Revision on January 1, 2019 at 20:51:23 by Ali Caglayan. See the history of this page for a list of all contributions to it.