proposition: Lemma uparam_induction `{Univalence} A (P : forall B, uparam A B -> Type) : P A id_uparam -> forall B f, P B f.
proof: Proof. move=> PA1 B f; rewrite -[f]/(B; f).2 -[B]/(B; f).1. suff : (A; id_uparam) = (B; f). { elim. done. } apply: path_ishprop; apply: hprop_inhabited_contr => _. apply: (contr_equiv' {x : _ & A = x}). apply: equiv_functor_sigma_id => {f}B. symmetry; apply: equiv_compose' uparam_equiv. exact: equiv_path_universe. Defined.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions