{Y X : Type@{i} } (f : Y -> X) (x : X) : O (hfiber f x) <~> O (hfiber (O_functor O' f) (to O' X x)) := Build_Equiv _ _ _ (OO_inverts_functor_hfiber_to_O f x).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.