The type ℕ∞ has decidable equality iff WLPO holds

[jkingdon]

This is mentioned as background knowledge at https://mathstodon.xyz/@MartinEscardo/113001536506411322 but I don't see it proved in iset.mm, or an issue for it.

In iset.mm notation this would be

A. x e. NN+oo A. y e. NN+oo DECID x = y <-> _om e. WOmni

[benjub]

/!\ Spoiler alert below the dots /!\

...

...

...

Forward implication:
Given a proposition $f \colon \omega \to 2$, define $g \in \mathbb{N}_\infty$ by $g(n) \coloneqq \min ( f(i) \mid i \leq n)$.
Then, $g$ is the point at infinity iff $\forall n \in \omega f(n)=1$.

Backward implication:
Decidability of equality with the point at infinity follows from the fact that $\mathbb{N}_\infty \subseteq \Omega$, and decidability of equality in $\mathbb{N}$ has been proved.