Definition isapropisdecprop (X : UU) : isaprop (isdecprop X). Proof. intros. unfold isdecprop. apply (isofhlevelweqf 1 (weqdirprodcomm _ _)). apply isofhleveltotal2. - apply isapropisaprop. - intro i. apply isapropdec. assumption. Defined.