{U : Type} (P : forall V, V <~> U -> Type) (didmap : P U (equiv_idmap U)) : equiv_induction_inv P didmap U (equiv_idmap U) = didmap := (equiv_ind_comp (P U) _ 1). Global Instance contr_basedequiv@{u +} {X : Type@{u}} : Contr {Y : Type@{u} & X <~> Y}. Proof. apply (Build_Contr _ (X; equiv_idmap)). intros [Y f]; revert Y f. exact (equiv_induction _ idpath). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.