I work on semantics of dependent type theories.

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.

I am a Lean enjoyer. I am working on HoTTLean, where we formalize the semantics of HoTT0 in Lean, and build an interpretation of a HoTT0 proof assistant within Lean into those semantics.