Skip to Main content Skip to Navigation
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Nicolas Tabareau Connect in order to contact the contributor
Submitted on : Sunday, September 8, 2019 - 11:55:23 PM
Last modification on : Wednesday, November 3, 2021 - 4:23:45 AM
Long-term archiving on: : Thursday, February 6, 2020 - 6:13:02 PM


Files produced by the author(s)



Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau. Setoid type theory - a syntactic translation. MPC 2019 - 13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩. ⟨hal-02281225⟩



Les métriques sont temporairement indisponibles