The Groupoid Model of Homotopy Type Theory in Lean4

Published:

Slides

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

Direct Link