[Agda] question about a form of irrelevance elimination

[Martin Escardo]

On 14/07/15 15:52, Martin Escardo wrote:
> 
> 
> 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.)

I meant to write "*if* it is consistent" (which may well be).

Martin

> 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