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

[Nils Anders Danielsson]

On 2010-07-06 18:00, Vag Vagoff wrote:
> It is well known how to formalize in constructive math statement "there
> is exist an element x of A with property P":
>
> data Ex {A : Set} (P : A -> Set) : Set where ex : {a : A} -> P a -> Ex P
>
> But how to formalize statement "there is exist a set A with property P"?

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

--
/NAD