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