Definition decreltobrel {X : UU} (R : decrel X) : brel X. Proof. intros. intros x x'. induction ((pr2 R) x x'). - apply true. - apply false. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.