{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:29:51Z","timestamp":1784255391632,"version":"3.55.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel\u2019s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_14","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"257-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Constructing Infinitary Quotient-Inductive Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8558-3492","authenticated-orcid":false,"given":"Marcelo P.","family":"Fiore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7775-3471","authenticated-orcid":false,"given":"Andrew M.","family":"Pitts","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3105-4098","authenticated-orcid":false,"given":"S. C.","family":"Steenkamp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science vol. 342(1), 3\u201327 (2005). DOI: 10.1016\/j.tcs.2005.06.002.","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Abel, A.: Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types. Electronic Proceedings in Theoretical Computer Science vol. 77, 1\u201311 (2012). DOI: 10.4204\/EPTCS.77.1.","DOI":"10.4204\/EPTCS.77.1"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B.: Well-Founded Recursion with Copatterns and Sized Types. J. Funct. Prog. vol. 26, e2 (2016). DOI: 10.1017\/S0956796816000022.","DOI":"10.1017\/S0956796816000022"},{"key":"14_CR4","unstructured":"Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., Nordvall Forsberg, F.: Quotient Inductive-Inductive Types. In: Baier, C., Dal Lago, U. (eds.) Foundations of Software Science and Computation Structures, FoSSaCS 2018, LNCS, vol. 10803, pp. 293\u2013310. Springer, Heidelberg (2018)."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Kaposi, A.: Type Theory in Type Theory Using Quotient Inductive Types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2016, pp. 18\u201329. ACM Press, St. Petersburg, FL, USA (2016). DOI: 10.1145\/2837614.2837638.","DOI":"10.1145\/2837614.2837638"},{"key":"14_CR6","unstructured":"Basold, H., Geuvers, H., van der Weide, N.: Higher Inductive Types in Programming. Journal of Universal Computer Science vol. 23 (1), 27 (2017). DOI: 10.3217\/jucs-023-01-0063."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Blass, A.: Words, Free Algebras, and Coequalizers. Fundamenta Mathematicae vol. 117 (2), 117\u2013160 (1983).","DOI":"10.4064\/fm-117-2-117-160"},{"key":"14_CR8","unstructured":"Cockx, J., Abel, A.: \u201cSprinkles of Extensionality for Your Vanilla Type Theory\u201d. Abstract for the 22nd International Conference on Types for Proofs and Programs (TYPES 2016), Novi Sad, Serbia."},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Cockx, J., Abel, A.: Elaborating Dependent (Co)Pattern Matching. Proceedings of the ACM on Programming Languages vol. 2, 1\u201330 (2018). DOI: 10.1145\/3236770.","DOI":"10.1145\/3236770"},{"key":"14_CR10","unstructured":"Dijkstra, G.: Quotient Inductive-Inductive Definitions. PhD thesis, University of Nottingham (2017), URL: http:\/\/eprints.nottingham.ac.uk\/42317\/1\/thesis.pdf."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Representing Inductively Defined Sets by Well orderings in Martin-L\u00f6f\u2019s Type Theory. Theoretical Computer Science vol. 176 (1-2), 329\u2013335 (1997). DOI: 10.1016\/S0304-3975(96)00145-4.","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Dybjer, P., Moeneclaey, H.: Finitary Higher Inductive Types in the Groupoid Model. Electronic Notes in Theoretical Computer Science vol. 336, 119\u2013134 (2018). DOI: 10.1016\/j.entcs.2018.03.019.","DOI":"10.1016\/j.entcs.2018.03.019"},{"key":"14_CR13","unstructured":"Fiore, M.: An Equational Metalogic for Monadic Equational Systems. Theory and Applications of Categories vol. 27(18), 464\u2013492 (2013). URL: https:\/\/emis.de\/journals\/TAC\/volumes\/27\/18\/27-18.pdf."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Fiore, M., Hur, C.-K.: On the Construction of Free Algebras for Equational Systems. Theoretical Computer Science vol. 410(18), 1704\u20131729 (2009). DOI: 10.1016\/j.tcs.2008.12.052.","DOI":"10.1016\/j.tcs.2008.12.052"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Forsberg, F.N., Setzer, A.: A Finite Axiomatisation of Inductive-Inductive Definitions. In: Berger, U., Diener, H., Schuster, P., Seisenberger, M. (eds.) Logic, Construction, Computation, Ontos mathematical logic, pp. 259\u2013287. De Gruyter (2012). DOI: 10.1515\/9783110324921.259.","DOI":"10.1515\/9783110324921.259"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Gambino, N., Kock, J.: Polynomial Functors and Polynomial Monads. Math. Proc. Camb. Phil. Soc. vol. 154 (1), 153\u2013192 (2013). DOI: 10.1017\/S0305004112000394.","DOI":"10.1017\/S0305004112000394"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Gitik, M.: All Uncountable Cardinals Can Be Singular. Israel J. Math. vol. 35 (1\u20132), 61\u201388 (1980).","DOI":"10.1007\/BF02760939"},{"key":"14_CR18","unstructured":"Hofmann, M.: Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh (1995)."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Kaposi, A., Kov\u00e1cs, A., Altenkirch, T.: Constructing Quotient Inductive-Inductive Types. Proc. ACM Program. Lang. vol. 3, 1\u201324 (2019). DOI: 10.1145\/3290315.","DOI":"10.1145\/3290315"},{"key":"14_CR20","unstructured":"Kelly, M.: A Unified Treatment of Transfinite Constructions for Free Algebras, Free Monoids, Colimits, Associated Sheaves, and so on. Bull. Austral. Math. Soc. vol. 22, 1\u201383 (1980)."},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Lumsdaine, P.L., Shulman, M.: Semantics of Higher Inductive Types. Math. Proc. Camb. Phil. Soc. (2019). DOI: 10.1017\/S030500411900015X.","DOI":"10.1017\/S030500411900015X"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Martin-L\u00f6f, P.: Constructive Mathematics and Computer Programming. In: Cohen, L.J., \u0141o\u015b, J., Pfeiffer, H., Podewski, K.-P. (eds.) Studies in Logic and the Foundations of Mathematics, pp. 153\u2013175. Elsevier (1982). https:\/\/doi.org\/10.1016\/S0049-237X(09)70189-210.1016\/S0049-237X(09)70189-2.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"14_CR23","unstructured":"McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)."},{"key":"14_CR24","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press (1990)."},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Shulman, M.: Brouwer\u2019s Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory. Mathematical Structures in Computer Science vol. 28, 856\u2013941 (2018).","DOI":"10.1017\/S0960129517000147"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Sojakova, K.: Higher Inductive Types as Homotopy-Initial Algebras. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages \u2013 POPL \u201915, pp.31\u201342. ACM Press, Mumbai, India (2015). DOI: 10.1145\/2676726.2676983.","DOI":"10.1145\/2676726.2676983"},{"key":"14_CR27","unstructured":"Streicher, T.: Investigations into Intensional Type Theory. Habilitation Thesis, Ludwig Maximilian University (1993)."},{"key":"14_CR28","unstructured":"Swan, A.: W-Types with Reductions and the Small Object Argument. (2018). arXiv:1802.07588 [math]."},{"key":"14_CR29","unstructured":"The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/homotopytypetheory.org\/book, Institute for Advanced Study (2013)."},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Vezzosi, A., M\u00f6rtberg, A., Abel, A.: Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proc. ACM Program. Lang. vol. 3 (ICFP), 87:1\u201387:29 (2019). DOI: 10.1145\/3341691.","DOI":"10.1145\/3341691"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:44:14Z","timestamp":1610027054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}