Name for this map of power sets associated with a function? Given a function $f: X \to Y$, there are two associated maps of power sets:  the direct image $f^{\to}: \mathcal{P}(X) \to \mathcal{P}(Y)$ and the inverse image $f^{\leftarrow}: \mathcal{P}(Y) \to \mathcal{P}(X)$.
Consider the map
$$
f^?: \mathcal{P}(X) \to \mathcal{P}(Y)
$$
defined by
$$
f^?(A) = \{y \in Y: f^\leftarrow(\{y\}) \subset A\}
$$
In words, $f^?(A)$ is the set of all $y \in Y$ so that every $x$ which maps to $y$ is in $A$.
Does this map have a standard name and notation?
Note:  I became interested in this while reading this nCategory Cafe post.  Knowing the context is not needed to answer the question, but $f^?$ is associated with universal quantification in the sense of the post.
 A: (Adapted from an email I sent the OP, who was also asking about connections with "the six operations" of Grothendieck.)
I guess it might depend which community you're talking to. I believe the notation $\exists_f$ (for direct image along $f$) and $\forall_f$ notation (for the thing OP is asking about) is somewhat standard for those working in topos theory and categorical logic. For example, you see both notations in Mac Lane-Moerdijk, Sheaves in Geometry and Logic, Proposition IV.9.3 and just before. In the same place you will see the parallel notation for functors between slice toposes, $\Sigma_f: E/X \to E/Y$ and $\Pi_f: E/X \to E/Y$.
(These notations make sense when you consider that
$$f^\to(A) = \exists_f(A) = \{y \in Y: \exists_{x \in X}\; y = f(x) \wedge x \in A\}$$
$$f^?(A) = \forall_f(A) = \{y \in Y: \forall_{x \in X}\; y = f(x) \Rightarrow x \in A\}$$
These notations may have begun with Lawvere, who uses it e.g. in his 1970 paper Quantifiers and Sheaves.)
For some reason, $\forall_f$ seems to be the "weak sister", much less well-known than her brother the direct image along $f$. I am not aware of any standard name or notation for it in the traditional logical literature. And yet, it plays a role here and there. For example, if X is a compact space with a countable base $B$ and $f: X \to Y$ is a continuous surjection to a Hausdorff space, then $Y$ also has a countable base; the most natural choice for that base is $\{\forall_f(U): U \in B\}$. Another example: it's more direct to prove that if $X$ is compact and $Y$ is a space, and $p: X \times Y \to Y$ is projection, then the operator $\forall_p$ takes open sets to open sets, than it is to prove that the direct image $\exists_p$ takes closed sets to closed sets (which is the De Morgan dual statement).
In representation theory, the corresponding operations are induction and coinduction (of a $G$-representation along a group homomorphism $f: G \to H$) that are left and right adjoint to the restriction functor along $f$. These can also be described by (enriched) Kan extensions. So $Res_f$ would be like pullback $f^\ast = f^\leftarrow$, $Ind_f$ would be like $\exists_f$, and $Coind_f$ would be like $\forall_f$.
Yes, morally this is related to "the six operations" although I don't know much about that either. In particular, what I know as "Frobenius reciprocity", whose logical form is $\exists_f(S) \wedge T = \exists_f(S \wedge f^\ast(T)$), is formally like the projection formula in algebraic geometry (and there's a similar-looking one for Chow rings). The name "Frobenius reciprocity" here was introduced by Lawvere (naturally), borrowing from terminology of representation theorists, who often refer just to the adjunction $Ind_f \dashv Res_f$ as "Frobenius reciprocity", but who sometimes include as part of this the analogous isomorphism
$$Ind_f(V) \otimes W \cong Ind_f(V \otimes Res_f(W)).$$
In the language of hyperdoctrines, these reciprocity isomorphisms arise from the fact that pulling back or restriction along $f$ preserves the internal hom (see again Mac Lane & Moerdijk, IV.9, although they don't mention the word "hyperdoctrine").
Sorry that I don't have a better answer to your question!
