{A B} (f : A -> B) (b : B) : O (hfiber f b) <~> hfiber (O_functor O f) (to O B b) := Build_Equiv _ _ (O_functor_hfiber O f b) _.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.