  The goal of this dissertation is to present synthetic homotopy theory in the
setting of homotopy type theory. We will present various results in this
framework, most notably the construction of the Atiyah-Hirzebruch and Serre
spectral sequences for cohomology, which have been fully formalized in the Lean
proof assistant.
