{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T10:40:46Z","timestamp":1776854446343,"version":"3.51.2"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.<\/jats:p>","DOI":"10.1145\/3290315","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Constructing quotient inductive-inductive types"],"prefix":"10.1145","volume":"3","author":[{"given":"Ambrus","family":"Kaposi","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"additional","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_2_2_2_1","unstructured":"Benedikt Ahrens and Peter LeFanu Lumsdaine. 2017. Displayed Categories. arXiv: arXiv:1705.04296  Benedikt Ahrens and Peter LeFanu Lumsdaine. 2017. Displayed Categories. arXiv: arXiv:1705.04296"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209130"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934514"},{"key":"e_1_2_2_8_1","first-page":"1","article-title":"Higher Inductive Types in Programming","volume":"23","author":"Basold Henning","year":"2017","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158132"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863547"},{"key":"e_1_2_2_13_1","volume-title":"The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24, 6","author":"Clairambault Pierre","year":"2014"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"e_1_2_2_15_1","volume-title":"Cubical Type Theory: a constructive interpretation of the univalence axiom. CoRR abs\/1611.02108","author":"Cohen Cyril","year":"2016"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_17_1","series-title":"Lecture Notes in Computer Science","volume-title":"Internal Type Theory","author":"Dybjer Peter"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.019"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. 1995a. Conservativity of Equality Reflection over Intensional Type Theory.. In TYPES 95. 153\u2013164.   Martin Hofmann. 1995a. Conservativity of Equality Reflection over Intensional Type Theory.. In TYPES 95. 153\u2013164.","DOI":"10.1007\/3-540-61780-9_68"},{"key":"e_1_2_2_22_1","volume-title":"Extensional concepts in intensional type theory","author":"Hofmann Martin"},{"key":"e_1_2_2_24_1","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs)) , H\u00e9l\u00e8ne Kirchner (Ed.)","volume":"108","author":"Kaposi Ambrus","year":"2018"},{"key":"e_1_2_2_25_1","unstructured":"Peter LeFanu Lumsdaine and Mike Shulman. 2017. Semantics of higher inductive types. arXiv: arXiv:1705.07088  Peter LeFanu Lumsdaine and Mike Shulman. 2017. Semantics of higher inductive types. arXiv: arXiv:1705.07088"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.33"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_18"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds John C.","year":"1983"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_2_2_34_1","volume-title":"24th International Conference on Types for Proofs and Programs, TYPES 2018 , Jos\u00e9 Esp\u00edrito Santo and Lu\u00eds Pinto (Eds.)","author":"Winterhalter Th\u00e9o","year":"2018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290315","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290315"],"URL":"https:\/\/doi.org\/10.1145\/3290315","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}