{A B C : Type} (f : B -> A) (g : C -> A) : O (Pullback f g) <~> Pullback (O_functor O f) (O_functor O g) := equiv_O_rec_O_inverts O (functor_pullback f g (O_functor O f) (O_functor O g) (to O A) (to O B) (to O C) (to_O_natural O f) (to_O_natural O g)).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.