[Agda] Postulated computing quotients are unsound

[Conor McBride]

On 16 May 2012, at 15:15, Nils Anders Danielsson wrote:

> On 2012-05-16 15:50, Altenkirch Thorsten wrote:
>> How can this be fixed? Can we hide things better?
> 
> I don't think we should let hacks like this influence the language
> design too much.

It seems to me that somehow, pattern matching is encoding
some unlicenced elimination behaviour (e.g., injectivity of
the hidden constructor). Epigram takes the eliminators as
primitive and derives....

....oh sorry, I fell asleep.

Cheers

Conor