Underlying representation of type theory.
Agda uses setoids under the hood.
Martin Hoffman
Reasoning strict proposition
2000’s Thorsten LICS paper on this
Joint Paper with Thorsten - Connor McBride
- Can compare things of different types
- Observational Type Theory = Setoid Type Theory
- Epigram