Solution (source code)

= Solution

The two <adjoints of inverse image on power sets> are
$$
\boxed{\exists_p(U)=p(U),\qquad\forall_p(U)=\{b\in B:p^{-1}(\{b\})\subseteq U\}.}
$$
These maps and $p^*(V)=p^{-1}(V)$ are <monotone functions> on the inclusion-ordered <power sets>. For $U\subseteq A$ and $V\subseteq B$,
$$
p(U)\subseteq V\iff U\subseteq p^{-1}(V),\qquad p^{-1}(V)\subseteq U\iff V\subseteq\forall_p(U).
$$
The first equivalence follows by following each element of $U$ through $p$. For the second, every <fiber> over $b\in V$ must lie in $U$, which is precisely the defining condition for $b\in\forall_p(U)$. These are the two <Galois connections>, proving $\exists_p\dashv p^*\dashv\forall_p$. In particular, a point outside $p(A)$ has an empty <fiber> and belongs to $\forall_p(U)$ even when $U$ is empty; omitting this case would give an incorrect <right adjoint>.