[Agda] question about a form of irrelevance elimination

[Andrew Pitts]

On 14 July 2015 at 13:46, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> I am a bit nervous about the computational consistency of this
> postulate. I think this may imply excluded middle (but I am not sure).

If true, that would be annoying, but interesting.

Thanks to all who posted replies to my question. Let me try to explain
why I asked the original question.

Stimulated by some work of one of my Masters students (see
<http://www.cl.cam.ac.uk/~amp12/index.html#choudhury>), I have been
thinking about an Agda development of nominal set theory which starts
with a decidable type of atoms that is infinite in the sense that for
every list of atoms there merely exists an atom not in the list. So I
need to use propositional reflection. I can hack that into Agda
following Dan Licata and Guillaume Brunerie's tricks in Agda-HoTT. But
as far as I know that forces me to construct proofs about
propositional reflection using its eliminator, which is tedious.
Whereas proofs using irrelevant truncation can make use of
pattern-matching and are rather nice. However, the theory of nominal
sets (when it comes to the Freshness Theorem and properties of name
abstraction) require unique-choice: if for every x : A I know there
merely exists a unique y : B with some property, I need to be able to
extract a function A -> B witnessing that. I can't see how one can do
that for  irrelevant truncation without extra postulates. Am I wrong?

Andy