`{Univalence} {O : Subuniverse} {Y : pType@{u}} `{IsConnected 0 Y} {F : Type@{u}} `{inO : In O F} : (Y ->* [Type_ O, (F; inO)]) <~> (Y ->* [Type@{u}, F]) := equiv_sigma_fibration_p^-1 oE equiv_sigma_fibration_Op_connected.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.