Advertisement

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

  • Pierre Clairambault
  • Peter Dybjer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)

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-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.

Keywords

Type Theory Natural Transformation Identity Type Lambda Calculus Terminal Object 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bénabou, J.: Fibred categories and the foundation of naive category theory. Journal of Symbolic Logic 50, 10–37 (1985)CrossRefzbMATHGoogle Scholar
  2. 2.
    Cartmell, J.: Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic 32, 209–243 (1986)CrossRefzbMATHGoogle Scholar
  3. 3.
    Curien, P.-L.: Substitution up to isomorphism. Fundamenta Informaticae 19(1,2), 51–86 (1993)zbMATHGoogle Scholar
  4. 4.
    Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120–134. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  5. 5.
    Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933.Springer, Heidelberg (1995)CrossRefGoogle Scholar
  6. 6.
    Hofmann, M.: Syntax and semantics of dependent types. In: Pitts, A., Dybjer, P. (eds.) Semantics and Logics of Computation.Cambridge University Press, Cambridge (1996)Google Scholar
  7. 7.
    Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics. AMS, Providence (1970)Google Scholar
  8. 8.
    Leinster, T.: Basic bicategories. arXiv:math/9810017v1 (1999)Google Scholar
  9. 9.
    Martin-Löf, P.: Constructive mathematics and computer programming. In: Logic, Methodology and Philosophy of Science, VI, 1979, pp. 153–175. North-Holland, Amsterdam (1982)Google Scholar
  10. 10.
    Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)Google Scholar
  11. 11.
    Martin-Löf, P.: Substitution calculus. Notes from a lecture given in Göteborg (November 1992)Google Scholar
  12. 12.
    Mimram, S.: Decidability of equality in categories with families. Report, Magistère d’Informatique et Modelisation, École Normale Superieure de Lyon (2004), http://www.pps.jussieu.fr/~smimram/
  13. 13.
    Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc. 95(1), 33–48 (1984)CrossRefzbMATHGoogle Scholar
  14. 14.
    Tasistro, A.: Formulation of Martin-Löf’s theory of types with explicit substitutions. Technical report, Department of Computer Sciences, Chalmers University of Technology and University of Göteborg, Licentiate Thesis (1993)Google Scholar
  15. 15.
    Taylor, P.: Practical Foundations of Mathematics. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Pierre Clairambault
    • 1
  • Peter Dybjer
    • 1
  1. 1.University of Bath and Chalmers University of TechnologySweden

Personalised recommendations