equiv_pfiber_fibration_pfibration@{u v} {Y F : pType@{u}} : { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F} <~> { p : pSlice@{u v} Y & pfiber p.2 <~>* F }. Proof. equiv_via (sig@{v u} (fun X : Type@{u} => { x : X & { p : X -> Y & { eq : p x = point Y & { e : hfiber p (point Y) <~> F & e^-1 (point F) = (x; eq) } } } })). - refine (_ oE _). + do 5 (rapply equiv_functor_sigma_id; intro). apply equiv_path_sigma. + cbn; make_equiv_contr_basedpaths. - refine (_ oE _). 2: { do 5 (rapply equiv_functor_sigma_id; intro). exact (equiv_path_inverse _ _ oE equiv_moveL_equiv_M _ _). } make_equiv. Defined.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.