1Functional Programming Laboratory (Functional Programming Laboratory School of Computer Science University of Nottingham Jubilee Campus, Wollaton Road Nottingham NG8 1BB United Kingdom - United Kingdom)
Abstract : We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a def-initional computation rule for transport. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We conjecture that our syntax is complete with regards to this translation.
https://hal.inria.fr/hal-02281225
Contributor : Nicolas Tabareau
<>
Submitted on : Sunday, September 8, 2019 - 11:55:23 PM
Last modification on : Tuesday, September 10, 2019 - 1:18:26 AM
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau. Setoid type theory - a syntactic translation. Mathematics of Program Construction, Oct 2019, Porto, Portugal. ⟨hal-02281225⟩
