{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:35:56Z","timestamp":1787067356596,"version":"build-2736575974"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101170308"],"award-info":[{"award-number":["101170308"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n                    The metatheory of dependent types has seen a lot of progress in recent years. In particular, the development of categorical gluing finally lets us work with\n                    <jats:italic toggle=\"yes\">semantic<\/jats:italic>\n                    presentations of type theory (such as categories with families) to establish fundamental properties of type theory such as canonicity and normalisation. However, proofs by gluing have yet to reach the stage of computer formalisation: formal proofs for the metatheory of dependent types are still stuck in the age of tedious syntactic proofs. The main reason for this is that semantic presentations of type theory are defined using sophisticated indexed inductive types, which are prone to \u201ctransport hell\u201d. In this paper, we introduce a new technique to work with CwFs in intensional type theory without getting stuck in transport hell. More specifically, we construct an alternative presentation of the initial CwF which encodes the substitutions as metatheoretical functions. This has the effect of strictifying all the equations that are involved in the substitution calculus, which greatly reduces the need for transports. As an application, we use our strictified initial CwF to give a short and elegant proof of canonicity for a type theory with dependent products and booleans with large elimination. The resulting proof is fully formalised in Agda.\n                  <\/jats:p>","DOI":"10.1145\/3747535","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"855-885","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Type Theory in Type Theory using a Strictified Syntax"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9897-8936","authenticated-orcid":false,"given":"Ambrus","family":"Kaposi","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2070-051X","authenticated-orcid":false,"given":"Lo\u00efc","family":"Pujet","sequence":"additional","affiliation":[{"name":"Stockholm University, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_1","volume-title":"Habilitation thesis","author":"Abel Andreas","year":"2013","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen. http:\/\/www2.tcs.ifi.lmu.de\/~abel\/habil.pdf."},{"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\/3636501.3636951"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561309"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.6"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_9_1","volume-title":"23rd International Conference on Types for Proofs and Programs, TYPES 2017","author":"Altenkirch Thorsten","year":"2017","unstructured":"Thorsten Altenkirch, Ambrus Kaposi, and Andr\u00e1s Kov\u00e1cs. 2017. Normalisation by Evaluation for a Type Theory with Large Elimination. In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Ed. by Ambrus Kaposi. E\u00f6tv\u00f6s Lor\u00e1nd University. http:\/\/types2017.elte.hu\/proc.pdf#page=26."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_13_1","unstructured":"Andrej Bauer Ga\u00ebtan Gilbert Philipp Haselwarter Matija Pretnar and Christopher A. Stone. 2016. Design and Implementation of the Andromeda proof assistant. Abstract at 22nd International Conference on Types for Proofs and Programs (TYPES 2016). (2016). http:\/\/www.types2016.uns.ac.rs\/images\/abstracts\/bauer2.pdf."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2021.3"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2023.18"},{"key":"e_1_3_2_16_1","unstructured":"Guillaume Brunerie and Menno de Boer. 2020. Formalization of the initiality conjecture. (2020). Retrieved July 31 2021 from https:\/\/github.com\/guillaumebrunerie\/initiality."},{"key":"e_1_3_2_17_1","unstructured":"Mario Carneiro. 2024. Lean4Lean: Towards a Verified Typechecker for Lean in Lean. (2024). https:\/\/arxiv.org\/abs\/2403.14064 arXiv: 2403.14064 [cs.PL]."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66545-6_5"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000881"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434341"},{"key":"e_1_3_2_22_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development Environment","author":"Constable R. L.","year":"1985","unstructured":"R. L. Constable et al.. 1985. Implementing Mathematics with the Nuprl Proof Development Environment. Prentice-Hall. http:\/\/www.nuprl.org\/book\/."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2014.03.003"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.6"},{"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.1145\/3531130.3532398"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_68"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022273"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_3_2_34_1","volume-title":"29th International Conference on Types for Proofs and Programs (TYPES 2023)","author":"Kaposi Ambrus","year":"2023","unstructured":"Ambrus Kaposi. 2023. Towards quotient inductive-inductive-recursive types. In: 29th International Conference on Types for Proofs and Programs (TYPES 2023). Ed. by Eduardo Hermo Reyes and Alicia Villanueva. Valencia. https:\/\/types2023.webs.upv.es\/TYPES2023.pdf."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_12"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"[SW] Ambrus Kaposi and Lo\u00efc Pujet Type Theory in Type Theory using a Strictified Syntax (accompanying formalisation) July 2025. doi: 10.5281\/zenodo.15860280 url: https:\/\/doi.org\/10.5281\/zenodo.15860280 10.5281\/zenodo.15860280.","DOI":"10.5281\/zenodo.15860280"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2024.10"},{"key":"e_1_3_2_40_1","volume-title":"27th International Conference on Types for Proofs and Programs, TYPES 2021","author":"Kaposi Ambrus","year":"2021","unstructured":"Ambrus Kaposi and Zongpu Xie. 2021. Quotient inductive-inductive types in the setoid model. In: 27th International Conference on Types for Proofs and Programs, TYPES 2021. Ed. by Henning Basold. Universiteit Leiden. https:\/\/types21.liacs.nl\/download\/quotient-inductive-inductive-types-in-the-setoid-model\/."},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2024.26"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_18"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394740"},{"key":"e_1_3_2_46_1","volume-title":"PhD thesis","author":"Pujet Lo\u00efc","year":"2022","unstructured":"Lo\u00efc Pujet. 2022. Computing with Extensionality Principles in Type Theory. PhD thesis. Nantes Universit\u00e9. https:\/\/github.com\/loic-p\/PhD-thesis\/releases."},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3719342"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6990769"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_3_2_53_1","unstructured":"The Agda Development Team. 2023. The Agda Programming Language. (2023). http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"key":"e_1_3_2_54_1","unstructured":"The Coq Development Team. 2021. The Coq Proof Assistant. (2021). https:\/\/www.coq.inria.fr."},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674647"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.70675\/f3c96514z4373z4f99z8b3fzb1b41307d558"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294095"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747535","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:00:20Z","timestamp":1784196020000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747535"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":57,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747535"],"URL":"https:\/\/doi.org\/10.1145\/3747535","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}