# [ilmath]\exists[/ilmath]-functor

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:
Requires fleshing out

## Definition

The [ilmath]\exists[/ilmath]-functor is a covariant functor taking [ilmath]\mathrm{SET} [/ilmath] [ilmath]\leadsto[/ilmath] [ilmath]\mathrm{SET} [/ilmath] defined as follows[1]:

• [ilmath]\forall A\in\text{Ob}(\mathrm{SET})[\exists:A\mapsto\mathcal{P}(A)][/ilmath], recall [ilmath]\mathcal{P}(X)[/ilmath] denotes the power set of [ilmath]X[/ilmath]
• The functor sends all objects to their powerset. and
• [ilmath]\forall (f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})\left[\exists(f)\mapsto\left\{\begin{array}{l}:\mathcal{P}(A)\rightarrow\mathcal{P}(B)\\:X\mapsto f(X)\end{array}\right.\right][/ilmath]
• That is to say the [ilmath]\exists[/ilmath]-functor takes the function [ilmath]f[/ilmath] to a function that takes each element of the powerset of the domain of [ilmath]f[/ilmath] to the image of that element under [ilmath]f[/ilmath] (which is obviously in the powerset of the co-domain of [ilmath]f[/ilmath])

### Proof of claim

Claim: that the [ilmath]\exists[/ilmath]-functor is a functor

This page requires one or more proofs to be filled in, it is on a to-do list for being expanded with them.
Please note that this does not mean the content is unreliable. Unless there are any caveats mentioned below the statement comes from a reliable source. As always, Warnings and limitations will be clearly shown and possibly highlighted if very important (see template:Caution et al).
The message provided is:
See page 82 in[1]

## Properties

Notice that the [ilmath]\exists[/ilmath]-functor has the following property:

• Given a [ilmath](f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})[/ilmath]
• [ilmath]\forall X\in\mathcal{P}(A)\ \forall b\in B\Big[ [b\in(\exists(f))(X)]\iff[\exists a\in A(b=f(a)\wedge a\in X)]\Big][/ilmath]

TODO: Describe this, something like [ilmath]b[/ilmath] is in the image of [ilmath]X[/ilmath] under the image of [ilmath]f[/ilmath] in the functor if and only if there is an [ilmath]a\in X[/ilmath] such that [ilmath]f(a)=b[/ilmath]