(n : trunc_index) (O : Subuniverse) : Subuniverse := match n with | -2 => O | n.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.