equiv_sigma_pfibration@{u v +} `{Univalence} {Y F : pType@{u}} : (Y ->* [Type@{u}, F]) <~> { p : pSlice@{u v} Y & pfiber p.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.