fact: Definition sig_coind `{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).
imports: HoTT.Basics Types.Arrow Types.Paths