Kripke Joyal Semantics For Dependent Type Theory
Date:
Abstract: Every topos has an internal higher-order intuitionistic logic. The so-called Kripke–Joyal semantics of a topos gives an interpretation to formulas written in this language used to express ordinary mathematics in that topos. The Kripke–Joyal semantics is in fact a higher order generalization of the well-known Kripke semantic for intuitionistic propositional logic. In this talk I shall report on joint work with Steve Awodey and Nicola Gambino on extending the Kripke–Joyal semantics to dependent type theories, including homotopy type theory.
Slides: Kripke-Joyal semantics for dependent type theory, Pittsburgh’s HoTT Seminar, December 2020
I also gave a talk on the same work in YaMCATS. Here I also explained the standard Beth-Kripke semantics –and how it extend to Kripke-Joyal semantics– since the large audience comprised of very diverse background.
Slides: Kripke-Joyal semantics for dependent type theory, Yorkshire and Midlands Category Theory Seminar, February 2021
And also in CATS seminars at ILLC in Amsterdam in March 2021.