Constructing a universe for the setoid model

Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Sattler, Christian; Sestini, Filippo

Abstract

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öf type theory with constructs that give full access to the extensionality principles that hold in the setoid model.

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.

Citation

Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021). Constructing a universe for the setoid model. In S. Kiefer, & C. Tasson (Eds.), Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings (1-21). https://doi.org/10.1007/978-3-030-71995-1_1

• Presentation Conference Type: Edited Proceedings
• Conference Name: 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021)
• Start Date: Mar 27, 2021
• End Date: Apr 1, 2021
• Acceptance Date: Feb 1, 2021
• Online Publication Date: Mar 23, 2021
• Publication Date: Mar 23, 2021
• Deposit Date: May 28, 2021
• Publicly Available Date: Jun 1, 2021
• Publisher: Springer Publishing Company
• Pages: 1-21
• Series Title: Lecture notes in computer science
• Series Number: 12650
• Series ISSN: 0302-9743
• Book Title: Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 202
• ISBN: 9783030719944
• DOI: https://doi.org/10.1007/978-3-030-71995-1_1
• Public URL: https://nottingham-repository.worktribe.com/output/5421642
• Publisher URL: https://link.springer.com/chapter/10.1007%2F978-3-030-71995-1_1