{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:03:17Z","timestamp":1770296597005,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030719944","type":"print"},{"value":"9783030719951","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-L\u00f6f type theory with constructs that give full access to the extensionality principles that hold in the setoid model.<\/jats:p><jats:p>Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_1","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Constructing a universe for the setoid model"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6582-5025","authenticated-orcid":false,"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[]},{"given":"Simon","family":"Boulier","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9897-8936","authenticated-orcid":false,"given":"Ambrus","family":"Kaposi","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Sattler","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8701-5613","authenticated-orcid":false,"given":"Filippo","family":"Sestini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"1_CR1","unstructured":"Andreas Abel. Extensional normalization in the logical framework with proof irrelevant equality. In Olivier Danvy, editor, Workshop on Normalization by Evaluation, affiliated to LiCS 2009, Los Angeles, 15 August 2009, 2009."},{"key":"1_CR2","unstructured":"Andreas Abel and Thierry Coquand. Failure of normalization in impredicative type theory with proof-irrelevant propositional equality, 2019. arXiv:1911.08174."},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Peter Aczel. The type theoretic interpretation of constructive set theory. In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium \u201977, volume\u00a096 of Studies in Logic and the Foundations of Mathematics, pages 55 \u2013 66. Elsevier, 1978. URL: http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X0871989X, doi:https:\/\/doi.org\/10.1016\/S0049-237X(08)71989-X.","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"1_CR4","unstructured":"Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pages 412\u2013420. IEEE Computer Society Press, July 1999."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau. Setoid type theory\u2014a syntactic translation. In Graham Hutton, editor, Mathematics of Program Construction, pages 155\u2013196, Cham, 2019. Springer International Publishing.","DOI":"10.1007\/978-3-030-33636-3_7"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. SIGPLAN Not., 51(1):18\u201329, January 2016. URL: https:\/\/doi.org\/10.1145\/2914770.2837638, doi:https:\/\/doi.org\/10.1145\/2914770.2837638.","DOI":"10.1145\/2914770.2837638"},{"key":"1_CR7","unstructured":"Thorsten Altenkirch, Ambrus Kaposi, Andr\u00e1s Kov\u00e1cs, and Jakob von Raumer. Reducing inductive-inductive types to indexed inductive types. In Jos\u00e9 Esp\u00edrito\u00a0Santo and Lu\u00eds Pinto, editors, 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho, 2018."},{"key":"1_CR8","unstructured":"Thorsten Altenkirch, Ambrus Kaposi, Andr\u00e1s Kov\u00e1cs, and Jakob von Raumer. Constructing inductive-inductive types via type erasure. In Marc Bezem, editor, 25th International Conference on Types for Proofs and Programs, TYPES 2019. Centre for Advanced Study at the Norwegian Academy of Science and Letters, 2019."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In PLPV \u201907: Proceedings of the 2007 workshop on Programming languages meets program verification, pages 57\u201368, New York, NY, USA, 2007. ACM. doi:http:\/\/doi.acm.org\/10.1145\/1292597.1292608.","DOI":"10.1145\/1292597.1292608"},{"key":"1_CR10","unstructured":"Thorsten Altenkrich, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. Agda formalization of the setoid universe. https:\/\/bitbucket.org\/taltenkirch\/setoid-univ, 2021."},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume\u00a026 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107\u2013128, Dagstuhl, Germany, 2014. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. URL: http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2014\/4628, doi:https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2013.107.","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"1_CR12","unstructured":"Simon Boulier. Extending Type Theory with Syntactical Models. PhD thesis, IMT Atlantique, 2018."},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume\u00a069 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1\u20135:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik. URL: http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/8475, doi:https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2015.5.","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. Internal type theory. In International Workshop on Types for Proofs and Programs, pages 120\u2013134. Springer, 1995.","DOI":"10.1007\/3-540-61780-9_66"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65, 06 2003. doi:https:\/\/doi.org\/10.2307\/2586554.","DOI":"10.2307\/2586554"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 129\u2013146, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.","DOI":"10.1007\/3-540-48959-2_11"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Ga\u00ebtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages, pages 1\u201328, January 2019. URL: https:\/\/hal.inria.fr\/hal-01859964, doi:https:\/\/doi.org\/10.1145\/329031610.1145\/3290316.","DOI":"10.1145\/329031610.1145\/3290316"},{"key":"1_CR18","unstructured":"Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Conservativity of equality reflection over intensional type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 153\u2013164, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.","DOI":"10.1007\/3-540-61780-9_68"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume\u00a036 of Oxford Logic Guides, pages 83\u2013111. Oxford Univ. Press, New York, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Ambrus Kaposi, Andr\u00e1s Kov\u00e1cs, and Ambroise Lafont. For finitary induction-induction, induction is enough. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1\u20136:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik. URL: https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13070, doi:https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2019.6.","DOI":"10.4230\/LIPIcs.TYPES.2019.6"},{"key":"1_CR22","unstructured":"Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock, and Conor McBride. Small induction recursion, indexed containers and dependent polynomials are equivalent, 2013. TLCA 2013."},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium \u201973, volume\u00a080 of Studies in Logic and the Foundations of Mathematics, pages 73 \u2013 118. Elsevier, 1975. URL: http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X08719451, doi:https:\/\/doi.org\/10.1016\/S0049-237X(08)71945-1.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"1_CR24","unstructured":"Per Martin-L\u00f6f. Intuitionistic type theory, volume\u00a01 of Studies in proof theory. Bibliopolis, 1984."},{"key":"1_CR25","unstructured":"Fredrik Nordvall\u00a0Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013."},{"key":"1_CR26","unstructured":"Erik Palmgren. From type theory to setoids and back. arXiv e-prints, page arXiv:1909.01414, September 2019. arXiv:1909.01414."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Erik Palmgren and Olov Wilander. Constructing categories and setoids of setoids in type theory. arXiv e-prints, page arXiv:1408.1364, August 2014. arXiv:1408.1364.","DOI":"10.2168\/LMCS-10(3:25)2014"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1\u201331:25. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2019. URL: http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10538, doi:https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.31.","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"1_CR29","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."}],"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-71995-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:04:14Z","timestamp":1616432654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"88","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":"28","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,2","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":"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 changed to an online format due to the COVID-19 pandemic","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)"}}]}}