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-Lof type theories

P. Clairambault ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Mathematical Structures in Computer Science (0960-1295). Vol. 24 (2014), 6, p. Art. no. e240606.
[Artikel, refereegranskad vetenskaplig]

Seely's paper Locally cartesian closed categories and type theory (Seely 1984) 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 Pi, Sigma 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 Pi-types, the resulting categories with families with only Sigma and extensional identity types are biequivalent to left exact categories.

Nyckelord: Computer Science, Theory & Methods

Denna post skapades 2014-12-05.
CPL Pubid: 207500


Läs direkt!

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

Institutioner (Chalmers)

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


Datavetenskap (datalogi)

Chalmers infrastruktur