The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective
Alexandre Buisse, Peter Dybjer · Electronic Notes in Theoretical Computer Science · 2008
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.