{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T00:38:47Z","timestamp":1760575127431,"version":"build-2065373602"},"reference-count":47,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.431.4","type":"journal-article","created":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:32:32Z","timestamp":1760347952000},"page":"42-64","source":"Crossref","is-referenced-by-count":0,"title":["Type Theory with Single Substitutions"],"prefix":"10.4204","volume":"431","author":[{"given":"Ambrus","family":"Kaposi","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University (ELTE)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Szumi","family":"Xie","sequence":"additional","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University (ELTE)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2025,10,14]]},"reference":[{"key":"DBLP:journals\/pacmpl\/0001OV18","doi-asserted-by":"publisher","DOI":"10.1145\/3158111","article-title":"Decidability of conversion for type theory in type theory","volume":"2","author":"Abel","year":"2018","journal-title":"Proc. ACM Program. Lang."},{"key":"DBLP:conf\/cpp\/AdjedjLMPP24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1145\/3636501.3636951","article-title":"Martin-L\u00f6f \u00e0 la Coq","volume-title":"Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024","author":"Adjedj","year":"2024"},{"key":"bc","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2023.41","article-title":"B-systems and C-systems are equivalent","author":"Ahrens","year":"2023","journal-title":"The Journal of Symbolic Logic"},{"key":"DBLP:conf\/aplas\/AhrensLN24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-981-97-8943-6_1","article-title":"Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories","volume-title":"Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings","volume":"15194","author":"Ahrens","year":"2024"},{"issue":"3","key":"DBLP:journals\/lmcs\/AhrensLV18","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(3:18)2018","article-title":"Categorical structures for type theory in univalent foundations","volume":"14","author":"Ahrens","year":"2018","journal-title":"Log. Methods Comput. Sci."},{"volume-title":"Constructions, Inductive Types and Strong Normalization","year":"1993","author":"Altenkirch","key":"alti:phd93"},{"key":"setoidhell","article-title":"From setoid hell to homotopy heaven? The role of extensionality in Type Theory","volume-title":"23rd International Conference on Types for Proofs and Programs, TYPES 2017","author":"Altenkirch","year":"2017"},{"key":"DBLP:conf\/mpc\/AltenkirchBKT19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-030-33636-3_7","article-title":"Setoid Type Theory - A Syntactic Translation","volume-title":"Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings","volume":"11825","author":"Altenkirch","year":"2019"},{"key":"DBLP:conf\/popl\/AltenkirchK16","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/2837614.2837638","article-title":"Type theory in type theory using quotient inductive types","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016","author":"Altenkirch","year":"2016"},{"key":"lmcs:4005","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017","article-title":"Normalisation by Evaluation for Type Theory, in Type Theory","volume":"Volume 13, Issue 4","author":"Altenkirch","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"cohtt","article-title":"Coherent Categories with Families","volume-title":"30th International Conference on Types for Proofs and Programs (TYPES 2024)","author":"Altenkirch","year":"2024"},{"key":"DBLP:conf\/fscd\/AltenkirchKSV23","series-title":"LIPIcs","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2023.24","article-title":"Combinatory Logic and Lambda Calculus Are Equal, Algebraically","volume-title":"8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy","volume":"260","author":"Altenkirch","year":"2023"},{"key":"DBLP:conf\/csl\/AltenkirchR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","article-title":"Monadic Presentations of Lambda Terms Using Generalized Inductive Types","volume-title":"Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings","volume":"1683","author":"Altenkirch","year":"1999"},{"issue":"2","key":"DBLP:journals\/mscs\/Awodey18","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1017\/S0960129516000268","article-title":"Natural models of homotopy type theory","volume":"28","author":"Awodey","year":"2018","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"DBLP:journals\/tocl\/Berg18","doi-asserted-by":"publisher","DOI":"10.1145\/3204492","article-title":"Path Categories and Propositional Identity Types","volume":"19","author":"van den Berg","year":"2018","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"DBLP:journals\/jfp\/BernardyJP12","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","article-title":"Proofs for free - Parametricity for dependent types","volume":"22","author":"Bernardy","year":"2012","journal-title":"J. Funct. Program."},{"key":"DBLP:journals\/corr\/abs-2211-07487","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2211.07487","article-title":"External univalence for second-order generalized algebraic theories","volume":"abs\/2211.07487","author":"Bocquet","year":"2022","journal-title":"CoRR"},{"key":"DBLP:conf\/fscd\/BocquetKS23","series-title":"LIPIcs","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2023.18","article-title":"For the Metatheory of Type Theory, Internal Sconing Is Enough","volume-title":"8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy","volume":"260","author":"Bocquet","year":"2023"},{"issue":"5","key":"DEBRUIJN1972381","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem","volume":"75","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"DBLP:journals\/apal\/Cartmell86","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","article-title":"Generalised algebraic theories and contextual categories","volume":"32","author":"Cartmell","year":"1986","journal-title":"Ann. Pure Appl. Log."},{"key":"Castellan2021","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-66545-6_5","volume-title":"Categories with Families: Unityped, Simply Typed, and Dependently Typed","author":"Castellan","year":"2021"},{"key":"chapman09eatitself","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.114","article-title":"Type Theory Should Eat Itself","volume":"228","author":"Chapman","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"6","key":"DBLP:journals\/mscs\/ClairambaultD14","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000881","article-title":"The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories","volume":"24","author":"Clairambault","year":"2014","journal-title":"Math. Struct. Comput. Sci."},{"key":"DBLP:journals\/pacmpl\/CockxTW21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434341","article-title":"The taming of the rew: a type theory with computational assumptions","volume":"5","author":"Cockx","year":"2021","journal-title":"Proc. ACM Program. Lang."},{"key":"DBLP:conf\/lics\/CoquandHM18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1145\/3209108.3209197","article-title":"On Higher Inductive Types in Cubical Type Theory","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018","author":"Coquand","year":"2018"},{"key":"DBLP:conf\/types\/Dybjer95","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","article-title":"Internal Type Theory","volume-title":"Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers","volume":"1158","author":"Dybjer","year":"1995"},{"volume-title":"Une s\u00e9mantique cat\u00e9gorique des types d\u00e9pendents","year":"1988","author":"Ehrhard","key":"ehrhard"},{"key":"DBLP:journals\/pacmpl\/GilbertCST19","doi-asserted-by":"publisher","DOI":"10.1145\/3290316","article-title":"Definitional proof-irrelevance without K","volume":"3","author":"Gilbert","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"issue":"1","key":"DBLP:journals\/jacm\/HarperHP93","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A Framework for Defining Logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"DBLP:conf\/lics\/Hofmann99","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1109\/LICS.1999.782616","article-title":"Semantical Analysis of Higher-Order Abstract Syntax","volume-title":"14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999","author":"Hofmann","year":"1999"},{"key":"glue","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25","article-title":"Gluing for Type Theory","volume-title":"4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)","volume":"131","author":"Kaposi","year":"2019"},{"key":"DBLP:journals\/pacmpl\/KaposiKA19","doi-asserted-by":"publisher","DOI":"10.1145\/3290315","article-title":"Constructing quotient inductive-inductive types","volume":"3","author":"Kaposi","year":"2019","journal-title":"Proc. ACM Program. Lang."},{"key":"DBLP:conf\/mpc\/KaposiKK19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-030-33636-3_12","article-title":"Shallow Embedding of Type Theory is Morally Correct","volume-title":"Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings","volume":"11825","author":"Kaposi","year":"2019"},{"key":"DBLP:conf\/fscd\/KaposiX24","series-title":"LIPIcs","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2024.10","article-title":"Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics","volume-title":"9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia","volume":"299","author":"Kaposi","year":"2024"},{"key":"singleTypes","article-title":"Type theory in type theory using single substitutions","volume-title":"30th International Conference on Types for Proofs and Programs (TYPES 2024)","author":"Kaposi","year":"2024"},{"key":"kaposi-qiit-setoid","article-title":"Quotient inductive-inductive types in the setoid model","volume-title":"27th International Conference on Types for Proofs and Programs, TYPES 2021","author":"Kaposi","year":"2021"},{"volume-title":"Type-Theoretic Signatures for Algebraic Theories and Inductive Types","year":"2022","author":"Kov\u00e1cs","key":"andras"},{"key":"MARTINLOF197573","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0049-237X(08)71945-1","article-title":"An Intuitionistic Theory of Types: Predicative Part","volume-title":"Logic Colloquium '73","volume":"80","author":"Martin-L\u00f6f","year":"1975"},{"volume-title":"Cubical models are cofreely parametric. (Les mod\u00e8les cubiques sont colibrement param\u00e9triques)","year":"2022","author":"Moeneclaey","key":"DBLP:phd\/hal\/Moeneclaey22"},{"key":"beluga","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","article-title":"Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)","volume-title":"Automated Reasoning","author":"Pientka","year":"2010"},{"volume-title":"Types and programming languages","year":"2002","author":"Pierce","key":"DBLP:books\/daglib\/0005958"},{"volume-title":"Computing with Extensionality Principles in Type Theory. (Calculer avec des Principes d'Extensionnalit\u00e9 en Th\u00e9orie des Types)","year":"2022","author":"Pujet","key":"DBLP:phd\/hal\/Pujet22"},{"issue":"5","key":"DBLP:journals\/jar\/SozeauABCFKMTW20","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/S10817-019-09540-0","article-title":"The MetaCoq Project","volume":"64","author":"Sozeau","year":"2020","journal-title":"J. Autom. Reason."},{"key":"DBLP:phd\/us\/Sterling22","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/19632681.V1","volume-title":"First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory","author":"Sterling","year":"2022"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013","author":"The Univalent Foundations Program","key":"HoTTbook"},{"volume-title":"Abstract and Concrete Type Theories","year":"2021","author":"Uemura","key":"uemura"},{"key":"DBLP:journals\/jfp\/VezzosiMA21","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034","article-title":"Cubical Agda: A dependently typed programming language with univalence and higher inductive types","volume":"31","author":"Vezzosi","year":"2021","journal-title":"J. Funct. Program."}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T11:11:20Z","timestamp":1760526680000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2510.12303v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,14]]},"references-count":47,"URL":"https:\/\/doi.org\/10.4204\/eptcs.431.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"type":"electronic","value":"2075-2180"}],"subject":[],"published":{"date-parts":[[2025,10,14]]}}}