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