{A B C : Type} (f : B -> A) (g : C -> A) : O (Pullback f g) <~> O (Pullback (O_functor O' f) (O_functor O' g)) := Build_Equiv _ _ _ (OO_inverts_functor_pullback_to_O f g).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.