fact: Definition O_functor_pullback {A B C : Type} (f : B -> A) (g : C -> A) : IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)).
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated