Definition iseqrellogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iseqrel L) : iseqrel R. Proof. intros. apply (make_dirprod (ispologeqf lg (pr1 isl)) (issymmlogeqf lg (pr2 isl))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.