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

[Ondrej Rypacek]

2010/7/12 Thorsten Altenkirch <txa at cs.nott.ac.uk>:
>
> 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?

Given a relation between sets I and J  of the form

I <- B -> A -> J

I need an opposite, but not

J <- A <- B -> I

but something of the same shape, i.e. something like

J <- A -> p B -> p I

where, p is the powerset functor Set -> Set and the middle arrow is
the inverse of the one above.

But if p has type : Set l -> Set (suc l), this and everything else
would have to be universe polymorphic, I guess. Not sure how it will
work with the rest of my development, but probably fine. Just makes it
more complicated.


>
> Unlike powerset quotients are predicatively acceptable, btw.
Do you mean that cardinality is not size? Hank has pointed this out to
me. It was just a wild guess, really.


Cheers,
Ondrej

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