Constructing a universe for the setoid model
(2021)
Conference Proceeding
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
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 pr... Read More about Constructing a universe for the setoid model.