{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:15:50Z","timestamp":1784211350683,"version":"3.55.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100004063","name":"Knut and Alice Wallenberg Foundation","doi-asserted-by":"crossref","award":["2019.0116"],"award-info":[{"award-number":["2019.0116"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>We prove canonicity for a Martin-L\u00f6f type theory with a countable universe hierarchy where each universe supports indexed inductive-recursive (IIR) types. We proceed in two steps. First, we construct IIR types from inductive-recursive (IR) types and other basic type formers, in order to simplify the subsequent canonicity proof. The constructed IIR types support the same definitional computation rules that are available in Agda\u2019s native IIR implementation. Second, we give a canonicity proof for IR types, building on the established method of gluing along the global sections functor. The main idea is to encode the canonicity predicate for each IR type using a metatheoretic IIR type.<\/jats:p>","DOI":"10.1145\/3776685","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1241-1269","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Canonicity for Indexed Inductive-Recursive Types"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-9781","authenticated-orcid":false,"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"University of Gothenburg, Gothenburg, Sweden"},{"name":"Chalmers University of Technology, Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632920"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_3_2_7_1","unstructured":"Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http:\/\/www.strictlypositive.org\/ott.pdf"},{"key":"e_1_3_2_8_1","volume-title":"Lecture Notes in Mathematics","author":"Artin Michael","year":"1971","unstructured":"Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. 1971. Theorie de Topos et Cohomologie Etale des Schemas I, II, III. Lecture Notes in Mathematics, Vol. 269, 270, 305. Springer."},{"issue":"4","key":"e_1_3_2_9_1","first-page":"265","article-title":"Universes for Generic Programs and Proofs in Dependent Type Theory","volume":"10","author":"Marcin Benke Peter Dybjer","year":"2003","unstructured":"Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. 7. Comput. 10, 4 (2003), 265\u2013289.","journal-title":"Nord. 7. Comput"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2023.18"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_10"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2021.9"},{"key":"e_1_3_2_17_1","unstructured":"Guillaume Brunerie and Menno de Boer. 2020. Formalization of the initiality conjecture. https:\/\/github.com\/guillaumebrunerie\/initiality"},{"key":"e_1_3_2_18_1","volume-title":"Generalised algebraic theories and contextual categories","author":"Cartmell John","year":"1978","unstructured":"John Cartmell. 1978. Generalised algebraic theories and contextual categories. Ph. D. Dissertation. Oxford University."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_20_1","unstructured":"Simon Castellan Pierre Clairambault and Peter Dybjer. 2019. Categories with Families: Unityped Simply Typed and Dependently Typed. CoRR abs\/1904.00827 (2019). arXiv:1904.00827 http:\/\/arxiv.org\/abs\/1904.00827"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Jonathan Chan and Stephanie Weirich. 2025. Bounded First-Class Universe Levels in Dependent Type Theory. CoRR abs\/2502.20485 (2025). arXiv:2502.20485 doi:10.48550\/ARXIV.2502.20485","DOI":"10.48550\/ARXIV.2502.20485"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434341"},{"key":"e_1_3_2_23_1","first-page":"239","volume-title":"European Symposium on Programming","author":"Cohen Cyril","year":"2024","unstructured":"Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2024. Trocq: proof transfer for free, with or without univalence. In European Symposium on Programming. Springer, 239\u2013268."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_3_2_25_1","volume-title":"Fully Generic Programming over Closed Universes of Inductive-Recursive Types","author":"Diehl Larry","year":"2017","unstructured":"Larry Diehl. 2017. Fully Generic Programming over Closed Universes of Inductive-Recursive Types. Ph. D. Dissertation. Portland State University."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_11"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAP.2005.07.001"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1093\/LOGCOM\/EXAD022"},{"key":"e_1_3_2_33_1","volume-title":"typed operational semantics for type theory","author":"Goguen Healfdene","year":"1994","unstructured":"Healfdene Goguen. 1994. A typed operational semantics for type theory. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/hdl.handle.net\/1842\/405"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2020.8"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_3_2_38_1","unstructured":"Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Nicolai Kraus. 2019b. Formalisations in Agda using a morally correct shallow embedding. https:\/\/bitbucket.org\/akaposi\/shallow\/src\/master\/"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_12"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.28"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Andr\u00e1s Kov\u00e1cs. 2023. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. CoRR abs\/2302.08837 (2023). arXiv:2302.08837 doi:10.48550\/ARXIV.2302.08837","DOI":"10.48550\/ARXIV.2302.08837"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674648"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Andr\u00e1s Kov\u00e1cs. 2025. Supplement to the paper \u201cCanonicity for Indexed Inductive-Recursive Types\u201d. doi:10.5281\/zenodo.17429493","DOI":"10.5281\/zenodo.17429493"},{"key":"e_1_3_2_44_1","volume-title":"Canonicity of the Mahlo Universe","author":"Kub\u00e1nek Ond\u0159ej","year":"2025","unstructured":"Ond\u0159ej Kub\u00e1nek. 2025. Canonicity of the Mahlo Universe. Master\u2019s thesis. Chalmers University of Technology, Gothenburg. https:\/\/github.com\/kubaneko\/External-Mahlo-Canonicity\/blob\/main\/Main.pdf"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_46_1","article-title":"Studies in Proof Theory","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages.","journal-title":"Intuitionistic type theory"},{"key":"e_1_3_2_47_1","first-page":"191","volume-title":"Twenty-five years of constructive type theory (Oxford Logic Guides, Vol. 36)","author":"Palmgren Erik","year":"1998","unstructured":"Erik Palmgren. 1998. On universes in type theory. In Twenty-five years of constructive type theory (Oxford Logic Guides, Vol. 36). Oxford University Press, 191 \u2013 204."},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.10.001"},{"key":"e_1_3_2_49_1","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-319-89884-1_9","volume-title":"Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 27","author":"P\u00e9drot Pierre-Marie","year":"2018","unstructured":"Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2018. Failure is Not an Option: An Exceptional Type Theory. In Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 27. Springer, 245\u2013271."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3719342"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571739"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050140"},{"key":"e_1_3_2_53_1","volume-title":"First Steps in Synthetic Tait Computability","author":"Sterling Jonathan","year":"2021","unstructured":"Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability. Ph. D. Dissertation. Carnegie Mellon University Pittsburgh, PA."},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling and Carlo Angiuli. 2021. Normalization for Cubical Type Theory. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2021 Rome Italy June 29 - July 2 2021. IEEE 1\u201315. doi:10.1109\/LICS52264.2021.9470719","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_3_2_57_1","unstructured":"The Agda Team. 2025a. Agda documentation. https:\/\/agda.readthedocs.io\/en\/v2.8.0\/"},{"key":"e_1_3_2_58_1","unstructured":"The Agda Team. 2025b. Agda documentation on -without-K. https:\/\/agda.readthedocs.io\/en\/v2"},{"key":"e_1_3_2_59_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_2_61_1","volume-title":"Une Th\u00e9orie des Constructions Inductives","author":"Werner Benjamin","year":"1994","unstructured":"Benjamin Werner. 1994. Une Th\u00e9orie des Constructions Inductives. Ph. D. Dissertation. Paris Diderot University, France. https:\/\/tel.archives-ouvertes.fr\/tel-00196524"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776685","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:42:22Z","timestamp":1784209342000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776685"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776685"],"URL":"https:\/\/doi.org\/10.1145\/3776685","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}