[Agda] Abstract existential ?

[Martin Escardo]

On 06/02/2019 22:06, carette at mcmaster.ca wrote:
> 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?

I don't know. But the cubical model can be thought of as a 
generalization of the setoid model (with a more intense level torture?), 
and cubical type theory / Agda can be thought of as such as library for 
the cubical model, where everything automatically preserves the 
generalized equivalence relations (that is, the cubical structure).

Regarding setoids themselves, the problem is that things become unclear 
when one considers universes (the types Set i in Agda), in particular 
when you consider things such as the type of all groups in a given 
universe. The cubical model / type theory is much better suited for 
that. (And more generally HoTT/UF, which is what cubical type theory was 
designed to give computational content to.)

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

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