## 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$ * A left unitor $$\lambda:\prod_{(a:A)} \mu(e,a)=a$$ * A right unitor $$\rho:\prod_{(a:A)} \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. * An [[A3-space]] $A$ is an H-space with an equality $\mu(\mu(a, b),c)=\mu(a,\mu(b,c))$ for every $a:A$, $b:A$, $c:A$ representing associativity up to homotopy. * A unital magma is a 0-truncated H-space. ## See also ## * [[Higher algebra]] * [[Synthetic homotopy theory]] * [[hopf fibration]] * [[unital Z-algebra]] * [[H-spaceoid]] ### 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