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):

Slides

This work depends on the formalization of two other projects: Polynomial Functors and Fibred Categories.

Direct Link