$\textsf{isStable}(A)\rightarrow\textsf{isProp}(A)$?

Question

I meet both $\neg\neg$-stable and proof-irrelevant types in Harper's handouts on homotopy type theory. I know clearly that proof irrelevance does not imply stability, but does stability imply proof irrelevance? Here is a description of my question:

A type $A$ is said to be $\neg\neg$-stable iff

$$\textsf{isStable}(A):=\neg\neg A\rightarrow A.$$

A type $A$ is said to be proof-irrelevant iff

$$\textsf{isProp}(A):=(\forall x,y:A)(x=_Ay).$$

Then can we prove the following formula?

$$\textsf{isStable}(A)\rightarrow \textsf{isProp}(A).$$

Answer 1

The formula is provably false. $\mathsf{Bool}$ is stable (take the constant $\mathsf{true}$ or $\mathsf{false}$ function for proof) and it's not a proposition, since $\mathsf{true} \neq \mathsf{false}$.