[Agda] question about a form of irrelevance elimination

[Martin Escardo]

On 14/07/15 14:11, Andrew Pitts wrote:
> 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.

I take this back: I was thinking you also had the computation rule for
elimination, but you don't. (Hence in this version of truncation (it is
consistent) the trick to get function extensionality doesn't work.)
If you did, you would conclude, with your postulate, that the elements
of any proposition would be definitionally equal.

Moreover, considering the proposition Sigma(y:X).x=y for any given x:X,
you would get equality reflection (from p:x=y you get that x and y are
definitionally equal.

But here you (1) give up the computation rule for truncation, and (2)
you declare that all elements of the truncation are definitionally
equal. This sounds very strange, but I can't see any contradiction or
taboo. However, the situation in which you don't give up (1) and insist
on (2) would seem suspicious to me (I assumed that when I read your
message).

Another remark is that from your


postulate
  !elim : {ℓ : Level}{A : Set ℓ}.(_ : isProp A) → (! A) → A

you get the usual elimination rule for truncations, of type


  {ℓ : Level}{X A : Set ℓ}.(_ : isProp A) → (X → A) → (! X) → A

Conversely this implies yours postulate.

Martin

> 
> 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
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe