## 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 [[hopf construction|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. ## See also ## [[Synthetic homotopy theory]] [[hopf fibration]] ### On the nlab ### Classically, an [[nLab:H-space]] is a [[nLab:homotopy type]] equipped with the structure of a [[nLab:unitality|unital]] [[nLab:magma]] in the [[nLab:homotopy category]] (only). ## References ## [[HoTT book]] category: homotopy theory