fact: Definition equiv_sig_ind' `{P : A -> Type} (Q : forall a, P a -> Type) : (forall (x:A) (y:P x), Q x y) <~> (forall xy, Q xy.1 xy.2) := equiv_sig_ind (fun xy => Q xy.1 xy.2).
imports: HoTT.Basics Types.Arrow Types.Paths