[Agda] Postulating double-negated consistent axioms without breaking canonicity?

[Nils Anders Danielsson]

On 2011-05-26 11:19, Andreas Abel wrote:
> If you say that if all your axioms are negative, consistency implies
> canonicity, I would find that plausible.  Your axiom "em" still looks
> ugly to me.

Why? If I understood you correctly, then your irrelevant projections
correspond to postulates without computational meaning. Do you consider
this feature to be ugly as well?

> As a research project, I suggest to try and add a classical,
> impredicative, proof-irrelevant universe Prop to Agda.  Maybe that would
> allow you to do your stuff?

The axiom Ulf suggested is apparently inconsistent in the presence of
impredicativity, so I guess not. Furthermore I would postulate a
universe-polymorphic version of the axiom.

-- 
/NAD