Martin Escardo 2012.

The following says that a particular kind of discontinuity for
functions p : ℕ∞ → ₂ is a taboo. Equivalently, it says that the
convergence of the constant sequence ₀ to the number ₁ in the type
of binary numbers is a taboo. A Brouwerian continuity axiom is
that any convergent sequence in the type ₂ of binary numbers must
be eventually constant (which we don't postulate).

\begin{code}

module BasicDiscontinuityTaboo where

open import GenericConvergentSequence
open import WLPO
open import Two
open import CurryHoward
open import Equality
open import SetsAndFunctions

basic-discontinuity : (ℕ∞ → ₂) → Prp
basic-discontinuity p = (∀ n → p(under n) ≡ ₀) ∧ p ∞ ≡ ₁

basic-discontinuity-taboo :

∀(p : ℕ∞ → ₂) → basic-discontinuity p → WLPO

basic-discontinuity-taboo p (f , r) u =
two-equality-cases lemma₀ lemma₁
where
fact₀ : u ≡ ∞ → p u ≡ ₁
fact₀ t = trans (cong p t) r

fact₁ : p u ≠ ₁ → u ≠ ∞
fact₁ = contra-positive fact₀

fact₂ : p u ≡ ₀ → u ≠ ∞
fact₂ = fact₁ ∘ Lemma[b≡₀→b≠₁]

lemma₀ : p u ≡ ₀ → u ≡ ∞ ∨ u ≠ ∞
lemma₀ s = in₁(fact₂ s)

fact₃ : p u ≡ ₁ → (∀ n → u ≠ under n)
fact₃ t n s =
zero-is-not-one(Lemma[x≡y→x≡z→y≡z](f n)(Lemma[x≡y→x≡z→y≡z](cong p s) t))

lemma₁ : p u ≡ ₁ → u ≡ ∞ ∨ u ≠ ∞
lemma₁ t = in₀(not-ℕ-is-∞ (fact₃ t))

\end{code}

If two ₂-valued functions defined on ℕ∞ agree at ℕ, they have to agree
at ∞ too, unless WLPO holds:

\begin{code}

disagreement-taboo :

∀(p q : ℕ∞ → ₂) → (∀ n → p(under n) ≡ q(under n)) → p ∞ ≠ q ∞ → WLPO

disagreement-taboo p q f g = basic-discontinuity-taboo r (r-lemma , r-lemma∞)
where
r : ℕ∞ → ₂
r u = (p u) ⊕ (q u)

r-lemma : ∀ n → r(under n) ≡ ₀
r-lemma n = Lemma[b≡c→b⊕c≡₀](f n)

r-lemma∞ : r ∞ ≡ ₁
r-lemma∞ = Lemma[b≠c→b⊕c≡₁] g

\end{code}