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

[Thorsten Altenkirch]

On 9 Jul 2010, at 16:59, Rypacek, Ondrej wrote:

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

Why do you need this?

Unlike powerset quotients are predicatively acceptable, btw.

Cheers,
Thorsten

>
> Cheers, Ondrej_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda