{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:14Z","timestamp":1775790794446,"version":"3.50.1"},"reference-count":37,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T00:00:00Z","timestamp":1637193600000},"content-version":"unspecified","delay-in-days":48,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over a base category. Any Grothendieck topology of the base category then gives rise to a family of left-exact modalities, and we recover a model of type theory by localizing the presheaf model with respect to this family of left-exact modalities. We provide then some examples.<\/jats:p>","DOI":"10.1017\/s0960129521000359","type":"journal-article","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T10:13:32Z","timestamp":1637230412000},"page":"979-1002","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Constructive sheaf models of type theory"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-5153","authenticated-orcid":false,"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Fabian","family":"Ruch","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6374-4427","authenticated-orcid":false,"given":"Christian","family":"Sattler","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,11,18]]},"reference":[{"key":"S0960129521000359_ref22","unstructured":"Quirin, K. (2016). Lawvere-Tierney Sheafification in Homotopy Type Theory. (Faisceautisation de Lawvere-Tierney en th\u00e9orie des types homotopiques). Phd thesis, \u00c9cole des mines de Nantes, France."},{"key":"S0960129521000359_ref32","unstructured":"Swan, A. and Uemura, T. (2019). On Church\u2019s thesis in cubical assemblies. CoRR, abs\/1905.03014."},{"key":"S0960129521000359_ref11","first-page":"50","article-title":"Inductively defined types","volume":"417","author":"Coquand","year":"1988","journal-title":"COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings"},{"key":"S0960129521000359_ref2","unstructured":"Angiuli, C. , Brunerie, G. , Coquand, T. , Hou (Favonia), K.-B. , Harper, R. and Licata, D. R. (2017). Cartesian cubical type theory. Draft."},{"key":"S0960129521000359_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"S0960129521000359_ref1","unstructured":"Aczel, P. (1998). On relating type theories and set theories. In: Altenkirch, T. , Naraschewski, W. and Reus, B. (eds.) Types for Proofs and Programs, International Workshop TYPES\u201998, Kloster Irsee, Germany, March 27\u201331, 1998, Selected Papers, Lecture Notes in Computer Science, vol. 1657, Springer, 1\u201318."},{"key":"S0960129521000359_ref34","unstructured":"Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"S0960129521000359_ref29","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"S0960129521000359_ref31","unstructured":"Shulman, M. (2019). All (\u221e ,1)-toposes have strict univalent universes. CoRR, abs\/1904.07004."},{"key":"S0960129521000359_ref7","unstructured":"Boulier, S. P. (2018). Extending Type Theory with Syntactic Models. (Etendre la th\u00e9orie des types \u00e0 l\u2019aide de mod\u00e8les syntaxiques). Phd thesis, Ecole nationale sup\u00e9rieure Mines-T\u00e9l\u00e9com Atlantique Bretagne Pays de la Loire, France."},{"key":"S0960129521000359_ref16","unstructured":"Joyal, A. (1984). Lettre \u00e0 Grothendieck."},{"key":"S0960129521000359_ref28","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2015.v17.n2.a6"},{"key":"S0960129521000359_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"S0960129521000359_ref13","doi-asserted-by":"publisher","DOI":"10.2307\/1969364"},{"key":"S0960129521000359_ref25","unstructured":"Sattler, C. (2017). The equivalence extension property and model structures. CoRR, abs\/1704.06911."},{"key":"S0960129521000359_ref18","volume-title":"Truncation Levels in Homotopy Type Theory","author":"Kraus","year":"2015"},{"key":"S0960129521000359_ref21","unstructured":"Orton, I. and Pitts, A. M. (2016). Axioms for modelling cubical type theory in a topos. In: Talbot, J.-M. and Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, LIPIcs, vol. 62, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 24:1\u201324:19."},{"key":"S0960129521000359_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S0960129521000359_ref6","unstructured":"Beth, E. W. (1956). Semantic Construction of Intuitionistic Logic. Medededlingen der koninklijke Nederlandse Akademie van Wetenschappen, afd. Letterkunde. Nieuwe Reeks, Deel 19, No. 11. N. V. Noord-Hollandsche Uitgevers Maatschappij, Amsterdam."},{"key":"S0960129521000359_ref36","first-page":"915","article-title":"A constructive model of directed univalence in bicubical sets","author":"Weaver","year":"2020","journal-title":"LICS\u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8\u201311, 2020"},{"key":"S0960129521000359_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-012-1082-0"},{"key":"S0960129521000359_ref12","unstructured":"Dybjer, P. (1995). Internal type theory. In: Berardi, S. and Coppo, M. (eds.) Types for Proofs and Programs, International Workshop TYPES\u201995, Torino, Italy, June 5\u20138, 1995, Selected Papers, Lecture Notes in Computer Science, vol. 1158, Springer, 120\u2013134."},{"key":"S0960129521000359_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BF02684778"},{"key":"S0960129521000359_ref17","unstructured":"Kaposi, A. , Huber, S. and Sattler, C. (2019). Gluing for type theory. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24\u201330, 2019, Dortmund, Germany, LIPIcs, vol. 131, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 25:1\u201325:19."},{"key":"S0960129521000359_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(74)90037-1"},{"key":"S0960129521000359_ref26","first-page":"109","article-title":"Quantum gauge field theory in cohesive homotopy type theory","volume":"158","author":"Schreiber","year":"2012","journal-title":"Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012, Brussels, Belgium, 10\u201312 October 2012"},{"key":"S0960129521000359_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"S0960129521000359_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005130"},{"key":"S0960129521000359_ref37","volume-title":"Formalizing Cartan Geometry in Modal Homotopy Type Theory","author":"Wellen","year":"2017"},{"key":"S0960129521000359_ref8","unstructured":"Cohen, C. , Coquand, T. , Huber, S. and M\u00f6rtberg, A. (2015). Cubical type theory: A constructive interpretation of the univalence axiom. In: Uustalu, T . (ed.) 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18\u201321, 2015, Tallinn, Estonia, LIPIcs, vol. 69, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 5:1\u20135:34."},{"key":"S0960129521000359_ref27","first-page":"403","volume-title":"To HB. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Scott","year":"1980"},{"key":"S0960129521000359_ref33","volume-title":"Constructivism in mathematics. Vol. II, Studies in Logic and the Foundations of Mathematics","author":"Troelstra","year":"1988"},{"key":"S0960129521000359_ref20","first-page":"5","article-title":"Dynamic Newton-Puiseux theorem","author":"Mannaa","year":"2013","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129521000359_ref23","unstructured":"Rezk, C. (2010). Toposes and homotopy toposes. Unpublished manuscript."},{"key":"S0960129521000359_ref24","article-title":"Modalities in homotopy type theory","volume":"16","author":"Rijke","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129521000359_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000498"},{"key":"S0960129521000359_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000359","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,21]],"date-time":"2022-06-21T05:55:55Z","timestamp":1655790955000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000359\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10]]},"references-count":37,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["S0960129521000359"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000359","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10]]},"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"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}