BasicDiscontinuity

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


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt

module Taboos.BasicDiscontinuity (fe : funextβ‚€) where

open import CoNaturals.Type

open import MLTT.Plus-Properties
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import Taboos.WLPO

basic-discontinuity : (β„•βˆž β†’ 𝟚) β†’ 𝓀₀ Μ‡
basic-discontinuity p = ((n : β„•) β†’ p (ΞΉ n) ＝ β‚€) Γ— (p ∞ ＝ ₁)

basic-discontinuity-taboo : (p : β„•βˆž β†’ 𝟚)
                          β†’ basic-discontinuity p
                          β†’ WLPO
basic-discontinuity-taboo p (f , r) u = 𝟚-equality-cases lemmaβ‚€ lemma₁
 where
  factβ‚€ : u ＝ ∞ β†’ p u ＝ ₁
  factβ‚€ t = p u ＝⟨ ap p t ⟩
            p ∞ ＝⟨ r ⟩
            ₁   ∎

  fact₁ : p u β‰  ₁ β†’ u β‰  ∞
  fact₁ = contrapositive factβ‚€

  factβ‚‚ : p u ＝ β‚€ β†’ u β‰  ∞
  factβ‚‚ = fact₁ ∘ equal-β‚€-different-from-₁

  lemmaβ‚€ : p u ＝ β‚€ β†’ (u ＝ ∞) + (u β‰  ∞)
  lemmaβ‚€ s = inr (factβ‚‚ s)

  fact₃ : p u ＝ ₁ β†’ ((n : β„•) β†’ u β‰  ΞΉ n)
  fact₃ t n s = zero-is-not-one (β‚€       ＝⟨ (f n)⁻¹ ⟩
                                 p (ι n) ＝⟨ (ap p s)⁻¹ ⟩
                                 p u     ＝⟨ t ⟩
                                 ₁       ∎)

  lemma₁ : p u ＝ ₁ β†’ (u ＝ ∞) + (u β‰  ∞)
  lemma₁ t = inl (not-finite-is-∞ fe (fact₃ t))


The converse also holds. It shows that any proof of WLPO is a
discontinuous function, which we use to build a discontinuous function
of type β„•βˆž β†’ 𝟚.


WLPO-is-discontinuous : WLPO
                      β†’ Ξ£ p κž‰ (β„•βˆž β†’ 𝟚), basic-discontinuity p
WLPO-is-discontinuous f = p , (d , d∞)
 where
  p : β„•βˆž β†’ 𝟚
  p u = equality-cases (f u) caseβ‚€ case₁
   where
    caseβ‚€ : (r : u ＝ ∞) β†’ f u ＝ inl r β†’ 𝟚
    caseβ‚€ r s = ₁

    case₁ : (r : u β‰  ∞) β†’ f u ＝ inr r β†’ 𝟚
    case₁ r s = β‚€

  d : (n : β„•) β†’ p (ΞΉ n) ＝ β‚€
  d n = equality-cases (f (ΞΉ n)) caseβ‚€ case₁
   where
    caseβ‚€ : (r : ΞΉ n ＝ ∞) β†’ f (ΞΉ n) ＝ inl r β†’ p (ΞΉ n) ＝ β‚€
    caseβ‚€ r s = 𝟘-elim (∞-is-not-finite n (r ⁻¹))

    case₁ : (g : ΞΉ n β‰  ∞) β†’ f (ΞΉ n) ＝ inr g β†’ p (ΞΉ n) ＝ β‚€
    case₁ g = ap (Ξ» - β†’ equality-cases - (Ξ» r s β†’ ₁) (Ξ» r s β†’ β‚€))

  d∞ : p ∞ ＝ ₁
  d∞ = equality-cases (f ∞) caseβ‚€ case₁
   where
    caseβ‚€ : (r : ∞ ＝ ∞) β†’ f ∞ ＝ inl r β†’ p ∞ ＝ ₁
    caseβ‚€ r = ap (Ξ» - β†’ equality-cases - (Ξ» r s β†’ ₁) (Ξ» r s β†’ β‚€))

    case₁ : (g : ∞ β‰  ∞) β†’ f ∞ ＝ inr g β†’ p ∞ ＝ ₁
    case₁ g = 𝟘-elim (g refl)


If two discrete-valued functions defined on β„•βˆž agree, they have to
agree at ∞ too, unless WLPO holds:


open import NotionsOfDecidability.Decidable
open import UF.DiscreteAndSeparated

module _ {D : 𝓀 Μ‡ } (d : is-discrete D) where

 disagreement-taboo' : (p q : β„•βˆž β†’ D)
                     β†’ ((n : β„•) β†’ p (ΞΉ n) ＝ q (ΞΉ n))
                     β†’ p ∞ β‰  q ∞
                     β†’ WLPO
 disagreement-taboo' p q f g = basic-discontinuity-taboo r (r-lemma , r-lemma∞)
  where
   A : β„•βˆž β†’ 𝓀 Μ‡
   A u = p u ＝ q u

   Ξ΄ : (u : β„•βˆž) β†’ is-decidable (p u ＝ q u)
   Ξ΄ u = d (p u) (q u)

   r : β„•βˆž β†’ 𝟚
   r = characteristic-map A Ξ΄

   r-lemma : (n : β„•) β†’ r (ΞΉ n) ＝ β‚€
   r-lemma n = characteristic-map-propertyβ‚€-back A Ξ΄ (ΞΉ n) (f n)

   r-lemma∞ : r ∞ ＝ ₁
   r-lemma∞ = characteristic-map-property₁-back A Ξ΄ ∞ (Ξ» a β†’ g a)

 agreement-cotaboo' : Β¬ WLPO
                    β†’ (p q : β„•βˆž β†’ D)
                    β†’ ((n : β„•) β†’ p (ΞΉ n) ＝ q (ΞΉ n))
                    β†’ p ∞ ＝ q ∞
 agreement-cotaboo' Ο† p q f = discrete-is-¬¬-separated d (p ∞) (q ∞)
                               (contrapositive (disagreement-taboo' p q f) Ο†)

disagreement-taboo : (p q : β„•βˆž β†’ 𝟚)
                   β†’ ((n : β„•) β†’ p (ΞΉ n) ＝ q (ΞΉ n))
                   β†’ p ∞ β‰  q ∞
                   β†’ WLPO
disagreement-taboo = disagreement-taboo' 𝟚-is-discrete

agreement-cotaboo : Β¬ WLPO
                  β†’ (p q : β„•βˆž β†’ 𝟚)
                  β†’ ((n : β„•) β†’ p (ΞΉ n) ＝ q (ΞΉ n))
                  β†’ p ∞ ＝ q ∞
agreement-cotaboo = agreement-cotaboo' 𝟚-is-discrete


Added 23rd August 2023. Variation.


basic-discontinuity' : (β„•βˆž β†’ β„•βˆž) β†’ 𝓀₀ Μ‡
basic-discontinuity' f = ((n : β„•) β†’ f (ΞΉ n) ＝ ΞΉ 0) Γ— (f ∞ ＝ ΞΉ 1)

basic-discontinuity-taboo' : (f : β„•βˆž β†’ β„•βˆž)
                           β†’ basic-discontinuity' f
                           β†’ WLPO
basic-discontinuity-taboo' f (fβ‚€ , f₁) = VI
 where
  I : (u : β„•βˆž) β†’ f u ＝ ΞΉ 0 β†’ u β‰  ∞
  I u p q = Zero-not-Succ
             (ι 0 ＝⟨ p ⁻¹ ⟩
              f u ＝⟨ ap f q ⟩
              f ∞ ＝⟨ f₁ ⟩
              ι 1 ∎)

  II : (u : β„•βˆž) β†’ f u β‰  ΞΉ 0 β†’ u ＝ ∞
  II u ν = not-finite-is-∞ fe III
   where
    III : (n : β„•) β†’ u β‰  ΞΉ n
    III n refl = V IV
     where
      IV : f (ι n) ＝ ι 0
      IV = fβ‚€ n

      V : f (ΞΉ n) β‰  ΞΉ 0
      V = Ξ½

  VI : WLPO
  VI u = Cases (finite-isolated fe 0 (f u))
          (Ξ» (p : ΞΉ 0 ＝ f u) β†’ inr (I u (p ⁻¹)))
          (Ξ» (Ξ½ : ΞΉ 0 β‰  f u) β†’ inl (II u (β‰ -sym Ξ½)))

WLPO-is-discontinuous' : WLPO
                       β†’ Ξ£ p κž‰ (β„•βˆž β†’ β„•βˆž), basic-discontinuity' p
WLPO-is-discontinuous' wlpo = II
 where
  inc : 𝟚 β†’ β„•
  inc = 𝟚-cases 0 1
  I : Ξ£ g κž‰ (β„•βˆž β†’ 𝟚) , ((n : β„•) β†’ g (ΞΉ n) ＝ β‚€) Γ— (g ∞ ＝ ₁)
  I = WLPO-is-discontinuous wlpo
  q = pr₁ I
  qβ‚€ = pr₁ (prβ‚‚ I)
  q₁ = prβ‚‚ (prβ‚‚ I)
  p : β„•βˆž β†’ β„•βˆž
  p = ι ∘ inc ∘ q
  pβ‚€ : (n : β„•) β†’ p (ΞΉ n) ＝ ΞΉ 0
  pβ‚€ n = ΞΉ (inc (q (ΞΉ n))) ＝⟨ ap (ΞΉ ∘ inc) (qβ‚€ n) ⟩
         ΞΉ (inc β‚€)         ＝⟨ refl ⟩
         ι 0               ∎
  p₁ : p ∞ ＝ ΞΉ 1
  p₁ = ΞΉ (inc (q ∞)) ＝⟨ ap (ΞΉ ∘ inc) q₁ ⟩
       ΞΉ (inc ₁)     ＝⟨ refl ⟩
       ι 1           ∎
  II : Ξ£ p κž‰ (β„•βˆž β†’ β„•βˆž) , ((n : β„•) β†’ p (ΞΉ n) ＝ ΞΉ 0) Γ— (p ∞ ＝ ΞΉ 1)
  II = p , pβ‚€ , p₁


Added 13th November 2023.


open import Notation.Order

β„•βˆž-linearity-taboo : ((u v : β„•βˆž) β†’ (u β‰Ό v) + (v β‰Ό u))
                   β†’ WLPO
β„•βˆž-linearity-taboo Ξ΄ = III
 where
  g : (u v : β„•βˆž) β†’ (u β‰Ό v) + (v β‰Ό u) β†’ 𝟚
  g u v (inl _) = β‚€
  g u v (inr _) = ₁

  f : β„•βˆž β†’ β„•βˆž β†’ 𝟚
  f u v = g u v (Ξ΄ u v)

  Iβ‚€ : (n : β„•) β†’ f (ΞΉ n) ∞ ＝ β‚€
  Iβ‚€ n = a (Ξ΄ (ΞΉ n) ∞)
   where
    a : (d : (ΞΉ n β‰Ό ∞) + (∞ β‰Ό ΞΉ n)) β†’ g (ΞΉ n) ∞ d ＝ β‚€
    a (inl _) = refl
    a (inr β„“) = 𝟘-elim (β‰Ό-gives-not-β‰Ί ∞ (ΞΉ n) β„“ (∞-β‰Ί-largest n))

  I₁ : (n : β„•) β†’ f ∞ (ΞΉ n) ＝ ₁
  I₁ n = b (Ξ΄ ∞ (ΞΉ n))
   where
    b : (d : (∞ β‰Ό ΞΉ n) + (ΞΉ n β‰Ό ∞)) β†’ g ∞ (ΞΉ n) d ＝ ₁
    b (inl β„“) = 𝟘-elim (β‰Ό-gives-not-β‰Ί ∞ (ΞΉ n) β„“ (∞-β‰Ί-largest n))
    b (inr _) = refl

  II : (b : 𝟚) β†’ f ∞ ∞ ＝ b β†’ WLPO
  II β‚€ e = basic-discontinuity-taboo p IIβ‚€
   where
    p : β„•βˆž β†’ 𝟚
    p x = complement (f ∞ x)

    IIβ‚€ : ((n : β„•) β†’ p (ΞΉ n) ＝ β‚€) Γ— (p ∞ ＝ ₁)
    IIβ‚€ = (Ξ» n β†’ p (ΞΉ n)                ＝⟨refl⟩
                 complement (f ∞ (ΞΉ n)) ＝⟨ ap complement (I₁ n) ⟩
                 complement ₁           ＝⟨refl⟩
                 β‚€                      ∎) ,
           (p ∞                ＝⟨refl⟩
            complement (f ∞ ∞) ＝⟨ ap complement e ⟩
            complement β‚€       ＝⟨refl⟩
            ₁                  ∎)
  II ₁ e = basic-discontinuity-taboo p II₁
   where
    p : β„•βˆž β†’ 𝟚
    p x = f x ∞

    II₁ : ((n : β„•) β†’ p (ΞΉ n) ＝ β‚€) Γ— (p ∞ ＝ ₁)
    II₁ = Iβ‚€ , e

  III : WLPO
  III = II (f ∞ ∞) refl