Homotopy Type Theory Synthetic homotopy theory (Rev #17, changes)

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

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

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 $K(G,n)$
• James construction $J(X) \simeq \Omega \Sigma X$
• localization

Fibrations

• Hopf construction: H-space on $A$ gives fibration $A \to A * A \to \Sigma A$

Misc.

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

Revision on October 17, 2018 at 10:40:39 by Ali Caglayan. See the history of this page for a list of all contributions to it.