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