{U : Type} (P : forall V, U <~> V -> Type) : (P U (equiv_idmap U)) -> (forall V (w : U <~> V), P V w). Proof. intros H0 V. apply (equiv_ind (equiv_path U V)). intro p; induction p; exact H0. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.