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.
T. Altenkirch—Supported by USAF grant FA9550-16-1-0029.
S. Boulier—Supported by ERC Starting Grant CoqHoTT 637339.
A. Kaposi—Supported by the Bolyai Fellowship of the Hungarian Academy of Sciences (BO/00659/19/3) and by the “Application Domain Specific Highly Reliable IT Solutions” project that has been implemented with support from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 funding scheme.
C. Sattler—Supported by USAF grant FA9550-16-1-0029 and Swedish Research Council grant 2019-03765.
Chapter PDF
Similar content being viewed by others
Keywords
References
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.
Andreas Abel and Thierry Coquand. Failure of normalization in impredicative type theory with proof-irrelevant propositional equality, 2019. arXiv:1911.08174.
Peter Aczel. The type theoretic interpretation of constructive set theory. In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55 – 66. Elsevier, 1978. URL: http://www.sciencedirect.com/science/article/pii/S0049237X0871989X, doi:https://doi.org/10.1016/S0049-237X(08)71989-X.
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–420. IEEE Computer Society Press, July 1999.
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau. Setoid type theory—a syntactic translation. In Graham Hutton, editor, Mathematics of Program Construction, pages 155–196, Cham, 2019. Springer International Publishing.
Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. SIGPLAN Not., 51(1):18–29, January 2016. URL: https://doi.org/10.1145/2914770.2837638, doi:https://doi.org/10.1145/2914770.2837638.
Thorsten Altenkirch, Ambrus Kaposi, András Kovács, and Jakob von Raumer. Reducing inductive-inductive types to indexed inductive types. In José Espírito Santo and Luís Pinto, editors, 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho, 2018.
Thorsten Altenkirch, Ambrus Kaposi, András Kovács, 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.
Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In PLPV ’07: Proceedings of the 2007 workshop on Programming languages meets program verification, pages 57–68, New York, NY, USA, 2007. ACM. doi:http://doi.acm.org/10.1145/1292597.1292608.
Thorsten Altenkrich, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. Agda formalization of the setoid universe. https://bitbucket.org/taltenkirch/setoid-univ, 2021.
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 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107–128, Dagstuhl, Germany, 2014. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2014/4628, doi:https://doi.org/10.4230/LIPIcs.TYPES.2013.107.
Simon Boulier. Extending Type Theory with Syntactical Models. PhD thesis, IMT Atlantique, 2018.
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 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 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2018/8475, doi:https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
Peter Dybjer. Internal type theory. In International Workshop on Types for Proofs and Programs, pages 120–134. Springer, 1995.
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.
Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 129–146, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages, pages 1–28, January 2019. URL: https://hal.inria.fr/hal-01859964, doi:https://doi.org/10.1145/329031610.1145/3290316.
Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, University of Edinburgh, 1995.
Martin Hofmann. Conservativity of equality reflection over intensional type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 153–164, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.
Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83–111. Oxford Univ. Press, New York, 1998.
Ambrus Kaposi, András Kovács, 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–6:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2020/13070, doi:https://doi.org/10.4230/LIPIcs.TYPES.2019.6.
Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock, and Conor McBride. Small induction recursion, indexed containers and dependent polynomials are equivalent, 2013. TLCA 2013.
Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium ’73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73 – 118. Elsevier, 1975. URL: http://www.sciencedirect.com/science/article/pii/S0049237X08719451, doi:https://doi.org/10.1016/S0049-237X(08)71945-1.
Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in proof theory. Bibliopolis, 1984.
Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013.
Erik Palmgren. From type theory to setoids and back. arXiv e-prints, page arXiv:1909.01414, September 2019. arXiv:1909.01414.
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.
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–31:25. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. URL: http://drops.dagstuhl.de/opus/volltexte/2019/10538, doi:https://doi.org/10.4230/LIPIcs.FSCD.2019.31.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., Sestini, F. (2021). Constructing a universe for the setoid model. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)