This page is under construction. - Ali
See open problems
Feel free to add and reorganise.
Type families $P : A \to \mathcal{U}$ and fibrations $P(\star_A ) \to \sum_{(a:A)}P(a) \to A$
pushout $Y \sqcup^X Z$
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$
Hopf construction: H-space on $A$ gives fibration $A \to A * A \to \Sigma A$
Gysin sequence?
Hopf invariant?
Mayer-Vietoris sequence?
Blakers-Massey Theorem?
Serre spectral sequence?
Atiyah–Hirzebruch spectral sequence?
CW complex?
Cellular cohomology?
covering space?
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
Revision on January 19, 2019 at 13:41:06 by Ali Caglayan. See the history of this page for a list of all contributions to it.