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).


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₁
  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))


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


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∞)
  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