Showing changes from revision #6 to #7: Added | Removed | Changed

Idea

H-spaces Sometimes are we simply can types equip equipped with the structure of a magma (from classical Algebra). They are useful classically in constructing fibrations.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 ofH-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$connected? , the H-space. maps Then for every$\mu (a,-),\mu (-,a):A\to A$ \mu(a,-),\mu(-,a):A a:A \to A , are the equivalences.maps? $\mu(a,-),\mu(-,a):A \to A$ are equivalences.

See also

Synthetic homotopy theory hopf fibration

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