(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)