(P : forall U V, U <~> V -> Type) (didmap : forall T, P T T (equiv_idmap T)) (U : Type) : equiv_induction' P didmap U U (equiv_idmap U) = didmap U := (equiv_ind_comp (P U U) _ 1).
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.