HoTTLean: Semantics of HoTT in Lean

Add to your list(s) Download to your calendar using vCal

• Steve Awodey (Royal Society Wolfson Visiting Fellow at Cambridge CST)
• Thursday 12 February 2026, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• Martin's interesting talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.