fact: Definition equiv_path_OO `{O' <= Sep O} {X : Type@{i}} (x y : X) : O (x = y) <~> (to O' X x = to O' X y) := Build_Equiv _ _ (path_OO x y) _.
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization