nLab Floris van Doorn (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

• webpage

Selected writings

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](https://arxiv.org/abs/1808.10690)]

On $\infty$-groups formalized in homotopy type theory:

• Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Higher Groups in Homotopy Type Theory, LICS ‘18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018) 205-214 [[arXiv:1802.04315](https://arxiv.org/abs/1802.04315), doi:10.1145/3209108.3209150]

Related entries

• Lean

• spectral sequence, Serre spectral sequence