{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:04Z","timestamp":1753894384911,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,2,1]],"date-time":"2022-02-01T00:00:00Z","timestamp":1643673600000},"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>The functorial structure of type constructors is the foundation for many\ndefinition and proof principles in higher-order logic (HOL). For example,\ninductive and coinductive datatypes can be built modularly from bounded natural\nfunctors (BNFs), a class of well-behaved type constructors. Composition,\nfixpoints, and, under certain conditions, subtypes are known to preserve the\nBNF structure. In this article, we tackle the preservation question for\nquotients, the last important principle for introducing new types in HOL. We\nidentify sufficient conditions under which a quotient inherits the BNF\nstructure from its underlying type. Surprisingly, lifting the structure in the\nobvious manner fails for some quotients, a problem that also affects the\nquotients of polynomial functors used in the Lean proof assistant. We provide a\nstrictly more general lifting scheme that supports such problematic quotients.\nWe extend the Isabelle\/HOL proof assistant with a command that automates the\nregistration of a quotient type as a BNF, reducing the proof burden on the user\nfrom the full set of BNF axioms to our inheritance conditions. We demonstrate\nthe command's usefulness through several case studies.<\/jats:p>","DOI":"10.46298\/lmcs-18(1:23)2022","type":"journal-article","created":{"date-parts":[[2022,2,2]],"date-time":"2022-02-02T12:55:56Z","timestamp":1643806556000},"source":"Crossref","is-referenced-by-count":0,"title":["Quotients of Bounded Natural Functors"],"prefix":"10.46298","volume":"Volume 18, Issue 1","author":[{"given":"Basil","family":"F\u00fcrer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5851-494X","authenticated-orcid":false,"given":"Andreas","family":"Lochbihler","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8253-4513","authenticated-orcid":false,"given":"Joshua","family":"Schneider","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7982-2768","authenticated-orcid":false,"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,2,1]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9022\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9022\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:19:49Z","timestamp":1687292389000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7354"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,1]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(1:23)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2104.05348v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2104.05348v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2104.05348","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2104.05348","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,2,1]]},"article-number":"7354"}}