[Agda] Abstract existential ?

[Martin Escardo]

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