کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422039 | 685008 | 2008 | 12 صفحه PDF | دانلود رایگان |

We give an intuitionistic view of Seely's interpretation of Martin-Löf's intuitionistic type theory in locally cartesian closed categories. The idea is to use Martin-Löf type theory itself as metalanguage, and E-categories, the appropriate notion of categories when working in this metalanguage. As an E-categorical substitute for the formal system of Martin-Löf type theory we use E-categories with families (E-cwfs). These come in two flavours: groupoid-style E-cwfs and proof-irrelevant E-cwfs. We then analyze Seely's interpretation as consisting of three parts. The first part is purely categorical: the interpretation of groupoid-style E-cwfs in E-locally cartesian closed categories. (The key part of this interpretation has been type-checked in the Coq system.) The second is a coherence problem which relates groupoid-style E-cwfs with proof-irrelevant ones. The third is a purely syntactic problem: that proof-irrelevant E-cwfs are equivalent to traditional lambda calculus based formulations of Martin-Löf type theory.
Journal: Electronic Notes in Theoretical Computer Science - Volume 218, 22 October 2008, Pages 21-32