proposition: Lemma uparam_equiv `{Univalence} {A B : Type} : uparam A B <~> (A <~> B).
proof: Proof. apply (equiv_compose' equiv_sig_relequiv^-1). unshelve eapply equiv_adjointify. - move=> [R mR msR]; exists R; exact: map_graph_equiv_isfun. - move=> [R mR msR]; exists R; exact: (map_graph_equiv_isfun _)^-1%equiv. - by move=> [R mR msR]; rewrite !equiv_invK. - by move=> [R mR msR]; rewrite !equiv_funK. Defined.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions