Another adjoint pair: Definable sets and set-builder formulas I see adjointness between the two concepts of "being  a definable set" and "being a set-builder formula":


A set $X$ is definable when there is a formula $\phi(x)$ such that $X = \lbrace x : \phi(x)\rbrace$.



A formula $\phi(x)$ is a set-builder when there is a set $X$ such that $X = \lbrace x : \phi(x)\rbrace$.


In which (category theoretical) contexts this adjointness is made explicit and valuable?
 A: Your question is not as precise as you portray it, and apart from the question of adjointness, a naive
treatment of definability like this leads easily to
contradictions. Specifically, I claim that your definitions do not
actually succeed in defining the concepts of definability and of
being a set-builder.
To convince you of this, let me prove that the property of a
set-theoretic formula $\varphi$ being a set-builder is not
expressible in the language of set theory.
Specifically, let me prove that no expressible property
$P(\varphi)$ aligns with your concept of being a set-builder.
Consider any property $P(\varphi)$ of formulas that is expressible
in the language of set theory. By the Gödel fixed point
lemma, there is a sentence $\sigma$ such that we can prove the
equivalence $\sigma\iff P(\sigma)$; and we can prove this
equivalence in a very weak system. Note that since $\sigma$ has no
free variables, it follows that $\{ x \mid \sigma\}$ is either the
empty set or everything, depending on whether $\sigma$ is false or
true, respectively. In particular, $\sigma$ is a set builder in your sense just
in case $\sigma$ is false. The point now is that this is
equivalent to saying that $P(\sigma)$ is false. Thus, this
particular formula $\sigma$ is a set-builder if and only if
$P(\sigma)$ fails, and so $P$ gets the wrong answer in this
instance. Since $P$ was arbitrary, there simply is no way to
express the property of a formula that it is a set-builder.
(One could alternatively argue like this: suppose that we could
express the property of being a set-builder. By the fixed-point
lemma, there is a sentence $\sigma$ that is equivalent to
"$\sigma$ is a set-builder". And so $\{x \mid
\sigma\}$ is a set if and only if it isn't.)
Moving to a richer theory or to category theory does not solve the
fundamental problem, since the Gödel fixed point lemma
applies to any sufficiently rich system, including GBC, KM or
ETCS. In these systems, there simply is no way to express the
concept of being a set-builder in that system.
In particular, you haven't actually defined what it means for a
formula to be a set-builder. And similar issues arise with the
concept of being a definable set.
The basic obstacle here, of course, is Tarski's theorem on the
non-definability of truth, which can be thought of as the claim
that we have no definable way to express when a particular
sentence is true. Both of your definitions in effect appeal to
such a predicate, since you are defining a property of $\varphi$,
but then making assertions about the truth of instances of
$\varphi$. Although we may speak of specific formulas being
set-builders or not, there simply is no general concept of a
formula being a set-builder that is expressible in the same
language.
Lastly, and perhaps this will be good enough for you, one can
address part of the problem by working in a stronger system, but
being satisfied with notions of definability and set-builders only
for formulas in a weaker system. For example, in Kelley-Morse set
theory KM, we can define a truth predicate for first-order truth
in the language of set theory. In this case, working in KM we have
robust concepts of definability and set-builders, but only for
formulas in the first-order language of set theory, and not for
formulas in the language of KM.
Another way to address the issues is to work with the notions of
definability and set-builders over a specific set model. If $M$ is
a set model of some theory, then we have notions of
definable-in-$M$ and of a formula $\varphi$ being a
set-builder-in-$M$. This model-theoretic treatment of
definability is used throughout logic. But when using it, one has in effect an outside-the-universe account of the topic, since the notions are not expressible inside the model $M$ being considered. The truly problematic 
issues arise only when one wants to refer to definability in the
whole universe.
These definability issues arose before on MathOverflow, in my
answers to Anixx's question Is analysis in fact the analysis of definable numbers? and to Scott Aaronson's
question Succinctly naming big numbers. In those answers, I show some
examples showing that there are models of set theory with a range
of paradoxical behavior with respect to definability. Most of
those examples appear also in my paper, J. D. Hamkins, D.
Linetsky, J. Reitz, Pointwise definable models of set theory,
JSL 78(1):2013, which includes a relatively accessible account of
some of these metamathematical issues with definability.
A: Given any pair of sets $X, Y$ (let me not be too specific about what "sets" means because what follows is robust with respect to changes in the definition), any relation $R : X \times Y \to 2$ whatsoever induces a contravariant adjunction between the poset of subsets of $X$ and the poset of subsets of $Y$ given by
$$2^X \ni S \mapsto F(S) = \{ y \in Y : xRy \forall x \in S \} \in 2^Y$$
$$2^Y \ni T \mapsto G(T) = \{ x \in X : xRy \forall y \in T \} \in 2^X.$$
A contravariant adjunction between posets is also known as an antitone Galois connection. Any such thing determines two closure operators, one on $2^X$ and one on $2^Y$, and it is often interesting to determine the corresponding closed subsets. Examples:


*

*Let $L/K$ be a Galois extension, let $X = L$, and let $Y = \text{Gal}(L/K)$. The relation is "the element $y \in Y$ fixes the element $x \in X$." The adjunction sends a subset of $L$ to the subgroup of the Galois group fixing it and sends a subset of the Galois group to its fixed field. The fundamental theorem of Galois theory tells us that the closed subsets are the subgroups of the Galois group on the one hand and the subextensions of the Galois extension on the other.

*Let $X = k[x_1, ..., x_n]$ be a polynomial ring over an algebraically closed field and let $Y = \mathbb{A}^n$ be the corresponding affine $n$-space. The relation is "the polynomial $x \in X$ vanishes on the point $y \in Y$." The adjunction sends a set of polynomials to the variety it cuts out and sends a set of points to the ideal of functions vanishing on it. The Nullstellensatz tells us that the closed subsets are the radical ideals on the one hand and the Zariski-closed subsets on the other (the second statement is tautologous; this is the definition of being Zariski closed. But the first one has content).

*Let $X$ be the set of models of a first-order theory $T$ and let $Y$ be the set of possible sentences that could be added to $T$. The relation is "the sentence $y \in Y$ is true in the model $x \in X$." The adjunction sends a set of models to the set of sentences true in every model and sends a set of sentences to the set of models of those sentences (together with $T$). The completeness theorem tells us that the closed subsets are the deductively closed sets of sentences on one hand and whatever their sets of models are on the other.
In your example one of the "sets" is the set of all sets, the other is the set of all formulas, and the relation is "the set $x \in X$ satisfies the formula $y \in Y$." It is a version of the slogan "syntax is adjoint to semantics," an observation first made, as far as I know, by Lawvere. 
A: This is really just an answer stub but it's worth mentioning anyway...
In some way, this is one of the many facets and extensions of Stone Duality. Henrik Forssell's 2008 thesis is one of the latest attempts that I am aware of to formalize this general idea to the fullest.
