{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:22Z","timestamp":1776316942096,"version":"3.50.1"},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2014,4,29]],"date-time":"2014-04-29T00:00:00Z","timestamp":1398729600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2014,12]]},"abstract":"<jats:p>Seely's paper<jats:italic>Locally cartesian closed categories and type theory<\/jats:italic>(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-L\u00f6f type theories with \u03a0, \u03a3 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\u00e9nabou\u2013Hofmann interpretation of Martin-L\u00f6f 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\u00f6f type theories. As a second result, we prove that if we remove \u03a0-types, the resulting categories with families with only \u03a3 and extensional identity types are biequivalent to left exact categories.<\/jats:p>","DOI":"10.1017\/s0960129513000881","type":"journal-article","created":{"date-parts":[[2014,9,3]],"date-time":"2014-09-03T13:03:12Z","timestamp":1409749392000},"source":"Crossref","is-referenced-by-count":20,"title":["The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories"],"prefix":"10.1017","volume":"24","author":[{"given":"PIERRE","family":"CLAIRAMBAULT","sequence":"first","affiliation":[]},{"given":"PETER","family":"DYBJER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,4,29]]},"reference":[{"key":"S0960129513000881_ref19","volume-title":"Practical Foundations of Mathematics","author":"Taylor","year":"1999"},{"key":"S0960129513000881_ref12","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129513000881_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"S0960129513000881_ref2","doi-asserted-by":"publisher","DOI":"10.2307\/2273784"},{"key":"S0960129513000881_ref18","unstructured":"Tasistro A. (1993) Formulation of Martin-L\u00f6f's theory of types with explicit substitutions. Licentiate Thesis. Technical report, Department of Computer Sciences, Chalmers University of Technology and University of G\u00f6teborg."},{"key":"S0960129513000881_ref15","unstructured":"Mimram S. (2004) Decidability of equality in categories with families. Report, Magist\u00e8re d'Informatique et Modelisation, \u00c9cole Normale Superieure de Lyon. Available at http:\/\/www.pps.jussieu.fr\/~smmimram\/."},{"key":"S0960129513000881_ref8","volume-title":"Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics","author":"Lawvere","year":"1970"},{"key":"S0960129513000881_ref1","volume-title":"ACM Conference on Principles of Programming Languages","author":"Abadi","year":"1990"},{"key":"S0960129513000881_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0960129513000881_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022273"},{"key":"S0960129513000881_ref4","doi-asserted-by":"crossref","first-page":"51","DOI":"10.3233\/FI-1993-191-204","article-title":"Substitution up to isomorphism","volume":"19","author":"Curien","year":"1993","journal-title":"Fundamenta Informaticae"},{"key":"S0960129513000881_ref13","unstructured":"Martin-L\u00f6f P. (1986) Amendment to intuitionistic type theory. Notes from a lecture given in G\u00f6teborg."},{"key":"S0960129513000881_ref7","first-page":"79","volume-title":"Semantics and Logics of Computation","author":"Hofmann","year":"1996"},{"key":"S0960129513000881_ref10","first-page":"73","volume-title":"Logic Colloquium '73","author":"Martin-L\u00f6f","year":"1975"},{"key":"S0960129513000881_ref9","unstructured":"Leinster T. (1999) Basic bicategories. arXiv:math\/9810017v1."},{"key":"S0960129513000881_ref16","first-page":"39","volume-title":"Handbook of Logic in Computer Science, Volume 5 \u2013 Algebraic and Logical Structures","author":"Pitts","year":"2000"},{"key":"S0960129513000881_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"S0960129513000881_ref14","unstructured":"Martin-L\u00f6f P. (1992) Substitution calculus. Notes from a lecture given in G\u00f6teborg."},{"key":"S0960129513000881_ref11","first-page":"153","volume-title":"Logic, Methodology and Philosophy of Science, VI, 1979","author":"Martin-L\u00f6f","year":"1982"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000881","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,16]],"date-time":"2022-04-16T05:51:48Z","timestamp":1650088308000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000881\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,29]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["S0960129513000881"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000881","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,29]]},"article-number":"e240606"}}