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