I'm a second year PhD student at the University of Western Ontario interested in all things mathematical logic, especially if category theory and (homotopy) type theory are involved. My supervisor is Dan Christensen. Before that, I wrote my master's thesis on simplicial homotopy type theory at the University of Bonn, supervised by Nima Rasekh and Floris van Doorn. This is the "finished" product.
For more details, here's my website.
- I am currently contributing to the Coq-HoTT library.
- As part of my master's thesis project I started working with Rzk, a proof assistant designed for synthetic ∞-catrgories. Everything I'm doing with it is here. I recently started an experimental Rzk project about 2-Segal types. It's just like Segal types, only the combinatorics are worse in every way and it's not as useful. Convinced yet?
- I've worked with Lean for a course taught by Floris van Doorn in Bonn and formalised Fodor's lemma, a set-theoretic property of a special class of "big" sets. I am certainly not the only person who has done this.
- Introductory notes on equivariant orthogonal spectra, for a graduate seminar in Bonn.
- Together with Kunhong Du and Tim Lichtnau, we gave a series of introductory talks on topics in homotopy type theory, as part of our thesis work. Here are the notes.