Definition deceq_to_decrel {X:UU} : isdeceq X -> decrel X. Proof. intros i. use make_decrel. - intros x y. exists (x=y). apply isasetifdeceq. assumption. - exact i. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.