Thursday 30 March 2023, 14:00, room 1Z34: (∞-)Categorical semantic of type theory: an introduction, El Mehdi Cherradi (IRIF).

The well-known Curry-Howard correspondence admits an extension, due to Lambek, further connecting proofs and programs to certain classes of categories. As such, from the perspective that category theory provides a foundational framework for reasoning and logic, it is interesting to identify the underlying categorical structure of models of a given type theory. The backbone of the correspondence is fairly well-understood for extensional flavors of type theory, notably following the work of Hofmann. However, the study of homotopy type theory counterparts is more recent and still incomplete. The goal of the talk is to sketch the basics of the so-called categorical semantic of type theory, and to hint at the ∞-categorical one towards which my PhD thesis aims at contributing.