The biequivalence of locally cartesian closed categories and martin-lof type theories


Clairambault, P. and Dybjer, P., 2011. The biequivalence of locally cartesian closed categories and martin-lof type theories. In: Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Proceedings.Vol. 6690 LNCS. Heidelberg: Springer, pp. 91-106. (Lecture Notes in Computer Science)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Book Sections
CreatorsClairambault, P.and Dybjer, P.
DepartmentsFaculty of Science > Computer Science
ID Code25001
Additional Information10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011. 1-3 June 2011. Novi Sad, Serbia.


Actions (login required)

View Item