{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T12:39:44Z","timestamp":1785415184576,"version":"3.56.0"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,12,17]],"date-time":"2025-12-17T00:00:00Z","timestamp":1765929600000},"content-version":"unspecified","delay-in-days":350,"URL":"https:\/\/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":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We introduce\n                    <jats:italic>Displayed Type Theory (dTT)<\/jats:italic>\n                    , a multi-modal homotopy type theory with\n                    <jats:italic>discrete<\/jats:italic>\n                    and\n                    <jats:italic>simplicial<\/jats:italic>\n                    modes. In the intended semantics, the discrete mode is interpreted by a model for an arbitrary\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inline1.png\"\/>\n                        <jats:tex-math>$\\infty$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -topos, while the simplicial mode is interpreted by Reedy fibrant augmented semi-simplicial diagrams in that model. This simplicial structure is represented inside the theory by a primitive notion of\n                    <jats:italic>display<\/jats:italic>\n                    or\n                    <jats:italic>dependency<\/jats:italic>\n                    , guarded by modalities, yielding a partially-internal form of unary parametricity. Using the display primitive, we then give a coinductive definition, at the simplicial mode, of a type\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA1.png\"\/>\n                    of semi-simplicial types. Roughly speaking, a semi-simplicial type\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA2.png\"\/>\n                    consists of a type\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA3.png\"\/>\n                    together with, for each\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA4.png\"\/>\n                    , a displayed semi-simplicial type over\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA5.png\"\/>\n                    . This mimics how simplices can be generated geometrically through repeated cones, and is made possible by the display primitive at the simplicial mode. The discrete part of\n                    <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952510025X_inlineA6.png\"\/>\n                    then yields the usual infinite indexed definition of semi-simplicial types, both semantically and syntactically. Thus, dTT enables working with semi-simplicial types in full semantic generality.\n                  <\/jats:p>","DOI":"10.1017\/s096012952510025x","type":"journal-article","created":{"date-parts":[[2025,12,17]],"date-time":"2025-12-17T01:37:06Z","timestamp":1765935426000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Displayed type theory and semi-simplicial types"],"prefix":"10.1017","volume":"35","author":[{"given":"Astra","family":"Kolomatskaia","sequence":"first","affiliation":[{"name":"Wesleyan University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9948-6682","authenticated-orcid":false,"given":"Michael","family":"Shulman","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/03jbbze48","id-type":"ROR","asserted-by":"publisher"}],"name":"University of San Diego"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2025,12,17]]},"reference":[{"key":"S096012952510025X_ref12","article-title":"Undecidability of equality in the free locally cartesian closed category (extended version)","volume":"13","author":"Castellan","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S096012952510025X_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000032"},{"key":"S096012952510025X_ref17","doi-asserted-by":"crossref","unstructured":"Herbelin, H. and Ramachandra, R. A parametricity-based formalization of semi-simplicial and semi-cubical sets. arXiv:2401.00512, 2024.","DOI":"10.1017\/S096012952500009X"},{"key":"S096012952510025X_ref22","doi-asserted-by":"publisher","DOI":"10.2307\/2275015"},{"key":"S096012952510025X_ref28","unstructured":"Shulman, M. (2019). All -toposes have strict univalent universes. arXiv:1904.07004."},{"key":"S096012952510025X_ref32","first-page":"347","volume-title":"Functional Programming Languages and Computer Architecture","author":"Wadler","year":"1989"},{"key":"S096012952510025X_ref33","unstructured":"Weinberger, J. (2022). Strict stability of extension types. arXiv:2203.07194."},{"key":"S096012952510025X_ref4","article-title":"Displayed categories","volume":"15","author":"Ahrens","year":"2019","journal-title":"Logical Methods in Computer Science"},{"key":"S096012952510025X_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"S096012952510025X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_10"},{"key":"S096012952510025X_ref21","first-page":"1","article-title":"Internal universes in models of homotopy type theory","volume":"108","author":"Licata","year":"2018","journal-title":"Leibniz International Proceedings in Informatics (LIPIcs)"},{"key":"S096012952510025X_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"S096012952510025X_ref16","article-title":"Multimodal dependent type theory","volume":"17","author":"Gratzer","year":"2021","journal-title":"Logical Methods in Computer Science"},{"key":"S096012952510025X_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3514241"},{"key":"S096012952510025X_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"S096012952510025X_ref25","unstructured":"Riley, M. , Finster, E. and Licata, D. R. (2021). Synthetic spectra via a monadic and comonadic modality. arXiv:2102.04099."},{"key":"S096012952510025X_ref20","unstructured":"Kraus, N. (2015). The general universal property of the propositional truncation. In: Herbelin, H. , Letouzey, P. and Sozeau, M. (eds.) 20th International Conference on Types for Proofs and Programs (TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany,. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, vol. 39, 111\u2013145. arXiv:1411.2682."},{"key":"S096012952510025X_ref23","unstructured":"Moulin, G. (2016). Internalizing Parametricity. Phd thesis, Chalmers University."},{"key":"S096012952510025X_ref6","unstructured":"Altenkirch, T. , Kaposi, A. and Shulman, M. (2022). Towards a third-generation HOTT. URL: https:\/\/ncatlab.org\/nlab\/show\/higher+observational+type+theory."},{"key":"S096012952510025X_ref30","unstructured":"Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics, first edition. http:\/\/homotopytypetheory.org\/book\/."},{"key":"S096012952510025X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"S096012952510025X_ref31","unstructured":"Uskuplu, E. (2023). Formalizing Two-Level Type Theory with Cofibrant exo-nat. Phd thesis, University of Southern California."},{"key":"S096012952510025X_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"S096012952510025X_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"S096012952510025X_ref11","doi-asserted-by":"crossref","unstructured":"Cavallo, E. (2021). Higher Inductive Types and Internal Parametricity for Cubical Type Theory. Phd thesis, Carnegie Mellon University.","DOI":"10.46298\/lmcs-17(4:5)2021"},{"key":"S096012952510025X_ref7","doi-asserted-by":"crossref","unstructured":"Annenkov, D. , Capriotti, P. , Kraus, N. and Sattler, C. (2023). Two-level type theory and applications. Mathematical Structures in Computer Science 1\u201356. arXiv:1705.03307.","DOI":"10.1017\/S096012952300021X"},{"key":"S096012952510025X_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66545-6_5"},{"key":"S096012952510025X_ref1","doi-asserted-by":"crossref","unstructured":"Aczel, P. (1978). The type theoretic interpretation of constructive set theory. In: Macintyre, A. , Pacholski, L. and Paris, J. (eds.) Logic Colloquium\u201977, Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55\u201366.","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"S096012952510025X_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2020.106563"},{"key":"S096012952510025X_ref2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. , Chamoun, Y. , Kaposi, A. and Shulman, M. (2024). Internal parametricity, without an interval. To appear in POPL\u201924. arXiv:2307.06448.","DOI":"10.1145\/3632920"},{"key":"S096012952510025X_ref24","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"S096012952510025X_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700006353"},{"key":"S096012952510025X_ref29","doi-asserted-by":"crossref","unstructured":"Shulman, M. (2023). Semantics of multimodal adjoint type theory. Electronic Notes in Theoretical Informatics and Computer Science 3 (Proceedings of MFPS XXXIX). arXiv:2303.02572.","DOI":"10.46298\/entics.12300"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012952510025X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,17]],"date-time":"2025-12-17T01:37:09Z","timestamp":1765935429000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012952510025X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":33,"alternative-id":["S096012952510025X"],"URL":"https:\/\/doi.org\/10.1017\/s096012952510025x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. 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 (https:\/\/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"}],"article-number":"e34"}}