equiv_sigma_fibration_p@{u v +} `{Univalence} {Y : pType@{u}} {F : Type@{u}} : (Y ->* [Type@{u}, F]) <~> { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F }. Proof. refine (_ oE (issig_pmap _ _)^-1). srapply (equiv_functor_sigma' equiv_sigma_fibration); intro P; cbn. refine (_ oE (equiv_path_universe@{u u v} _ _)^-1%equiv). refine (equiv_functor_equiv _ equiv_idmap). apply hfiber_fibration. Defined.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.