[Agda] Postulated computing quotients are unsound

[Benja Fallenstein]

Hi Dominique!

On Wed, May 16, 2012 at 4:27 PM, Dominique Devriese
<dominique.devriese at gmail.com> wrote:
>> * The exported constructors compute to the real ones, also in
>>  equalities. For instance, [ true ] ≡ [ false ] computes to box true ≡
>>  box false.
>
> Out of interest: what would happen if [_] were made abstract?

Then, alas, (elim f proof [ x ]) no longer reduces to (f x), which is
the whole point of the present exercise (you can get non-computing
quotients by simply postulating the quotient type and eliminator)...

Cheers,
- Benja