[[!redirects Homotopy theory in HoTT]] +--{.query} *This page is under construction. - Ali* =-- * table of contents {: toc} ## Open problems ## See [[open problems]] ## Basic notions ## * [[Higher inductive types]] * [[Type families]] $P : A \to \mathcal{U}$ and fibrations $P(\star_A ) \to \sum_{(a:A)}P(a) \to A$ ## Constructions and concepts ## ### Homotopy groups### * [[homotopy groups of spheres]] ### Spaces ### * [[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]] ### Homological Algebra ### * [[homology]] * [[cohomology]] $H^n(X;A) \equiv \| X \to K(A,n) \|_0$ * [[spectral sequences]] ### Fibrations ### * [[Hopf construction]]: [[H-space]] on $A$ gives fibration $A \to A * A \to \Sigma A$ ### Misc. ### * [[Whitehead product]] * [[loop space of a wedge of circles]] +--{.query} I would like to include some articles about spectra here. This would probably absorb homological algeba. Floris van Doorn's thesis should be a good start. - Ali =-- ## Useful references ## * [[On the homotopy groups of spheres in homotopy type theory]] Guillaume Brunerie's thesis. Covers: * [[Sequential colimit]] * [[James construction]] * [[Whitehead product]] * [[Smash product]] and it's monoidal structure * [[Cohomology]] rings * [[Mayer-Vietoris sequence]] * [[Hopf invariant]] * [[Gysin sequence]] * Computation of $\pi_4(S^3)=\mathbb{Z}/n\mathbb{Z}$ and later $n=2$. * [[On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory]] Floris van Doorn's thesis * [[Eilenberg-Maclane spaces]] * [[Smash product]] and it's monoidal structure * [[Spectral sequence]] * Serre spectral sequence * Spectral sequence for Cohomology * Spectral sequence for Homology * Computations of cohomology of spheres * [[Spectra]] * Generalised cohomology theories * [[Higher-Dimensional Types in the Mechanization of Homotopy Theory]] Favonia's thesis * Covering spaces * Seifert-van Kampen theorem * Blakers-Massey Theorem * CW complexes * Cellular cohomology category: homotopy theory,navigation