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