Intuition for Exists and Forall functors This question gives a concise definition of the exists and forall functors, in the form invented (I gather) by Lawvere.
Quoting:

Let $f:X\rightarrow Y$ be an arrow in $\mathsf{Set}$. $f$ induces
three functors: $$\exists (f),\forall (f):\mathcal P(X)\rightarrow
> \mathcal P(Y),\; \mathsf I(f):\mathcal P(Y)\rightarrow \mathcal P(X)$$
where the powerset is a poset category. The action on objects is given
by $$\exists (f)(A)=f[A],\; \mathsf I(f)(B)=f^\leftarrow (B),\;
> \forall (f)(A)=f[A^c]^c.$$ and one can prove $$\exists (f)\dashv
> \mathsf I(f) \dashv \forall (f).$$ In particular, the inverse image
functor is right adjoint to the direct image functor.

I've been trying to get an intuitive grasp of this, in the simplest possible terms. What I have so far is the idea of "ingredients" and "recipes". X is the set of ingredients, Y of recipes.
Now, it seems to me that this is making some sense. The exists functor takes a set of ingredients and gives us the set of all recipes for which we have at least one of the ingredients. The forall functor takes a set of ingredients and gives us the set of recipes for which we have all the ingredients.
It seems like it is necessary to work with the category of sets and relations rather than sets and functions (since ingredients can appear in more than one recipe). But maybe this doesn't invalidate the basic analogy—I hope it translates in a straightforward way.
I first came across this adjunction on the Wikipedia page for universal quantification. The exposition there is not great and apparently originated from a section on Wikipedia's power set page. So it would be great to get any thoughts on the validity or otherwise of my example.
 A: It is useful to try to visualize things like you do. I'll try to help even if your interrogation is not very precise. You can think of a function $f : X→Y$ as an $Y$-indexed family of sets $(f^{-1}(y))_{y∈Y}$ and then what you say about ingredients and recipes is right, even if it's a bit confusing because as you say, an ingredient can be used in multiple recipes. Given $U ⊆ X$, we have $y ∈ ∃(f)(U)$ if there is some $x ∈ f^{-1}(y)$ with $x ∈ U$. And $y ∈ ∀(f)(U)$ if for all $x ∈ f^{-1}(y)$ we have $x ∈ U$.
A special case that could help is the following. Take the projection $p : X×Y → Y$. A subset $U ⊆ X×Y$ is a proposition $φ(x,y)$ of two variables $x ∈ X$ and $y ∈ Y$. Then the image of $U$ by $∃(p)$ is given by the formula $∃x:φ(x,y)$. When we take an arbitrary function instead of such a projection, we allow the possible values for $x$ to depend on $y$ (the fibers $f^{-1}(y)$ are not constant).
For instance, take the two propositions "Mayor $y$ is liked by everybody in their town" and "Mayor $y$ is liked by somebody in their town". We would want to formalize the first proposition as $∀x:φ(x,y)$ and the second one as $∃x:φ(x,y)$, with $φ$ the "likes" relation. But then the range of $x$ has to depend on $y$: it is the set of persons in the town of mayor $y$. If $x$ ranges over all the people in every town, we have to chose how to define $φ(x,y)$ for $x$ not in the town of Mayor $y$. If we say it is "false", then $∀x:φ(x,y)$ becomes always false. If we say it is "true", then $∃x:φ(x,y)$ becomes always true. In this situation, we need the range of $x$ to depend on $y$: the function $f : \text{People} → \text{Mayors}$ sends a person to the Mayor of their town. Then $f^{-1}(y)$ is the set of people in the town of Mayor $y$.
If you want, Lawvere wrote a book called "conceptual mathematics". I don't know if he explains quantifiers in it, but you might find this book interesting.
If you want to generalize this to relations instead of functions, it works a bit differently (even if it is a generalization). Let $R ⊆ X×Y$ be a relation. For a subset $U ⊆ X$, let $∃_R(U) = \{y∈Y\,|\,∃x∈X:R(x,y)∧x∈U\}$ and let $∀_R(U) = \{y∈Y\,|\,∀x∈X:R(x,y)⇒x∈U\}$. Let $R' ⊆ Y×X$ be the transpose of $R$. Then $∃_R : \mathcal{P}(X) → \mathcal{P}(Y)$ is left adjoint to $∀_{R'} : \mathcal{P}(Y) → \mathcal{P}(X)$. So in this context, "existential quantification is left adjoint to universal quantification".
