{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:57:47Z","timestamp":1770994667580,"version":"3.50.1"},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T00:00:00Z","timestamp":1479340800000},"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":[[2018,2]]},"abstract":"<jats:p>The notion of a <jats:italic>natural model<\/jats:italic> of type theory is defined in terms of that of a <jats:italic>representable natural transfomation<\/jats:italic> of presheaves. It is shown that such models agree exactly with the concept of a <jats:italic>category with families<\/jats:italic> in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums \u03a3, dependent products \u03a0 and intensional identity types <jats:monospace>Id<\/jats:monospace>, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.<\/jats:p>","DOI":"10.1017\/s0960129516000268","type":"journal-article","created":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T08:50:16Z","timestamp":1479372616000},"page":"241-286","source":"Crossref","is-referenced-by-count":34,"title":["Natural models of homotopy type theory"],"prefix":"10.1017","volume":"28","author":[{"given":"STEVE","family":"AWODEY","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,11,17]]},"reference":[{"key":"S0960129516000268_ref17","article-title":"The local universes model: An overlooked coherence construction for dependent type theories","volume":"16","author":"LeFanu Lumsdaine","year":"2015","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129516000268_ref16","unstructured":"Kapulkin C. , LeFanu Lumsdaine P. and Voevodsky V. (2014). The simplicial model of univalent foundations. On the arXiv as 1211.2851v2, dated 15 April 2014."},{"key":"S0960129516000268_ref12","volume-title":"Semantics of Logics of Computation","author":"Hofmann","year":"1997"},{"key":"S0960129516000268_ref7","doi-asserted-by":"crossref","unstructured":"Fiore M. (2012). Discrete generalised polynomial functors. Talk given at ICALP.","DOI":"10.1007\/978-3-642-31585-5_22"},{"key":"S0960129516000268_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.06.004"},{"key":"S0960129516000268_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"S0960129516000268_ref19","unstructured":"Streicher T. (2006). Identity Types and Weak Omega-Groupoids. Talks in Uppsala at a meeting on \u2018Identity Types - Topological and Categorical Structure\u2019."},{"key":"S0960129516000268_ref11","first-page":"427","volume-title":"CSL","author":"Hofmann","year":"1994"},{"key":"S0960129516000268_ref13","first-page":"315","article-title":"Partial products, bagdomains and hyperlocal toposes","volume":"177","author":"Johnstone","year":"1992","journal-title":"LMS Lecture Note Series"},{"key":"S0960129516000268_ref15","unstructured":"Joyal A. (2014). Categorical homotopy type theory. Slides from a talk at MIT dated 17 March 2014."},{"key":"S0960129516000268_ref18","first-page":"73","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Martin-L\u00f6f","year":"1975"},{"key":"S0960129516000268_ref6","first-page":"103","article-title":"Exponentiable morphisms, partial products and pullback complements","volume":"7","author":"Dyckhoff","year":"1987","journal-title":"JPAA"},{"key":"S0960129516000268_ref20","unstructured":"Streicher T. (2014). Semantics of type theory formulated in terms of representability. Unpublished note dated 26 February 2014."},{"key":"S0960129516000268_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00120-8"},{"key":"S0960129516000268_ref4","unstructured":"Bezem M. , Coquand T. and Huber S. (2014). A model of type theory in cubical sets. Unpublished preprint dated 3 May 2014."},{"key":"S0960129516000268_ref5","first-page":"120","article-title":"Internal type theory","volume":"1158","author":"Dybjer","year":"1996","journal-title":"LNCS"},{"key":"S0960129516000268_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129516000268_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071371"},{"key":"S0960129516000268_ref21","unstructured":"The Stacks Project Authors (2016). Stacks Project. Available at: http:\/\/stacks.math.columbia.edu."},{"key":"S0960129516000268_ref1","volume-title":"Lecture Notes in Mathematics","author":"Artin","year":"1972"},{"key":"S0960129516000268_ref22","unstructured":"The Univalent Foundations Program, Institute for Advanced Study (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Available at: http:\/\/homotopytypetheory.org\/book"},{"key":"S0960129516000268_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"S0960129516000268_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002058"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129516000268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,15]],"date-time":"2019-04-15T19:57:17Z","timestamp":1555358237000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129516000268\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,17]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["S0960129516000268"],"URL":"https:\/\/doi.org\/10.1017\/s0960129516000268","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,17]]}}}