Homotopy Type Theory Synthetic homotopy theory > history (Rev #18, changes)

Showing changes from revision #17 to #18: Added | Removed | Changed

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

  • homotopy cofiber?

  • smash product $X \wedge Y$

  $K(G,n)$
• Eilenberg-MacLane James spaces construction $\mathrm{<span><del\; class="diffmod">\; K</del><ins\; class="diffmod">\; J</ins></span>}(\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; X</ins></span>},n)\simeq \Omega \Sigma X$ K(G,n) J(X) \simeq \Omega \Sigma X
• James localization construction $\mathrm{<span><del\; class="diffmod">\; J</del><ins\; class="diffmod">\; L</ins></span>}(X)\simeq \Omega \Sigma X$ J(X) L \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

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