{A B : Type} (f : A -> B) `{O_inverts O' f} (x y : A) : O (x = y) <~> O (f x = f y) := Build_Equiv _ _ (O_functor O (ap f)) _.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.