The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theory with Pi, Sigma, and Extensional Identity Types

Photograph of Pierre Clairambault

Pierre Clairambault

(University of Bath)

(Joint work with Peter Dybjer)

In his paper Locally cartesian closed categories and type theory (1984), Robert Seely presented a proof that the category LCC of locally cartesian closed categories and the category ML of syntactically presented Martin-Löf type theories (with Pi, Sigma, and extensional identity types) are equivalent. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks in categories. In his paper "Substitution up to isomorphism" Curien (1993) shows that Seely's problem is essentially a coherence problem and proposed how to solve this problem using cut-elimination. An alternative interpretation was then proposed by Hofmann (1994) based on a method due to Benabou. However, neither Curien nor Hofmann showed that their respective interpretations lead to an equivalence between LCC and ML. In this paper we show that Hofmann's interpretation functor gives rise to a biequivalence of 2-categories, and claim that this is the appropriate formulation of Seely's theorem. We replace ML with a categorical analogue CWFLCC of categories with families (with extensional identity types, and Sigma and Pi-types) which are democratic in the sense that each context is represented by a closed type. Most of the difficulty of this proof already appears when relating categories with finite limits (without assuming local cartesian closure) and categories with families without Pi-types. We therefore present this biequivalence (of the 2-categories FL and CWFFL) separately.

Thursday 14th October 2010, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science