proposition: Lemma equiv_sig_relequiv `{Univalence} {A B : Type@{i}} : (A <~> B) <~> RelEquiv A B.
proof: Proof. apply (equiv_composeR' (issig_equiv _ _)^-1). apply (equiv_compose' issig_relequiv). apply (equiv_compose' (equiv_sigma_assoc' _ _)^-1). unshelve eapply equiv_functor_sigma. - exact: fun_equiv_isfun. - by move=> f; apply: isequiv_isfun. - exact: equiv_isequiv. - by move=> f; apply: equiv_isequiv. Defined.
imports: Coq(ssreflect)