**Setoid type theory-a syntactic translation**
(2019)

Conference Proceeding

Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019). Setoid type theory-a syntactic translation. In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedingshttps://doi.org/10.1007/978-3-030-33636-3_7

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a s... Read More about Setoid type theory-a syntactic translation.