(O : Subuniverse) {A B : Type} (i : A -> B) `{IsEmbedding i} `{In (Sep O) B} : In (Sep O) A. Proof. intros x y. refine (inO_equiv_inO' _ (equiv_ap_isembedding i x y)^-1). Defined.
Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath. Require Import HFiber Extensions Factorization Limits.Pullback. Require Import Modality Accessible Descent. Require Import Truncations.Core. Require Import Homotopy.Suspension.