{X Y : Type} {n : trunc_index} `{istr : IsTrunc n.+1 Y} (i : X -> Y) `{isem : IsEmbedding i} : IsTrunc n.+1 X. Proof. apply istrunc_S. exact (@in_SepO_embedding (Tr n) _ _ i isem istr). 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.