(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).
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.