0
$\begingroup$

The Observational Equality from Epigram 2 seems to be intensional equality (like Coq and Agda have), but it also supports function extensionality. In that sense it seems that Observational Equality is better in every way than intensional equality in a type theory.

Is it true that it's always better to have Observational Equality instead of just intensional equality, or are there other trade-offs involved?

Improve this question
$\endgroup$
4
  • $\begingroup$ I cannot resist but to counter with "define better". Seriously, better with respect to what? $\endgroup$
    – Andrej Bauer
    Jun 19 '20 at 15:56
  • $\begingroup$ I admit it is a vague question. Better in the sense that you can prove the same things as with an intensional equality, but also you get function extensionality. So better in the sense that if you could add an intensional equality to your language then you could add observational equality instead and get function extensionality. $\endgroup$
    – Labbekak
    Jun 19 '20 at 18:20
  • $\begingroup$ What is Epigram 2? Please define your terms. $\endgroup$
    – reinierpost
    Jun 20 '20 at 11:45
  • $\begingroup$ It's a programming language by McBride and McKinna (and probably others). Development was stalled. There was a lovely talk by McBride in Andrej Bauer's organized talks on proof assistants. $\endgroup$
    – Labbekak
    Jun 21 '20 at 12:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.