[[!redirects Homotopy theory in HoTT]] +--{.query} *This page is under construction. - Ali* =-- * table of contents {: toc} ## Open problems ## See [[open problems]] ## 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$ * [[suspension]] $\Sigma X$ * [[wedge sum]] $X \vee Y$ * [[homotopy fiber]] * [[homotopy cofiber]] * [[smash product]] $X \wedge Y$ * [[Eilenberg-MacLane spaces]] $K(G,n)$ * [[James construction]] $J(X) \simeq \Omega \Sigma X$ * [[localization]] $L X$ * [[homology]] * [[cohomology]] $H^n(X;A) \equiv \| X \to K(A,n) \|_0$ * [[spectral sequences]] * [[Hopf construction]]: [[H-space]] on $A$ gives fibration $A \to A * A \to \Sigma A$ * [[Whitehead product]] * [[loop space of a wedge of circles]] * [[spectrum]] * [[Gysin sequence]] * [[Hopf invariant]] * [[Mayer-Vietoris sequence]] * [[Blakers-Massey Theorem]] * [[Serre spectral sequence]] * [[AtiyahâHirzebruch spectral sequence]] * [[Seifert-van Kampen theorem]] * [[CW complex]] * [[Cellular cohomology]] * [[covering space]] ## Rational homotopy theory ## * [[rational numbers]] * [[torsion-free divisible group]] * [[rationalization of an abelian group]] * [[rational homotopy type]] * [[rationalization of a simply connected type]] * [[rational cohomology]] * [[rational homology]] ## Spaces ## * [[circle]] * [[spheres]] * [[interval]] * [[real projective space]] ## 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