{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T03:42:09Z","timestamp":1649043729104},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2021,9,20]],"date-time":"2021-09-20T00:00:00Z","timestamp":1632096000000},"content-version":"unspecified","delay-in-days":142,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,5]]},"abstract":"Abstract<\/jats:title>\n\t Locally cartesian closed (lcc) categories are natural categorical models of extensional dependent type theory. This paper introduces the \u201cgros\u201d semantics in the category of lcc categories: Instead of constructing an interpretation in a given individual lcc category, we show that also the category of all lcc categories can be endowed with the structure of a model of dependent type theory. The original interpretation in an individual lcc category can then be recovered by slicing. As in the original interpretation, we face the issue of coherence: Categorical structure is usually preserved by functors only up to isomorphism, whereas syntactic substitution commutes strictly with all type-theoretic structures. Our solution involves a suitable presentation of the higher category of lcc categories as model category. To that end, we construct a model category of lcc sketches, from which we obtain by the formalism of algebraically (co)fibrant objects model categories of strict lcc categories and then algebraically cofibrant strict lcc categories. The latter is our model of dependent type theory.<\/jats:p>","DOI":"10.1017\/s0960129521000098","type":"journal-article","created":{"date-parts":[[2021,9,20]],"date-time":"2021-09-20T07:37:51Z","timestamp":1632123471000},"page":"469-494","update-policy":"http:\/\/dx.doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["An interpretation of dependent type theory in a model category of locally cartesian closed categories"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-2238-8731","authenticated-orcid":false,"given":"Martin E.","family":"Bidlingmaier","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,9,20]]},"reference":[{"key":"S0960129521000098_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060485"},{"key":"S0960129521000098_ref1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1978-14512-1"},{"key":"S0960129521000098_ref17","first-page":"39","article-title":"Joyal\u2019s arithmetic universe as list-arithmetic pretopos","volume":"24","author":"Maietti","year":"2010","journal-title":"Theory and Applications of Categories"},{"key":"S0960129521000098_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5587-4_8"},{"key":"S0960129521000098_ref14","unstructured":"Lack, S. (2007). Homotopy-theoretic aspects of 2-monads. Journal of Homotopy and Related Structures 2 (2) 229\u2013260."},{"key":"S0960129521000098_ref9","unstructured":"Guillou, B. and May, J. P. (2020). Enriched model categories and presheaf categories. New York Journal of Mathematics 26\u00a037\u201391. http:\/\/nyjm.albany.edu\/j\/2020\/Vol26.htm."},{"key":"S0960129521000098_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-019-02305-w"},{"key":"S0960129521000098_ref12","unstructured":"Isaev, V. (2016). Model category of marked objects. https:\/\/arxiv.org\/abs\/1610.08459."},{"key":"S0960129521000098_ref6","first-page":"43","article-title":"Substitution up to isomorphism","volume":"23","author":"Curien","year":"1990","journal-title":"Diagrammes"},{"key":"S0960129521000098_ref21","doi-asserted-by":"publisher","DOI":"10.4115\/jla.2019.11.FT4"},{"key":"S0960129521000098_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(89)90160-6"},{"key":"S0960129521000098_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2010.12.004"},{"key":"S0960129521000098_ref19","first-page":"33","volume-title":"Mathematical proceedings of the Cambridge philosophical society","author":"Seely","year":"1984"},{"key":"S0960129521000098_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_10"},{"key":"S0960129521000098_ref4","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2014.v16.n2.a9"},{"key":"S0960129521000098_ref11","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1994) On the interpretation of type theory in locally cartesian closed categories. In: International Workshop on Computer Science Logic, Springer, Berlin, Heidelberg, 427\u2013441.","DOI":"10.1007\/BFb0022273"},{"key":"S0960129521000098_ref10","volume-title":"Model Categories and their Localizations","volume":"99","author":"Hirschhorn","year":"2003"},{"key":"S0960129521000098_ref13","unstructured":"Kelly, G. M. (1982). Basic Concepts of Enriched Category Theory, vol. 64, London Mathematical Society Lecture Note Series, Cambridge University Press, Cambridge."},{"key":"S0960129521000098_ref8","doi-asserted-by":"crossref","unstructured":"Dybjer, P. (1995). Internal type theory. In: International Workshop on Types for Proofs and Programs, Springer, Berlin, Heidelberg, 120\u2013134.","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0960129521000098_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"S0960129521000098_ref16","doi-asserted-by":"publisher","DOI":"10.1515\/9781400830558"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000098","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T03:19:42Z","timestamp":1649042382000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000098\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5]]},"references-count":21,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,2]]}},"alternative-id":["S0960129521000098"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000098","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,5]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}