[Agda] How to formalize 'there exists a set' phrase?

[Benja Fallenstein]

Hi Vag,

On Wed, Jul 7, 2010 at 4:34 PM, Vag Vagoff <vag.vagoff at gmail.com> wrote:
>> data ∃ (P : Set → Set) : Set₁ where
>> _,_ : (A : Set) → P A → ∃ P
>
> Okay. But it is still unknown how to state "There exist a subset of A that
> property P holds" (i.e. "there exist a set of primes")

Subsets of A can be interpreted as functions A → Set:

data ∃ (A : Set) (P : (A → Set) → Set) : Set₁ where
    _,_ : (S : A → Set) → P S → ∃ P

(Of course, this does not guarantee that P depends only on whether (S
x) is inhabited; you could have P = \x. S x == Nat. But that's just
the general situation of Agda not having quotient types -- if you
model real numbers as Cauchy series, you also need to take care to use
only predicates that don't depend on the particular Cauchy series
you're using.)

All the best,
- Benja