## 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]]. **Proof.** We define $\mu : S^1 \to S^1 \to S^1$ by circle induction: $$\mu(base)\equiv id_{S^1}\qquad ap_{\mu}\equiv funext(h)$$ where $h : \prod_{x : S^1} x = x$ is defined in Lemma 6.4.2 of the [[HoTT book]]. We now need to show that $\mu(x,e)=mu(e,x)=x$ for every $x : S^1$. Showing $\mu(e,x)=x$ is quite simple, the other way requires some more manipulation. Both of which are done in the book. * 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