Rencontre annuelle GeoCal,
Feb. 15, 2013
Pierre-Louis Curien (CNRS), Revisiting the categorical interpretation of dependent type theory
Schedule
- Feb. 15, 2013, 10:30 - 11:00
Abstract
(travail en commun avec Richard Garner (Macquarie University, Sydney) et Martin Hofmann (Ludwig-Maximilian's-Universität, München)
We relate Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories. As an outcome, we obtain a new proof of the coherence theorem that Curien had proved, which implied that Seely's interpretation in the end was sound.
(exposé en français)