fact: Definition equiv_sigma_fibration `{Univalence} {Y : Type@{u}} : (Y -> Type@{u}) <~> { X : Type@{u} & X -> Y } := Build_Equiv _ _ _ isequiv_sigma_fibration.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations