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