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.
Author supplied keywords
Cite
CITATION STYLE
Altenkirch, T., Boulier, S., Kaposi, A., & Tabareau, N. (2019). Setoid Type Theory—A Syntactic Translation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11825 LNCS, pp. 155–196). Springer. https://doi.org/10.1007/978-3-030-33636-3_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
