| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Setoid type theory - a syntactic translation
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 definitional 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.
Cited literature [34 references]
https://hal.inria.fr/hal-02281225
Contributor : Nicolas Tabareau <>
Submitted on : Sunday, September 8, 2019 - 11:55:23 PM
Last modification on : Tuesday, January 5, 2021 - 4:26:24 PM
Long-term archiving on: : Thursday, February 6, 2020 - 6:13:02 PM
Contributor : Nicolas Tabareau <>
Submitted on : Sunday, September 8, 2019 - 11:55:23 PM
Last modification on : Tuesday, January 5, 2021 - 4:26:24 PM
Long-term archiving on: : Thursday, February 6, 2020 - 6:13:02 PM
File
mpc2019.pdf
Files produced by the author(s)