{A B} (f : A -> B) (b : B) : (O_functor_hfiber f b) o to O (hfiber f b) == functor_hfiber (fun u => (to_O_natural f u)^) b. Proof. intros [a p]; unfold O_functor_hfiber, functor_hfiber, functor_sigma; cbn. refine (O_rec_beta _ _ @ _). exact (ap _ (inv_V _ @@ 1))^. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.