Revisiting the categorical interpretation of dependent type theory

摘要

We show that Hofmann's and Curien's interpretations of Martin-Lof'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, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.