[[!redirects Homotopy theory in HoTT]] < [[nlab:synthetic homotopy theory]] +--{.query} *This page is under construction. - Ali* =-- * table of contents {: toc} ## Rough list ## +--{.query} Feel free to add and reorganise. =-- * [[Higher inductive types]] * [[Type families]] $P : A \to \mathcal{U}$ and fibrations $P(\star_A ) \to \sum_{(a:A)}P(a) \to A$ * [[homotopy groups of spheres]] * [[pushout]] $Y \sqcup^X Z$ * [[join]] $ X * Y$ * [[wedge sum]] $X \vee Y$ * [[homotopy fiber]] * [[smash product]] $X \wedge Y$ * [[Eilenberg-MacLane spaces]] $K(G,n)$ * [[localization]] $L X$ * [[cohomology]] $H^n(X;A) \equiv \| X \to K(A,n) \|_0$ * [[Hopf construction]]: [[H-space]] on $A$ gives fibration $A \to A * A \to \Sigma A$ * [[loop space of a wedge of circles]] ## Rational homotopy theory ## * [[rational numbers]] * [[torsion-free divisible group]] * [[rationalization of an abelian group]] * [[rational homotopy type]] * [[rationalization of a simply connected type]] ## Useful references ## * [[On the homotopy groups of spheres in homotopy type theory]], [[Guillaume Brunerie]] * [[On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory]], [[Floris van Doorn]] * [[Higher-Dimensional Types in the Mechanization of Homotopy Theory]], [[Favonia]] * [[HoTT book]] category: homotopy theory,navigation