Definition isrefllogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isrefl L) : isrefl R. Proof. intros. intro x. apply (pr1 (lg _ _) (isl x)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.