On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory

Abstract

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.

arXiv commentDissertation, 146 pages

References in corpus (3)

• Homotopy Type Theory in Lean
• Formalization of the fundamental group in untyped set theory using auto2
• Synthetic Homology in Homotopy Type Theory

Cited by in corpus (7)

• All $(\infty ,1)$-toposes have strict univalent universes
• Internal Parametricity for Cubical Type Theory
• Synthetic Homology in Homotopy Type Theory
• The Hurewicz theorem in Homotopy Type Theory
• Synthetic Spectra via a Monadic and Comonadic Modality
• Symmetric Monoidal Smash Products in Homotopy Type Theory
• Computational Synthetic Cohomology Theory in Homotopy Type Theory