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?