Homotopy Type Theory Synthetic homotopy theory > history (Rev #6)

Open problems

See open problems

Basic notions

• Higher inductive types
• Type families and fibrations $P : A \to \mathcal{U}$ type family

Constructions and concepts

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

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