Definition isdecrellogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isdecrel L) : isdecrel R. Proof. intros. intros x1 x2. induction (isl x1 x2) as [ l | nl ]. - apply (ii1 (pr1 (lg _ _) l)). - apply (ii2 (negf (pr2 (lg _ _)) nl)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.