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

Showing changes from revision #4 to #5: Added | Removed | Changed

Open problems

See open problems

Useful Basic constructions notions

• Homotopy pushout?Higher inductive types $Y \sqcup^X Z$
  • Join? $X * Y$
  • Suspension $\Sigma X$
  • Homotopy fiber?
  • Smash product $X \wedge Y$
• Eilenberg Maclane spaces?Type families and fibrations$\mathrm{<span><del\; class="diffmod">\; K</del><ins\; class="diffmod">\; P</ins></span>}<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; :</ins></span>\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; A</ins></span>}<span><del\; class="diffmod">\; ,</del><ins\; class="diffmod">\; \to </ins></span>\mathrm{<span><del\; class="diffmod">\; n</del><ins\; class="diffmod">\; 𝒰</ins></span>})$ K(G,n) P : A \to \mathcal{U}
• James construction $J(X) \simeq \Omega \Sigma X$
• Hopf construction H-space on $A$ gives fibration $A \to A * A \to \Sigma A$
• Localization
• Whitehead product
• Homology?
• Cohomology $H^n(X;A) \equiv \| X \to K(A,n) \|_0$
• loop space of a wedge of circles

Useful references

• On the homotopy groups of spheres in homotopy type theory

  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