Sina Hazratpour: Formalizing the meta-theory of HoTT in Lean 4

Abstract

This is a report on a new collaborative project on bringing HoTT to Lean4. I will talk about the formalization of the groupoid model of HoTT in Lean4, and the steps toward translation of results of HoTT into classical results about groupoids in Lean4. As future goals, we aim to extend this framework to the simplicial model of HoTT in Lean, with the long-term goal of extending it to the \(\infty\)-toposes model.

For more details, see our project documentation: https://sinhp.github.io/groupoid_model_in_lean4/