Dear Thorsten, Robin,
Now that the discussion has turned to setoids and observational type theory, I
could not help myself from responding. (Thorsten and I had quite some
off-line discussion about this).
I generally agree with Thorsten's description of observational type theory as
internalizin
Hi Robin,
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
