Definition breltodecrel {X : UU} (B : brel X) : decrel X := @make_decrel _ (λ x x', make_hProp ((B x x') = true) (isasetbool _ _)) (λ x x', (isdeceqbool _ _)).
Require Import UniMath.Foundations.UnivalenceAxiom.