Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
434190 | Theoretical Computer Science | 2014 | 21 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Pierre-Louis Curien, Richard Garner, Martin Hofmann,