fact: Fixpoint nSep (n : trunc_index) (O : Subuniverse) : Subuniverse := match n with | -2 => O | n.+1 => Sep (nSep n O) end.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated