{O : Modality} {A : Type} `{In O A} (P : A -> Type) : {x:A & O (P x)} <~> O {x:A & P x}. Proof. transitivity (O {x:A & O (P x)}). - rapply equiv_to_O. - apply equiv_O_sigma_O. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.