CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories

P. Clairambault ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Lecture Notes in Computer Science. 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, Novi Sad,1-3 June 2011 (0302-9743). Vol. 6690 (2011), p. 91-106.
[Konferensbidrag, refereegranskat]

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-Löf 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 Bénabou-Hofmann interpretation of Martin-Löf 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-Löf type theories. As a second result we prove that if we remove Π-types the resulting categories with families are biequivalent to left exact categories.



Denna post skapades 2012-02-10.
CPL Pubid: 154997

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)

Ämnesområden

Information Technology

Chalmers infrastruktur