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 Michail Karatarakis
A Computable Lean 4 Mechanization of GNNs in Monoidal Locoses
with Peter Lumsdaine
Mechanization of Essentially Algebraic Theories in Arithmetic Universes (Rocq and Lean 4)
Watch Peter's talk at Itaca Fest 2025
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