Abstract

This is the first of two related talks, the second of which by Wojciech Nawrocki will be on SynthLean and other formalization aspects of HoTTLean. The following summary is from the ReadMe of the HoTTLean project, which is here https://github.com/sinhp/HoTTLean.

HoTTLean is a Lean formalization of the groupoid model of homotopy type theory, as well as of category-theoretic models of Martin-Löf type theories in general, together with a proof mode for developing mathematics synthetically in those type theories. HoTTLean is work-in-progress. It currently contains the following components:

• A deep embedding of MLTT syntax with Π, Σ, Id types, and base constants (HoTTLean.Syntax).

• SynthLean, a proof assistant for these deeply embedded theories (HoTTLean.Frontend). It includes a certifying typechecker (HoTTLean.Typechecker).

• Natural model semantics of MLTT in presheaf categories (HoTTLean.Model) and a proof that this semantics is sound for the syntax (ofType_ofTerm_sound).

• A sorry-free construction of the groupoid model of type theory with Π, Σ, Id types (HoTTLean.Groupoids).

• Pieces of general mathematics and category theory such as the Grothendieck construction for groupoids (HoTTLean.ForMathlib, HoTTLean.Grothendieck, HoTTLean.Pointed). These are being upstreamed to Mathlib.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk