On higher inductive types and (Atiyah-Hirzebruch-/Serre-)spectral sequences in homotopy type theory formalized in Lean (cf. cohomology in homotopy type theory and spectral sequences in homotopy type theory):
Floris van Doorn, Spectral (github.com/cmu-phil/Spectral)
Floris van Doorn, On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory (2018) [arXiv:1808.10690]
On $\infty$-groups formalized in homotopy type theory:
Last revised on February 2, 2023 at 14:00:07. See the history of this page for a list of all contributions to it.