Homotopy Type Theory
Synthetic homotopy theory (Rev #3)

Open problems

See open problems

Useful constructions

• Homotopy pushout $Y \sqcup^X Z$
  • Join? $X * Y$
  • Suspension $\Sigma X$
  • Homotopy fiber?
  • Smash product $X \wedge Y$
• Eilenberg Maclane spaces? $K(G,n)$
• 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(G,n) \|_0$
• loop space of a wedge of circles

Useful references

• On the homotopy groups of spheres in homotopy type theory