About me

I work on proof assistants and semantics of dependent type theories.

Currently, I am a PhD student at Carnegie Mellon University, supervised by Steve Awodey. My thesis will be written on the semantics of groupoid and cubical quotients in models of HoTT.

Teaching resources

• Logic and Proof

  I updated the textbook Logic and Proof by Jeremy Avigad, Robert Lewis, and Floris van Doorn to Lean4, for teaching the course Logic and Mathematical Inquiry at CMU (summer of 2024). Available at leanprover-community.github.io/logic_and_proof.

• The HoTT Game

  I designed a guided introduction to synthetic homotopy theory in Cubical Agda. Available at thehottgameguide.readthedocs.io.

Talks and publications

• HoTTLean at TYPES 2025

  Constructing a proof assistant HoTTLean within Lean, allowing users to apply synthetic reasoning to mathematical objects such as groupoids. Repository, extended abstract, slides, talk.

• Cubical quotients at MURI meeting 2025

  Defining quotients of (Cartesian) cubical objects; classifying higher kernels of cubical quotients as Segal (groupoid) cubical objects. Slides

• Fibrant Inductive Types from Universal Monads at CMU HoTT Seminar 2024

  Assuming an algebraic fibration structure on cubical sets, prove the existence of fibrant W-types over a fibrant signature. Abstract

• Higher inductive types in cartesian cubical sets at CMU HoTT Seminar 2024

  Demonstrate how basic higher inductive types can be constructed in the category of cubical sets. Abstract

• Ax-Grothendieck at Lean Summer Projects 2021

  Formalizing model theory and Ax-Grothendieck in Lean. Talk