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