“Constructing a universe for the setoid model”
Giovedì 9 Giugno 2022, ore 15:00 - Aula 2AB40 - Filippo Sestini (PhD student - University of Nottingham, UK)
Abstract
Setoids are known to provide semantics for dependent type theory with extensionality. A strict version of the setoid model by Altenkirch gives rise to a model of intensional type theory with function extensionality and a universe of propositions where equality is propositional equivalence.
In this talk, we present how we extended the strict setoid model with a universe of setoids.
Despite initially formulating the universe as an infinitary inductive-recursive-recursive type, our final version can entirely be defined as a simple inductive family. We achieved this by applying, in a novel way, known techniques to reduce complex forms of induction to simpler ones.
As a consequence, our meta-theory is a relatively simple extension of intensional Martin-Löf type theory, where the only unusual aspect is a definitionally proof-irrelevant identity type that can eliminate into proof-relevant types.
Our constructions have been fully formalized in the Agda proof-assistant.
This is joint work with T. Altenkirch, S. Boulier, A. Kaposi, C. Sattler.
