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.