Normal term of double negation of W-type
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.