equiv_sigma_fibration_Op_connected@{u v +} `{Univalence} {O : Subuniverse} {Y : pType@{u}} `{IsConnected 0 Y} {F : Type@{u}} `{inO : In O F} : (Y ->* [Type_ O, (F; inO)]) <~> { p : Slice@{u v} Y & hfiber p.2 (point Y) <~> F }. Proof. refine (_ oE equiv_sigma_fibration_Op). refine (_ oE (equiv_sigma_assoc' _ (fun p _ => hfiber p.2 (point Y) <~> F))^-1%equiv). srapply equiv_functor_sigma_id; intro; cbn. refine (_ oE equiv_sigma_symm0 _ _). apply equiv_sigma_contr; intro e. rapply contr_inhabited_hprop. rapply conn_point_elim. apply (inO_equiv_inO F e^-1). Defined.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.