Propositional canonicity for natural numbers under intuitionistic LLPO

Let $\a0\mathbf{LLPO}_\vee$ denote the version of LLPO using propositional truncation, and let $(x:\mathbf{LLPO}_\vee)$ be the corresponding context in a type theory with bracket types. The context has propositional canonicity for $\mathbb{N}$ when every term $t:\mathbb{N}$ in the context is propositionally equal to a numeral: there are $n\in\mathbb{N}$ and a term $p$ such that $p:\operatorname{Id}_{\mathbb{N}}(t,\underline{n})$.

Propositional-canonicity conjecture. The context $(x:\mathbf{LLPO}_\vee)$ has propositional canonicity for $\mathbb{N}$ over type theory with bracket types, as studied by Awodey and Bauer, or over similar systems studied by Maietti.

The preceding theorem shows that the analogous context $(x:\mathbf{LLPO}_+)$ does not have propositional canonicity for $\mathbb{N}$ in any consistent theory of the specified computably enumerable kind. This conjecture predicts that propositional truncation changes the situation for bracket-type theories, but the source gives no proof or resolution.