HoTTLean: Formalizing the Meta-Theory of HoTT in Lean 4
Published in Types 2025, 2025
with Steve Awodey, Mario Carneiro, Joseph Hua, Wojciech Nawrocki, Spencer Woolfson
Publications
A 2-categorical proof of Frobenius for fibrations defined from a generic point
Published in Mathematical Structures in Computer Science, 2024
with Emily Riehl
Kripke-Joyal forcing for type theory and uniform fibrations
Published in Selecta Mathematica, Volume 30, No. 7, 2024
with Steve Awodey and Nicola Gambino
Fibration of contexts beget fibrations of toposes
Published in Theory and Application of Categories (TAC), 2020
Joint with Steve Vickers
PhD Thesis
Published in University of Birmingham (UK), 2019
Under supervision of Steve Vickers