Hi there! 👋

I'm a mathematician and computer scientist, working in their intersection: Using ideas from CS to make the practice of mathematics better, and using ideas from mathematics to make the practice of CS better.

• 🧊 My current passion project is the 1Lab, a free and open-source online introductory and reference resource for univalent mathematics done in Cubical type theory. In addition to being the only long-form introduction to formalised Cubical type theory, work pioneered in the 1lab has spun off into being the state of the art in Agda publishing.

• 📚 On my off-time, I'm working on Cubical Methods for Homotopy Type Theory, a traditional-format textbook on the applications of cubical type theory to HoTT, with a focus towards its applications to homotopy-coherent category theory.

• 👩‍🏫 I'm one of the teaching assistants for the HoTTEST Summer School 2022, which has been an endless source of joy and a fantastic opportunity to help share my passion for type theory with others.

• 👩‍🔬 I contribute to @EgbertRijke's agda-unimath library, in particular around the applications of univalent mathematics outside of pure mathematics. Our current research has been focused on the representation of hydrocarbons as homotopy types.

• ⏪ In my senior year of high school I implemented the type checker for the Amulet programming language, a functional programming language with support for closed type families, type classes with functional dependencies, GADTs, and "quick look" impredicative typing. The rest of the compiler was joint work with @SquidDev, one of my closest friends.

• ⏪ As practice, I wrote my own implementation of CCHM cubical type theory, with complete support for univalence and higher inductive types (higher inductive types in the style of CHM, with comp split into hcomp and transp), and formalised the proof that π₁(S¹) ≃ Z as a stress test.

Your support would mean being able to dedicate more of my time to type theory, in particular working on:

• Maintainer-ship of the 1Lab: we have several outstanding formalisation projects (in univalent category theory, bicategory theory, homological algebra, topos theory, and synthetic homotopy theory) which stagnated as a result of recovering from COVID.

  Additionally, I'd like to polish and split off the 1Lab's build system so that anyone can deploy their own websites based on Agda. I've done this for the HoTTEST Summer School Agda lecture notes, but in an ad-hoc way which can not be easily re-used.

• Cubical Methods. I have hardly enough material to publish as a blog post, let alone a textbook! My roadmap for the book (which will eventually live on the repository) is to have a structure similar to the 2013 HoTT book, where the first half deals with foundational results and the latter half deals with concrete mathematical applications.

• More time for original research in HoTT 🙂