The Groupoid Model of Homotopy Type Theory in Lean4
Published:
My talk at the Prospects of Formal Mathematics at the Hausdorff Institute in Bonn (02 Aug 2024):
This work depends on the formalization of two other projects: Polynomial Functors and Fibred Categories.