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

[Rypacek, Ondrej]

On Jul 7, 2010, at 11:19 PM, Rypacek, Ondrej wrote:
>> Subsets of A can be interpreted as functions A → Set:

But A -> Set doesn't fit into Set , for A : Set . It is an ZF axiom . 
Or is this one inconsistent intuitionistically ? 
Or perhaps that's where quotients would help to make things precise and fit the powerset of A : Set a into Set ?

Cheers, Ondrej