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

[Rypacek, Ondrej]

Hi, 
out of curiosity : 

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

Why not A -> bool ?  Isn't it precisely a subset of A (as the fiber over T, say) ?

Cheers,
Ondrej

> (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.)



_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda