BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Exploring the ∞-categorical semantics of homotopy type theory
DTSTART:20261015T100000
DTEND:20261015T110000
DTSTAMP:20261002T231644Z
UID:16efb3134b1f625e5e28d3041b9d692d7c3db6543d281f2ee80775bc
CATEGORIES:Conferences - Seminars
DESCRIPTION:El Mehdi Cherradi\, IRIF\nThis talk is meant to give an overvi
 ew of the semantics of HoTT in (∞\,1)-categories\, tackling the key chal
 lenge of rigidification: the process of bridging homotopy-coherent notions
  phrased in models of higher categories such as quasicategories\, and thei
 r type-theoretical counterparts that must account for the inherent strictn
 ess of type theory.\nAfter quickly recalling the usual categorical semanti
 cs of extensional Martin-Löf type theory within locally cartesian closed 
 category\, the plan is to present some useful ideas to carry over some of 
 the argument to the higher setting. Specifically\, I will discuss the proc
 ess of turning an elementary higher topos into a model of HoTT\, and sketc
 h important ideas used to prove the internal language conjecture for local
 ly cartesian closed (∞\,1)-categories.\n\n 
LOCATION:CM 1 517 https://plan.epfl.ch/?room==CM%201%20517
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR