fact: Definition equiv_sigma_pfibration@{u v +} `{Univalence} {Y F : pType@{u}} : (Y ->* [Type@{u}, F]) <~> { p : pSlice@{u v} Y & pfiber p.2 <~>* F} := equiv_pfiber_fibration_pfibration oE equiv_sigma_fibration_p.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations