`{Univalence} (O : Subuniverse) {Y F : pType} `{inO : In O F} : (Y ->* [Type_ O, (pointed_type F; inO)]) <~> { p : { q : pSlice Y & MapIn O q.2 } & pfiber p.1.2 <~>* F }. Proof. refine (_ oE equiv_sigma_fibration_Op). refine (_ oE equiv_sigma_symm' _ (fun q => hfiber q.2 (point Y) <~> F)). refine (equiv_sigma_symm' (fun q => pfiber q.2 <~>* F) _ oE _). by rapply (equiv_functor_sigma' equiv_pfiber_fibration_pfibration). Defined.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.