{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:56:24Z","timestamp":1767927384192,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394770","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"648-661","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Large and Infinitary Quotient Inductive-Inductive Types"],"prefix":"10.1145","author":[{"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ambrus","family":"Kaposi","sequence":"additional","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Benedikt Ahrens and Peter LeFanu Lumsdaine. 2019. Displayed Categories. Logical Methods in Computer Science 15 1 (2019). https: \/\/doi.org\/10.23638\/LMCS-15(1:20)2019 Benedikt Ahrens and Peter LeFanu Lumsdaine. 2019. Displayed Categories. Logical Methods in Computer Science 15 1 (2019). https: \/\/doi.org\/10.23638\/LMCS-15(1:20)2019"},{"key":"e_1_3_2_1_2_1","volume-title":"Foundations of Software Science and Computation Structures -21st International Conference, FOSSACS","author":"Altenkirch Thorsten","year":"2018"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_31"},{"key":"e_1_3_2_1_4_1","unstructured":"Carlo Angiuli Robert Harper and Todd Wilson. 2016. Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR abs\/1604.08873 (2016). arXiv:1604.08873 http:\/\/arxiv.org\/abs\/1604.08873 Carlo Angiuli Robert Harper and Todd Wilson. 2016. Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR abs\/1604.08873 (2016). arXiv:1604.08873 http:\/\/arxiv.org\/abs\/1604.08873"},{"key":"e_1_3_2_1_5_1","volume-title":"Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018","volume":"119","author":"Angiuli Carlo","year":"2018"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209130"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_8_1","volume-title":"19th International Conference on Types for Proofs and Programs, TYPES 2013","volume":"26","author":"Bezem Marc","year":"2013"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_1_10_1","unstructured":"Guillaume Brunerie. 2019. A formalization of the initiality conjecture in Agda. (August 2019). https:\/\/guillaumebrunerie.github.io\/pdf\/initiality.pdf Slides of a talk at the Homotopy Type Theory 2019 Conference Carnegie Mellon University Pittsburgh Pennsylvania. Guillaume Brunerie. 2019. A formalization of the initiality conjecture in Agda. (August 2019). https:\/\/guillaumebrunerie.github.io\/pdf\/initiality.pdf Slides of a talk at the Homotopy Type Theory 2019 Conference Carnegie Mellon University Pittsburgh Pennsylvania."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Pierre Clairambault and Peter Dybjer. 2014. The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24 6 (2014). https:\/\/doi.org\/10.1017\/S0960129513000881 Pierre Clairambault and Peter Dybjer. 2014. The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24 6 (2014). https:\/\/doi.org\/10.1017\/S0960129513000881","DOI":"10.1017\/S0960129513000881"},{"key":"e_1_3_2_1_15_1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Cohen Cyril","year":"2015"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_3_2_1_17_1","unstructured":"Gabe Dijkstra. 2017. Quotient inductive-inductive definitions. Ph.D. Dissertation. University of Nottingham UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.728471 Gabe Dijkstra. 2017. Quotient inductive-inductive definitions. Ph.D. Dissertation. University of Nottingham UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.728471"},{"key":"e_1_3_2_1_18_1","volume-title":"International Workshop TYPES'95","volume":"1158","author":"Dybjer Peter","year":"1995"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.019"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Peter T Johnstone. 2002. Sketches of an elephant: A topos theory compendium. Vol. 1. Oxford University Press. Peter T Johnstone. 2002. Sketches of an elephant: A topos theory compendium. Vol. 1. Oxford University Press.","DOI":"10.1093\/oso\/9780198515982.003.0004"},{"key":"e_1_3_2_1_22_1","unstructured":"Ambrus Kaposi and Andr\u00e1s Kov\u00e1cs. 2019. Signatures and Induction Principles for Higher Inductive-Inductive Types. CoRR abs\/1902.00297 (2019). arXiv:1902.00297 http:\/\/arxiv.org\/abs\/1902.00297 Ambrus Kaposi and Andr\u00e1s Kov\u00e1cs. 2019. Signatures and Induction Principles for Higher Inductive-Inductive Types. CoRR abs\/1902.00297 (2019). arXiv:1902.00297 http:\/\/arxiv.org\/abs\/1902.00297"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Thorsten Altenkirch. 2019. Constructing quotient inductive-inductive types. PACMPL 3 POPL (2019) 2:1--2:24. https:\/\/doi.org\/10.1145\/3290315 Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Thorsten Altenkirch. 2019. Constructing quotient inductive-inductive types. PACMPL 3 POPL (2019) 2:1--2:24. https:\/\/doi.org\/10.1145\/3290315","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_1_24_1","unstructured":"Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Lafont Ambroise. 2019. For Induction-Induction Induction is Enough. Submitted to TYPES 2019 post-proceedings (2019). https:\/\/github.com\/amblafont\/UniversalII\/blob\/cwf-syntax\/paper\/paper.pdf Ambrus Kaposi Andr\u00e1s Kov\u00e1cs and Lafont Ambroise. 2019. For Induction-Induction Induction is Enough. Submitted to TYPES 2019 post-proceedings (2019). https:\/\/github.com\/amblafont\/UniversalII\/blob\/cwf-syntax\/paper\/paper.pdf"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S030500411900015X"},{"key":"e_1_3_2_1_26_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book\/ The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_1_28_1","unstructured":"Jonathan Sterling. 2019. Algebraic type theory and universe hierarchies. arXiv preprint arXiv:1902.08848 (2019). Jonathan Sterling. 2019. Algebraic type theory and universe hierarchies. arXiv preprint arXiv:1902.08848 (2019)."},{"key":"e_1_3_2_1_29_1","unstructured":"Thomas Streicher. 2012. Semantics of type theory: correctness completeness and independence results. Springer Science & Business Media. Thomas Streicher. 2012. Semantics of type theory: correctness completeness and independence results. Springer Science & Business Media."},{"key":"e_1_3_2_1_30_1","volume-title":"Cumulative Inductive Types In Coq. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","volume":"108","author":"Timany Amin","year":"2018"},{"key":"e_1_3_2_1_31_1","unstructured":"Niels van der Weide. 2016. Higher Inductive Types. Master's thesis. Radboud University Nijmegen. Niels van der Weide. 2016. Higher Inductive Types. Master's thesis. Radboud University Nijmegen."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Andrea Vezzosi Anders M\u00f6rtberg and Andreas Abel. 2019. Cubical agda: a dependently typed programming language with univalence and higher inductive types. PACMPL 3 ICFP (2019) 87:1--87:29. https: \/\/doi.org\/10.1145\/3341691 Andrea Vezzosi Anders M\u00f6rtberg and Andreas Abel. 2019. Cubical agda: a dependently typed programming language with univalence and higher inductive types. PACMPL 3 ICFP (2019) 87:1--87:29. https: \/\/doi.org\/10.1145\/3341691","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_1_33_1","unstructured":"Vladimir Voevodsky. 2011. Resizing rules slides from a talk at TYPES2011. At author's webpage (2011). https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/2011_Bergen.pdf Vladimir Voevodsky. 2011. Resizing rules slides from a talk at TYPES2011. At author's webpage (2011). https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/2011_Bergen.pdf"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394770","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394770"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":33,"alternative-id":["10.1145\/3373718.3394770","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394770","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}