fact: Definition O_cover@{u} `{O : ReflectiveSubuniverse@{u}} (X : Type@{u}) (x : O X) : Type@{u} := hfiber (to O _) x.
imports: Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed Modalities.ReflectiveSubuniverse