Given a model of set theory $V$ there are various ways to construct a model in which the Axiom of Choice holds, such as Gödel's constructible universe $L(V)$ or by using forcing. I'm wondering if any of these constructions have a nice universal property in the sense of category theory.

In particular are there any adjoints to the inclusion 2-functor $\mathcal{ZFC}\to\mathcal{ZF}$?

(Where $\mathcal{ZF}$ is the 2-category whose objects are either

 1. Models of ZF
 2. Toposes

and whose morphisms are either

 1. Geometric morphisms
 2. Logical functors
 3. Elementary embeddings

and where $\mathcal{ZFC}$ is the full subcategory on the objects that obey Choice.)

I think that the concept of the "[minimal model][1]" might allow one to construct a right adjoint which is similar in character to the constructable universe. Forcing goes "the other way" by adding sets rather than restricting them, so I suspect it might give a left adjoint.

  [1]: https://en.wikipedia.org/wiki/Minimal_model_(set_theory)