BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:HoTTLean: Semantics of HoTT in Lean - Steve Awodey (Royal Society 
 Wolfson Visiting Fellow at Cambridge CST)
DTSTART:20260212T170000Z
DTEND:20260212T180000Z
UID:TALK243271@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:This is the first of two related talks\, the second of which b
 y Wojciech Nawrocki will be on SynthLean and other formalization aspects o
 f HoTTLean.\nThe following summary is from the ReadMe of the HoTTLean proj
 ect\, which is here https://github.com/sinhp/HoTTLean.\n\nHoTTLean is a Le
 an formalization of the groupoid model of homotopy type theory\, as well a
 s of category-theoretic models of Martin-Löf type theories in general\, t
 ogether with a proof mode for developing mathematics synthetically in thos
 e type theories. HoTTLean is work-in-progress.\nIt currently contains the 
 following components:\n\n    • A deep embedding of MLTT syntax with Π\,
  Σ\, Id types\, and base constants (HoTTLean.Syntax).\n\n    • SynthLea
 n\, a proof assistant for these deeply embedded theories (HoTTLean.Fronten
 d). It includes a certifying typechecker (HoTTLean.Typechecker).\n\n    
 • Natural model semantics of MLTT in presheaf categories (HoTTLean.Model
 ) and a proof that this semantics is sound for the syntax (ofType_ofTerm_s
 ound).\n\n    • A sorry-free construction of the groupoid model of type 
 theory with Π\, Σ\, Id types (HoTTLean.Groupoids).\n\n    • Pieces of 
 general mathematics and category theory such as the Grothendieck construct
 ion for groupoids (HoTTLean.ForMathlib\, HoTTLean.Grothendieck\, HoTTLean.
 Pointed). These are being upstreamed to Mathlib.\n\n=== Hybrid talk ===\n\
 nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuT
 ideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR