fact: Definition equiv_induction_comp {U : Type} (P : forall V, U <~> V -> Type) (didmap : P U (equiv_idmap U)) : equiv_induction P didmap U (equiv_idmap U) = didmap := (equiv_ind_comp (P U) _ 1).
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod