{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,17]],"date-time":"2025-12-17T08:38:01Z","timestamp":1765960681767},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642216909"},{"type":"electronic","value":"9783642216916"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21691-6_10","type":"book-chapter","created":{"date-parts":[[2011,6,11]],"date-time":"2011-06-11T01:31:26Z","timestamp":1307755886000},"page":"91-106","source":"Crossref","is-referenced-by-count":6,"title":["The Biequivalence of Locally Cartesian Closed Categories and Martin-L\u00f6f Type Theories"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"10","DOI":"10.2307\/2273784","volume":"50","author":"J. B\u00e9nabou","year":"1985","unstructured":"B\u00e9nabou, J.: Fibred categories and the foundation of naive category theory. Journal of Symbolic Logic\u00a050, 10\u201337 (1985)","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"Cartmell, J.: Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic\u00a032, 209\u2013243 (1986)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1,2","key":"10_CR3","doi-asserted-by":"crossref","first-page":"51","DOI":"10.3233\/FI-1993-191-204","volume":"19","author":"P.-L. Curien","year":"1993","unstructured":"Curien, P.-L.: Substitution up to isomorphism. Fundamenta Informaticae\u00a019(1,2), 51\u201386 (1993)","journal-title":"Fundamenta Informaticae"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs","author":"P. Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 120\u2013134. Springer, Heidelberg (1996)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933.Springer, Heidelberg (1995)"},{"key":"10_CR6","volume-title":"Semantics and Logics of Computation","author":"M. Hofmann","year":"1996","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Pitts, A., Dybjer, P. (eds.) Semantics and Logics of Computation.Cambridge University Press, Cambridge (1996)"},{"key":"10_CR7","volume-title":"Applications of Categorical Algebra, Proceedings of Symposia in Pure Mathematics","author":"F.W. Lawvere","year":"1970","unstructured":"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)"},{"key":"10_CR8","unstructured":"Leinster, T.: Basic bicategories. arXiv:math\/9810017v1 (1999)"},{"key":"10_CR9","first-page":"153","volume-title":"Logic, Methodology and Philosophy of Science, VI, 1979","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Logic, Methodology and Philosophy of Science, VI, 1979, pp. 153\u2013175. North-Holland, Amsterdam (1982)"},{"key":"10_CR10","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"10_CR11","unstructured":"Martin-L\u00f6f, P.: Substitution calculus. Notes from a lecture given in G\u00f6teborg (November 1992)"},{"key":"10_CR12","unstructured":"Mimram, S.: Decidability of equality in categories with families. Report, Magist\u00e8re d\u2019Informatique et Modelisation, \u00c9cole Normale Superieure de Lyon (2004), http:\/\/www.pps.jussieu.fr\/~smimram\/"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. Seely","year":"1984","unstructured":"Seely, R.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.\u00a095(1), 33\u201348 (1984)","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"10_CR14","unstructured":"Tasistro, A.: Formulation of Martin-L\u00f6f\u2019s theory of types with explicit substitutions. Technical report, Department of Computer Sciences, Chalmers University of Technology and University of G\u00f6teborg, Licentiate Thesis (1993)"},{"key":"10_CR15","volume-title":"Practical Foundations of Mathematics","author":"P. Taylor","year":"1999","unstructured":"Taylor, P.: Practical Foundations of Mathematics. Cambridge University Press, Cambridge (1999)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21691-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T19:51:27Z","timestamp":1637783487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21691-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642216909","9783642216916"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21691-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}