TY - CHAP
T1 - The biequivalence of locally cartesian closed categories and martin-löf type theories
AU - Clairambault, Pierre
AU - Dybjer, Peter
PY - 2011
Y1 - 2011
N2 - Seely's paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Lof type theories with , , and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Benabou-Hofmann interpretation of Martin-Lof type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Lof type theories. As a second result we prove that if we remove -types the resulting categories with families are biequivalent to left exact categories.
AB - Seely's paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Lof type theories with , , and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Benabou-Hofmann interpretation of Martin-Lof type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Lof type theories. As a second result we prove that if we remove -types the resulting categories with families are biequivalent to left exact categories.
UR - http://dx.doi.org/10.1007/978-3-642-21691-6_10
U2 - 10.1007/978-3-642-21691-6_10
DO - 10.1007/978-3-642-21691-6_10
M3 - Chapter
SN - 0302-9743
VL - 6690 LNCS
T3 - Lecture Notes in Computer Science
SP - 91
EP - 106
BT - Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Proceedings
PB - Springer
CY - Heidelberg
T2 - 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, June 1, 2011 - June 3, 2011
Y2 - 1 January 2011
ER -