proposition: Theorem isapropdec (X : UU) : isaprop X -> isaprop (decidable X).
proof: Proof. intros i. apply isapropcoprod. - exact i. - apply isapropneg. - exact (λ x n, n x). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom