fact: Definition equiv_OO_pullback {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).
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization