Normal term of double negation of W-type Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle.
Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is inhabited. Then $W_{a:A}B(a)$ is inhabited and so $(W_{a:A}B(a)\to 0)\to 0$ is inhabited. As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one term in normal form. What is that term?
As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one
term in normal form.

First, without function extensionality, this type cannot be proven to be propositional. Second, propositional types do not necessarily have unique normal forms. Normal forms are up to $\beta\eta$ rules, not propositional equality.
$0 \to 0$ has infinitely many normal inhabitants. Listing a few:
$$\lambda\,x. x$$
$$\lambda\,x. \text{0-elim}\,x$$
$$\lambda\,x. \text{0-elim}\,(\text{0-elim}\,x)$$
Similarly, for any inhabited $A$, $(A \to 0) \to 0$ has infinitely many normal inhabitants.