Homotopy Type Theory


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


A H-Space consists of


Let AA be a connected? H-space. Then for every a:Aa:A, the maps? μ(a,),μ(,a):AA\mu(a,-),\mu(-,a):A \to A are equivalences?.


Proof. We define μ:S 1S 1S 1\mu : S^1 \to S^1 \to S^1 by circle induction:

μ(base)id S 1ap μfunext(h)\mu(base)\equiv id_{S^1}\qquad ap_{\mu}\equiv funext(h)

where h: x:S 1x=xh : \prod_{x : S^1} x = x is defined in Lemma 6.4.2 of the HoTT book. We now need to show that μ(x,e)=mu(e,x)=x\mu(x,e)=mu(e,x)=x for every x:S 1x : S^1. Showing μ(e,x)=x\mu(e,x)=x is quite simple, the other way requires some more manipulation. Both of which are done in the book.

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


HoTT book

category: homotopy theory