[[!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 ### * [[Homotopy pushout]] $Y \sqcup^X Z$ * [[Join]] $ X \star Y$ * [[Suspension]] $\Sigma X$ * [[Wedge sum]] $X \vee Y$ * [[Homotopy fiber]] * [[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 \star 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](https://arxiv.org/abs/1606.05916) 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](http://florisvandoorn.com/papers/dissertation.pdf) 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](https://favonia.org/files/thesis.pdf) Favonia's thesis * Covering spaces * Seifert-van Kampen theorem * Blakers-Massey Theorem * CW complexes * Cellular cohomology category: homotopy theory,navigation