fact: Definition equiv_path_O {X : Type@{i}} (x y : X) : O (x = y) <~> (to O X x = to O X y) := equiv_path_OO O O x y.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated