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 (or not? See comments). 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" 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.

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" 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.

*Or not? See comments.

**Asaf Karagila notes that there can't exist an elementary embedding between a model where Choice holds and one where it doesn't. So there can't be an adjunction in this case, because its unit or counit would sometimes have to be such a morphism. But perhaps there's some other kind of morphism between models of ZF that does allow an adjunction?

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 (or not? See comments). 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" 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.

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 (or not? See comments). 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" 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.