Skip to main content
Inserted a word and a sentence
Source Link

This might not precisely answer your question, but why not use topos theory? The category of (Grothendieck) topoi has as its objects generalized universes of sets whose internal logic does no not necessarily fulfill the axiom of choice or the law of the excluded middle (both of these can be demanded by restricting to a suitable subcategory), but otherwise fulfill the same statements in geometric logic that the category of sets fulfills. Furthermore, forcing can be understood as creating a topos $Y$ as a category of sheaves on a site $J$ over a base topos $X$: $Y:=Sh_X(J)$ (see here for more detailed reasoning), so the operator you want could be understood as a 2-functor which associates to each elementary topos its category of Grothendieck topoi. Finally, the categorical structure you are looking for could be understood as a fibered category with the category of elementary topoi as its base, such that the fiber category over each elementary topos is the category of its Grothendieck topoi. You could try to axiomatize the category of elementary topoi similar to how Lawvere tried to axiomatize the category of sets through ETCS or the category of categories with ETCC, then defining a the category of Grothendieck topoi over any base topos, then seeing how these categories of (relative) Grothendieck topoi are mapped (covariantly or contravariantly) along logical morphisms of elementary topoi.

P.S. I think the truth of regularity should vary if you consider different elementary topoi.

This might not precisely answer your question, why not use topos theory? The category of (Grothendieck) topoi has as its objects generalized universes of sets whose internal logic does no not necessarily fulfill the axiom of choice or the law of the excluded middle (both of these can be demanded by restricting to a suitable subcategory), but otherwise fulfill the same statements in geometric logic that the category of sets fulfills. Furthermore, forcing can be understood as creating a topos $Y$ as a category of sheaves on a site $J$ over a base topos $X$: $Y:=Sh_X(J)$ (see here for more detailed reasoning), so the operator you want could be understood as a 2-functor which associates to each elementary topos its category of Grothendieck topoi. Finally, the categorical structure you are looking for could be understood as a fibered category with the category of elementary topoi as its base, such that the fiber category over each elementary topos is the category of its Grothendieck topoi. You could try to axiomatize the category of elementary topoi similar to how Lawvere tried to axiomatize the category of sets through ETCS or the category of categories with ETCC.

P.S. I think the truth of regularity should vary if you consider different elementary topoi.

This might not precisely answer your question, but why not use topos theory? The category of (Grothendieck) topoi has as its objects generalized universes of sets whose internal logic does no not necessarily fulfill the axiom of choice or the law of the excluded middle (both of these can be demanded by restricting to a suitable subcategory), but otherwise fulfill the same statements in geometric logic that the category of sets fulfills. Furthermore, forcing can be understood as creating a topos $Y$ as a category of sheaves on a site $J$ over a base topos $X$: $Y:=Sh_X(J)$ (see here for more detailed reasoning), so the operator you want could be understood as a 2-functor which associates to each elementary topos its category of Grothendieck topoi. Finally, the categorical structure you are looking for could be understood as a fibered category with the category of elementary topoi as its base, such that the fiber category over each elementary topos is the category of its Grothendieck topoi. You could try to axiomatize the category of elementary topoi similar to how Lawvere tried to axiomatize the category of sets through ETCS or the category of categories with ETCC, then defining a the category of Grothendieck topoi over any base topos, then seeing how these categories of (relative) Grothendieck topoi are mapped (covariantly or contravariantly) along logical morphisms of elementary topoi.

P.S. I think the truth of regularity should vary if you consider different elementary topoi.

Source Link

This might not precisely answer your question, why not use topos theory? The category of (Grothendieck) topoi has as its objects generalized universes of sets whose internal logic does no not necessarily fulfill the axiom of choice or the law of the excluded middle (both of these can be demanded by restricting to a suitable subcategory), but otherwise fulfill the same statements in geometric logic that the category of sets fulfills. Furthermore, forcing can be understood as creating a topos $Y$ as a category of sheaves on a site $J$ over a base topos $X$: $Y:=Sh_X(J)$ (see here for more detailed reasoning), so the operator you want could be understood as a 2-functor which associates to each elementary topos its category of Grothendieck topoi. Finally, the categorical structure you are looking for could be understood as a fibered category with the category of elementary topoi as its base, such that the fiber category over each elementary topos is the category of its Grothendieck topoi. You could try to axiomatize the category of elementary topoi similar to how Lawvere tried to axiomatize the category of sets through ETCS or the category of categories with ETCC.

P.S. I think the truth of regularity should vary if you consider different elementary topoi.