[Agda] Abstract existential ?

[Jacques Carette]

Thanks - I was aware that in HoTT/UF, this was just propositional 
truncation. And that in cubical Agda, this should just 'work'. But I am 
trying to get as far as possible with 'vanilla' Agda (without any 
axioms, for funext is out too).  Thanks for reminding me of this paper, 
I did mean to reread it, now that I understand a lot of these issues 
much better than when I first attempted to read it.

I am quite willing to go through the torture of working with Setoids if 
that's what it takes. Has someone worked that out -- i.e. is there are 
library that gives the main infrastructure needed to do propositional 
truncation on Setoids?

Jacques

On 2019-02-06 4:54 p.m., Martin Escardo wrote:
> In HoTT/UF, and in cubical Agda, you can achieve this by considering 
> the propositional truncation of a Sigma type
>
>   ||Sigma(x:X), A x||.
>
> This is constructive in the way you wish. Not always can you have
>
>   ||Sigma(x:X), A x|| -> Sigma(x:X) -> A x,
>
> as you would be able to deduce excluded middle if you could do this 
> for all X:Set and A:X->Set.
>
> However, sometimes you can, e.g. for f:N->N,
>
>   ||Sigma(n:N), f n = 0|| -> Sigma(n:N), f n = 0.
>
> (If such a function has a root, you can find one.)
>
> I emphasize that this is not Markov's principle
>
>   ¬¬(Sigma(n:N), f n = 0) -> Sigma(n:N), f n = 0,
>
> which is *not* provable. (And so ||-|| is not the same thing as ¬¬(-).)
>
> This is discussed in detail in the paper
> "Notions of anonymous existence in Martin-Loef Type Theory"
> https://arxiv.org/abs/1610.03346
> by Kraus, Escardo, Coquand, Altenkirch.
>
> In terms of setoids, you can think of the propositional truncation of 
> a setoid B to be the setoid with the same underlying type, but with 
> the given equivalence relation replaced by the the chaotic, or 
> indiscrete, equivalence relation that relates any two points.
>
> Martin
>
>
> On 06/02/2019 21:30, carette at mcmaster.ca wrote:
>> Is there a way to encode an existential in Agda where the "exists" 
>> part of the dependent pair is abstract/private?  ∃ from the standard 
>> library just says that the first part is implicit (i.e. can be 
>> uniquely inferred).
>>
>> I think I could use the same trick as in Haskell (i.e. use a wrapper 
>> where I don't export the constructor but do provide accessor 
>> functions that don't leak), but that somehow seems heavy.  Is there 
>> something simpler?
>>
>> I don't mean a fully non-constructive exists here: I mean 
>> (informally!) "a dependent pair where the first projection is 
>> abstract and cannot leak". So to build such a thing, a definite type 
>> must be used, but once it is created, the 'clients' as it were, 
>> cannot find out what that type is.
>>
>> Jacques
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>