`{A : X -> Type} (P : forall x, A x -> Type) (f : forall x, A x) (g : forall x, P x (f x)) : (forall x, sig (P x)) := sig_coind_uncurried P (f;g).
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.