{A:Type} (R : Relation A) : Type := {_ : Reflexive R | { _ : Symmetric R | Transitive R}}. Global Instance trunc_sig_equiv_rel `{Funext} {A : Type} (R : Relation A) {n} `{!forall (x y : A), IsTrunc n (R x y)} : IsTrunc n ( R). Proof. apply @istrunc_sigma. - apply istrunc_forall. - intros. apply @istrunc_sigma; intros; apply istrunc_forall. Defined.