Synthetic Homotopy Theory

The goal of this dissertation is to present results from synthetic homotopy theory based on homotopy type theory (HoTT). After an introduction to Martin-Löf’s dependent type theory and homotopy type theory, key results include a synthetic construction of the Hopf fibration, a proof of the Blakers–Massey theorem, and a derivation of the Freudenthal suspension theorem, with calculations of some homotopy groups of $n$-spheres.