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 equivalence relation". 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. -- Robin
