Projects per year
Abstract
Seely's paper Locally cartesian closed categories and type theory contains a wellknown result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of MartinLof 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 BenabouHofmann interpretation of MartinLof type theory in locally cartesian closed categories yields a biequivalence of 2categories. To facilitate the technical development we employ categories with families as a substitute for syntactic MartinLof 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  91106 
Number of pages  16 
Volume  6690 LNCS 
ISBN (Electronic)  9783642216916 
ISBN (Print)  03029743 
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 martinlöf type theories'. Together they form a unique fingerprint.Projects
 1 Finished

Semantic Structures for HigherOrder Information Flow
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council