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