Projects per year
Abstract
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.
Original language | English |
---|---|
Title of host publication | Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Proceedings |
Place of Publication | Heidelberg |
Publisher | Springer |
Pages | 91-106 |
Number of pages | 16 |
Volume | 6690 LNCS |
ISBN (Electronic) | 978-3-642-21691-6 |
ISBN (Print) | 0302-9743 |
DOIs | |
Publication status | Published - 2011 |
Event | 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, June 1, 2011 - June 3, 2011 - Novi Sad, Serbia Duration: 1 Jan 2011 → … |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Conference
Conference | 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, June 1, 2011 - June 3, 2011 |
---|---|
Country/Territory | Serbia |
City | Novi Sad |
Period | 1/01/11 → … |
Fingerprint
Dive into the research topics of 'The biequivalence of locally cartesian closed categories and martin-löf type theories'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Semantic Structures for Higher-Order Information Flow
Laird, J. (PI)
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council