TY - JOUR
T1 - Revisiting the categorical interpretation of dependent type theory
AU - Curien, Pierre Louis
AU - Garner, Richard
AU - Hofmann, Martin
PY - 2014/8/21
Y1 - 2014/8/21
N2 - We show that 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, 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.
AB - We show that 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, 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.
UR - http://www.scopus.com/inward/record.url?scp=84926689015&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2014.03.003
DO - 10.1016/j.tcs.2014.03.003
M3 - Article
AN - SCOPUS:84926689015
SN - 0304-3975
VL - 546
SP - 99
EP - 119
JO - Theoretical Computer Science
JF - Theoretical Computer Science
ER -