{"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":1784255391242,"version":"3.55.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T00:00:00Z","timestamp":1654560000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper introduces an expressive class of indexed quotient-inductive\ntypes, called QWI types, within the framework of constructive type theory. They\nare initial algebras for indexed families of equational theories with possibly\ninfinitary operators and equations. We prove that QWI types can be derived from\nquotient types and inductive types in the type theory of toposes with natural\nnumber object and universes, provided those universes satisfy the Weakly\nInitial Set of Covers (WISC) axiom. We do so by constructing QWI types as\ncolimits of a family of approximations to them defined by well-founded\nrecursion over a suitable notion of size, whose definition involves the WISC\naxiom. We developed the proof and checked it using the Agda theorem prover.<\/jats:p>","DOI":"10.46298\/lmcs-18(2:15)2022","type":"journal-article","created":{"date-parts":[[2022,6,8]],"date-time":"2022-06-08T14:51:41Z","timestamp":1654699901000},"source":"Crossref","is-referenced-by-count":7,"title":["Quotients, inductive types, and quotient inductive types"],"prefix":"10.46298","volume":"Volume 18, Issue 2","author":[{"given":"Marcelo P.","family":"Fiore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":"25203","published-online":{"date-parts":[[2022,6,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9655\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9655\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:19:23Z","timestamp":1687292363000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7076"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(2:15)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2101.02994v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.02994v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.02994v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2101.02994","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2101.02994","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,7]]},"article-number":"7076"}}