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

[Andreas Abel]

On Jul 7, 2010, at 4:34 PM, Vag Vagoff wrote:
> Okay. But it is still unknown how to state "There exist a subset of  
> A that property P holds" (i.e. "there exist a set of primes")

P is that very subset.

On Jul 7, 2010, at 11:19 PM, Rypacek, Ondrej wrote:
>> 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) ?

Because this formalizes only the decidable subsets of A.

Cheers,

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/