fact: Definition IsOProjective (O : Modality) (X : Type) : Type := forall A, In O A -> forall B, In O B -> forall f : X -> B, forall p : A -> B, IsSurjection p -> merely (exists s : X -> A, p o s == f).
imports: Basics Types Truncations.Core Truncations.SeparatedTrunc Modalities.Modality Modalities.Identity Limits.Pullback