The biequivalence of locally cartesian closed categories and martin-löf type theories

Pierre Clairambault, Peter Dybjer

Research output: Chapter in Book/Report/Conference proceedingChapter

10 Citations (SciVal)

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 languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Proceedings
Place of PublicationHeidelberg
PublisherSpringer
Pages91-106
Number of pages16
Volume6690 LNCS
ISBN (Electronic)978-3-642-21691-6
ISBN (Print)0302-9743
DOIs
Publication statusPublished - 2011
Event10th 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

NameLecture Notes in Computer Science
PublisherSpringer Verlag

Conference

Conference10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, June 1, 2011 - June 3, 2011
Country/TerritorySerbia
CityNovi Sad
Period1/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.

Cite this