proposition: Lemma isdecproppaths {X : UU} (is : isdeceq X) (x x' : X) : isdecprop (x = x').
proof: Proof. intros. apply (isdecpropif _ (isasetifdeceq _ is x x') (is x x')). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom