Research

This book tracks my current research goals and progress.

• Git repository

Current research: Formalizing spectral sequences in cubical Agda.

Resources

I have scaled down some of these materials to eBook size, for easier reading on mobile phones. The original full PDFs are linked as well.

• Homotopy Type Theory Book [ebook-sized pdf]
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, by Floris van Doorn (2018) [ebook-sized pdf] [original pdf]
• A Concise Course in Algebraic Topology, by J.P. May (2007) [ebook-sized pdf] [original pdf]
• Cubical Type Theory: a constructive interpretation of the univalence axiom (CCHM) (2015) [ebook-sized pdf] [original pdf]