{X : Type} (x y : X) : (equiv_path_O x y) o (to O (x = y)) == @ap _ _ (to O X) x y. Proof. intros p; unfold equiv_path_O, equiv_path_OO, path_OO; cbn. apply O_rec_beta. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.