{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,6]],"date-time":"2026-08-06T02:24:55Z","timestamp":1785983095464,"version":"3.56.0"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T00:00:00Z","timestamp":1416787200000},"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":[[2015,6]]},"abstract":"<jats:p>We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (\u221e, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.<\/jats:p>","DOI":"10.1017\/s0960129514000565","type":"journal-article","created":{"date-parts":[[2014,11,26]],"date-time":"2014-11-26T05:26:49Z","timestamp":1416979609000},"page":"1203-1277","source":"Crossref","is-referenced-by-count":48,"title":["Univalence for inverse diagrams and homotopy canonicity"],"prefix":"10.1017","volume":"25","author":[{"given":"MICHAEL","family":"SHULMAN","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,24]]},"reference":[{"key":"S0960129514000565_ref31","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","volume-title":"Higher Topos Theory","author":"Lurie","year":"2009"},{"key":"S0960129514000565_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071371"},{"key":"S0960129514000565_ref33","unstructured":"Moerdijk I. (2012) Fiber bundles and univalence. Available at: http:\/\/www.pitt.edu\/~krk56\/fiber_bundles_univalence.pdf. (Notes prepared by Chris Kapulkin)."},{"key":"S0960129514000565_ref6","doi-asserted-by":"publisher","DOI":"10.2307\/2273952"},{"key":"S0960129514000565_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097438"},{"key":"S0960129514000565_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129514000565_ref35","unstructured":"Radulescu-Banu A. (2006) Cofibrations in homotopy theory. ArXiv:math\/0610009."},{"key":"S0960129514000565_ref37","unstructured":"Shulman M. (2014) The univalence axiom for elegant Reedy presheaves. To appear in HHA. ArXiv:1307.6248."},{"key":"S0960129514000565_ref45","first-page":"347","volume-title":"Functional Programming Languages and Computer Architecture","author":"Wadler","year":"1989"},{"key":"S0960129514000565_ref17","volume-title":"Model Categories and their Localizations","author":"Hirschhorn","year":"2003"},{"key":"S0960129514000565_ref12","unstructured":"Cisinski D.-C. (2006) Les pr\u00e9faisceaux comme mod\u00e8les type d'homotopie. Vol. 308. Ast\u00e9risque. Soc. Math. France."},{"key":"S0960129514000565_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.05.002"},{"key":"S0960129514000565_ref3","doi-asserted-by":"crossref","unstructured":"Awodey S. , Garner R. , Martin-L\u00f6f P. and Voevodsky V. (2011) Mini-workshop: The homotopical interpretation of constructive type theory. Oberwolfach Reports 8.1, 609\u2013638.","DOI":"10.4171\/OWR\/2011\/11"},{"key":"S0960129514000565_ref15","unstructured":"Gepner D. and Kock J. (2012) Univalence in locally Cartesian closed 1-categories. ArXiv:1208.1749."},{"key":"S0960129514000565_ref28","unstructured":"Lumsdaine P. L. (2011) Strong functional extensionality from weak. Available at: http:\/\/homotopytypetheory.org\/2011\/12\/19\/strong-funext-from-weak\/."},{"key":"S0960129514000565_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_7"},{"key":"S0960129514000565_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-012-1082-0"},{"key":"S0960129514000565_ref30","unstructured":"Lumsdaine P. L. and Warren M. (2014) The local universes model: an overlooked coherence construction for dependent type theories. ArXiv:1411.1736."},{"key":"S0960129514000565_ref21","unstructured":"HoTT Project (2013) The homotopy type theory coq library. Available at: http:\/\/github.com\/HoTT\/HoTT\/."},{"key":"S0960129514000565_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"S0960129514000565_ref5","doi-asserted-by":"publisher","DOI":"10.2140\/agt.2013.13.1089"},{"key":"S0960129514000565_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003153"},{"key":"S0960129514000565_ref9","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1973-0341469-9"},{"key":"S0960129514000565_ref2","unstructured":"Avigad J. , Kapulkin C. and Lumsdaine P. L. (2013) Homotopy limits in Coq. ArXiv:1304.0680."},{"key":"S0960129514000565_ref19","first-page":"83","volume-title":"Oxford Logic Guides","author":"Hofmann","year":"1998"},{"key":"S0960129514000565_ref44","unstructured":"Voevodsky V. (2013) Univalent foundations. Avaiolable at: http:\/\/github.com\/vladimirias\/Foundations\/."},{"key":"S0960129514000565_ref43","unstructured":"Voevodsky V. (2011) Notes on type systems. Available at: http:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_Foundations.html."},{"key":"S0960129514000565_ref46","unstructured":"Warren M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University."},{"key":"S0960129514000565_ref23","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S0960129514000565_ref40","unstructured":"Univalent Foundations Program (2013) Homotopy type theory: Univalent foundations of mathematics. Available at: http:\/\/homotopytypetheory.org\/book\/."},{"key":"S0960129514000565_ref38","unstructured":"Streicher T. (1991) Semantics of Type Theory: Correctness, Completeness, and Independence Results, Progress in Theoretical Computer Science, Birkha\u00e4user."},{"key":"S0960129514000565_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-010-0770-x"},{"key":"S0960129514000565_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304912"},{"key":"S0960129514000565_ref36","unstructured":"Reedy C. L. (n.d.) Homotopy theory of model categories. Available at: http:\/\/www-math.mit.edu\/~psh\/."},{"key":"S0960129514000565_ref24","first-page":"179","article-title":"On modified Reedy and modified projective model structures","volume":"24","author":"Johnson","year":"2010","journal-title":"Theory and Applications of Categories"},{"key":"S0960129514000565_ref26","first-page":"337","volume-title":"Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '12","author":"Licata","year":"2012"},{"key":"S0960129514000565_ref13","unstructured":"Cisinski D.-C. (2012) Blog comment on post The mysterious nature of right properness. Available at: http:\/\/golem.ph.utexas.edu\/category\/2012\/05\/the_mysterious_nature_of_right.html#c041306."},{"key":"S0960129514000565_ref41","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"S0960129514000565_ref32","unstructured":"Makkai M. (1995) First order logic with dependent sorts, with applications to category theory. Available at: http:\/\/www.math.mcgill.ca\/makkai\/folds\/."},{"key":"S0960129514000565_ref27","first-page":"1","article-title":"Weak omega-categories from intensional type theory","volume":"6","author":"Lumsdaine","year":"2010","journal-title":"Typed Lambda Calculi and Applications"},{"key":"S0960129514000565_ref18","unstructured":"Hofmann M. (1994) On the interpretation of type theory in locally cartesian closed categories. In: Proceedings of Computer Science Logic. Springer Lecture Notes in Computer Science 427\u2013441."},{"key":"S0960129514000565_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"S0960129514000565_ref29","unstructured":"Lumsdaine P. L. and Shulman M. (2014) Semantics of higher inductive types. In preparation."},{"key":"S0960129514000565_ref25","unstructured":"Kapulkin C. , Lumsdaine P. L. and Voevodsky V. (2012) The simplicial model of univalent foundations. ArXiv:1211.2851."},{"key":"S0960129514000565_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(01)00176-1"},{"key":"S0960129514000565_ref22","volume-title":"Model Categories","author":"Hovey","year":"1999"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000565","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T20:51:52Z","timestamp":1566075112000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000565\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,24]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000565"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000565","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,24]]}}}