HoTTLean: Formalizing the Meta-Theory of HoTT in Lean 4
Presented in Types 2025
Download Paper Cite Paper Lean blueprint Code
Research
Work in Progress 🛠️
with Peter Lumsdaine
Gödel's Incompleteness Theorems in Lean 4
A Lean blueprint for Gödel's incompleteness theorems and its categorification in Arithmetic Universes
Code
Selected Publications
You can find the full list of my articles on my Google Scholar profile.
A 2-categorical proof of Frobenius for fibrations defined from a generic point
with Emily Riehl
Published in Mathematical Structures in Computer Science
Download Paper Cite Paper arXiv:2210.00078
Kripke-Joyal forcing for type theory and uniform fibrations
with Steve Awodey, Nicola Gambino
Published in Selecta Mathematica
Download Paper Cite Paper arXiv:2110.14576
Fibration of contexts beget fibrations of toposes
with Steve Vickers
Published in Theory and Application of Categories (TAC)
Download Paper Cite Paper arXiv:1808.08291
A logical study of some 2-categorical aspects of topos theory (PhD Thesis)
University of Birmingham (UK)
Download Paper