Thanks to all who replied.
I have another couple of questions, more fundamental this time.
The paper says "Observational reasoning can be simulated in Intensional
Type Theory by the use of setoids, i.e. types with an explicit
I'm not clear on what the differences are between OTT and simulating
observational reasoning with setoids in ITT. Clearly OTT has an
explicit equivalence relation (=) which is "polymorphic" over (certain)
types. So does the paper mean "explicit" in some other sense?
And doesn't OTT have the same problems (equality not automatically
substitutive, complications in formalising category theory, lots of
explicit coercions) that the paper says ITT has? I don't see how OTT
helps with any of those problems, but the way that OTT is contrasted
with ITT suggests that it should. I must be misunderstanding something.