Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Thorsten Altenkirch
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

Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Bas Spitters
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