FalseWithoutIdentityTypes

Martin Escardo 2015.

If all functions (ℕ → ℕ) → ℕ are continuous then 0 = 1.

In this version we don't use identity types, but we use a universe
instead, in order to define equality on ℕ. This is the only equality
type we consider, and we name it ≡.


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

module ContinuityAxiom.FalseWithoutIdentityTypes where

open import MLTT.Sigma
open import MLTT.NaturalNumbers
open import MLTT.Unit
open import MLTT.Empty

infix  _≡_

_≡_ : ℕ → ℕ → 𝓤₀ ̇
        ≡         = 𝟙
(succ m) ≡         = 𝟘
        ≡ (succ n) = 𝟘
(succ m) ≡ (succ n) = m ≡ n

refl : ∀ n → n ≡ n
refl  = ⋆
refl (succ n) = refl n

≡-ind : (A : (m n : ℕ) → m ≡ n → 𝓤₀ ̇ )
      → (∀ n → A n n (refl n)) →  ∀ m n p → A m n p
≡-ind A r   ⋆               = r 
≡-ind A r (succ m)  p        = 𝟘-elim p
≡-ind A r  (succ n) p        = 𝟘-elim p
≡-ind A r (succ m) (succ n) p = ≡-ind
                                 (λ m n → A (succ m) (succ n))
                                 (λ n → r(succ n)) m n p

We only use ≡-ind to define ≡-rec:


≡-rec : (A : ℕ → ℕ → 𝓤₀ ̇ ) → (∀ n → A n n) →  ∀ m n → m ≡ n → A m n
≡-rec A = ≡-ind (λ m n _ → A m n)


We only use ≡-rec to define transport:


transport : (A : ℕ → 𝓤₀ ̇ ) → {x y : ℕ} → x ≡ y → A x → A y
transport A {x} {y} = ≡-rec (λ x y → A x → A y) (λ _ a → a) x y


From transport we prove all properties of equality we need here:


sym : ∀{x y} → x ≡ y → y ≡ x
sym {x} {y} p = transport (λ z → z ≡ x) {x} {y} p (refl x)

euclidean : ∀{a b c} → b ≡ c → b ≡ a → c ≡ a
euclidean {a} {b} {c} = transport (λ d → d ≡ a) {b} {c}

trans : ∀{x y z} → x ≡ y → y ≡ z → x ≡ z
trans {x} {y} {z} p = euclidean {z} {y} (sym {x} p)

ap : ∀(f : ℕ → ℕ) → ∀{x y} → x ≡ y → f x ≡ f y
ap f {x} {y} p = transport (λ z → f x ≡ f z) {x} {y} p (refl(f x))


The Baire space of infinite sequences of natural numbers, ranged over
by α and β:


Baire : 𝓤₀ ̇
Baire = ℕ → ℕ

head : {X : ℕ → 𝓤₀ ̇ } → ((i : ℕ) → X i) → X 
head α = α 

tail : {X : ℕ → 𝓤₀ ̇ } → ((i : ℕ) → X i) → ((i : ℕ) → X (succ i))
tail α = λ i → α(succ i)

_≡[_]_ : Baire → ℕ → Baire → 𝓤₀ ̇
α ≡[ zero ] β   = 𝟙
α ≡[ succ n ] β = (head α ≡ head β) × (tail α ≡[ n ] tail β)


The sequence consisting of n zeros followed by infinitely many k's
is written "n zeros-and-then k":


_zeros-and-then_ : ℕ → ℕ → Baire
(        zeros-and-then k)  i       = k
((succ n) zeros-and-then k)         = 
((succ n) zeros-and-then k) (succ i) = (n zeros-and-then k) i

zeros-and-then-spec₀ : ∀ n k → (n zeros-and-then k) n ≡ k
zeros-and-then-spec₀         k = refl k
zeros-and-then-spec₀ (succ n) k = zeros-and-then-spec₀ n k


The sequence consisting of infinitely many zeros:


O : Baire
O = λ i → 

zeros-and-then-spec₁ : ∀ n k → O ≡[ n ] (n zeros-and-then k)
zeros-and-then-spec₁ zero k = ⋆
zeros-and-then-spec₁ (succ n) k = ⋆ , (zeros-and-then-spec₁ n k)


We now come to the subject of this file. We define the Curry-Howard
interpretation of a Brouwerian continuity principle, and show that not
all functions are continuous. Notice that, by definition, 0≡1 is 𝟘.


continuous : (Baire → ℕ) → 𝓤₀ ̇
continuous f = ∀ α → Σ n ꞉ ℕ , (∀ β → α ≡[ n ] β → f α ≡ f β)

theorem : (∀(f : Baire → ℕ) → continuous f) →  ≡ 
theorem continuity = zero-is-one
 where

  M : (Baire → ℕ) → ℕ
  M f = pr₁ (continuity f O)

  continuity₀ : ∀ f β → O ≡[ M f ] β → f O ≡ f β
  continuity₀ f = pr₂(continuity f O)

  m : ℕ
  m = M(λ α → )

  f : Baire → ℕ
  f β = M(λ α → β (α m))

  crucial-observation : f O ≡ m
  crucial-observation = refl (f O)

  crucial-fact : ∀ β → O ≡[ M f ] β → m ≡ f β
  crucial-fact = continuity₀ f

  lemma₀ : M f ≡  →  ≡ 
  lemma₀ p = zero-is-one
   where
    c₀ : ∀ β → O ≡[ M f ] β
    c₀ β = transport (λ n → O ≡[ n ] β) (sym {M f} p) (refl )

    c₁ : ∀ β → m ≡ f β
    c₁ β = crucial-fact β (c₀ β)

    c₂ : M(λ α → α m) ≡ m
    c₂ = sym {m} (c₁ (λ i → i))

    c₃ : ∀ α → O ≡[ M(λ α → α m) ] α →  ≡ α m
    c₃ = continuity₀ (λ α → α m)

    c₄ : ∀ α → O ≡[ m ] α →  ≡ α m
    c₄ = transport (λ n → ∀ α → O ≡[ n ] α →  ≡ α m) c₂ c₃

    α : Baire
    α = m zeros-and-then 

    α-property₀ : α m ≡ 
    α-property₀ = zeros-and-then-spec₀ m 

    α-property₁ : O ≡[ m ] α
    α-property₁ = zeros-and-then-spec₁ m 

    c₅ :  ≡ α m
    c₅ = c₄ α α-property₁

    zero-is-one :  ≡ 
    zero-is-one = trans {} {α m} c₅ α-property₀

  lemma₁ : (Σ n ꞉ ℕ , (M f ≡ succ n)) →  ≡ 
  lemma₁ (n , p) = zero-is-one
   where
    β : Baire
    β = (M f) zeros-and-then 

    β-property₀ : β (M f) ≡ 
    β-property₀ = zeros-and-then-spec₀ (M f) 

    β-property₁ : O ≡[ M f ] β
    β-property₁ = zeros-and-then-spec₁ (M f) 

    c₀ : f β ≡ m
    c₀ = sym {m} (crucial-fact β β-property₁)

    c₁ : ∀ α → O ≡[ f β ] α → β  ≡ β (α m)
    c₁ α = continuity₀ (λ α → β (α m)) α

    c₂ : ∀ α → O ≡[ m ] α → β  ≡ β (α m)
    c₂ = transport (λ n → ∀ α → O ≡[ n ] α → β  ≡ β (α m)) c₀ c₁

    α : Baire
    α = m zeros-and-then (M f)

    α-property₀ : α m ≡ M f
    α-property₀ = zeros-and-then-spec₀ m (M f)

    α-property₁ : O ≡[ m ] α
    α-property₁ = zeros-and-then-spec₁ m (M f)

    c₃ : β  ≡ β (α m)
    c₃ = c₂ α α-property₁

    c₅ : β (α m) ≡ β (M f)
    c₅ = ap β α-property₀

    c₆ : β (α m) ≡ 
    c₆ = trans {β (α m)} c₅ β-property₀

    c₄ : β  ≡ 
    c₄ = trans {β } c₃ c₆

    c₈ : O ≡[ succ n ] β
    c₈ = transport (λ n → O ≡[ n ] β) p β-property₁

    c₉ : O ≡[ succ n ] β →  ≡ β 
    c₉ e = pr₁ e

    c₇ :  ≡ β 
    c₇ = c₉ c₈

    zero-is-one :  ≡ 
    zero-is-one = trans {} {β } c₇ c₄

  lemma : (Σ n ꞉ ℕ , M f ≡ n) →  ≡ 
  lemma (      , p) = lemma₀ p
  lemma (succ n , p) = lemma₁(n , p)

  zero-is-one :  ≡ 
  zero-is-one = lemma(M f , refl(M f))


The following observation was communicated to me independently by
each of Altenkirch, Coquand and Martin-Lӧf.

A continuous function is extensional in the sense that it assigns the
same value to pointwise equal inputs:


continuous-functions-are-extensional : (f : Baire → ℕ)
                                     → continuous f
                                     → ∀ α β → (∀ i → α i ≡ β i) → f α ≡ f β
continuous-functions-are-extensional f f-continuous α β e = g β (h α β e n)
 where
  n : ℕ
  n = pr₁ (f-continuous α)

  g : ∀ β → α ≡[ n ] β → f α ≡ f β
  g = pr₂(f-continuous α)

  h : ∀ α β → (∀ i → α i ≡ β i) → ∀ n → α ≡[ n ] β
  h α β e zero     = ⋆
  h α β e (succ n) = (e zero) , (h (tail α) (tail β) (tail e) n)


So there is some amount of extensionality built-in in the definition
of continuity.

And here is a simplification suggested by an anonymous TLCA'2015
referee, which we incorporated in the TLCA final version of the paper:

  "Considering \beta = 0^(Mf+1) 1^\omega and \alpha = 0^m
   (Mf+1)^\omega, one can avoid the proof case Mf = 0 and use just the
   other one."


≡[]-lemma : {α β : Baire} (n : ℕ) → α ≡[ succ n ] β → α ≡[ n ] β
≡[]-lemma zero     _       = ⋆
≡[]-lemma (succ n) (p , q) = p , ≡[]-lemma n q

theorem' : (∀(f : Baire → ℕ) → continuous f) →  ≡ 
theorem' continuity = zero-is-one
 where
  M : (Baire → ℕ) → ℕ
  M f = pr₁ (continuity f O)

  continuity₀ : ∀ f β → O ≡[ M f ] β → f O ≡ f β
  continuity₀ f = pr₂ (continuity f O)

  m : ℕ
  m = M(λ α → )

  f : Baire → ℕ
  f β = M(λ α → β (α m))

  β : Baire
  β = (succ(M f)) zeros-and-then 

  β-property₀ : β (succ(M f)) ≡ 
  β-property₀ = zeros-and-then-spec₀ (succ(M f)) 

  β-property₁ : O ≡[ succ(M f) ] β
  β-property₁ = zeros-and-then-spec₁ (succ(M f)) 

  β-property₂ : O ≡[ M f ] β
  β-property₂ = ≡[]-lemma (M f) β-property₁

  c₀ : f β ≡ m
  c₀ = sym {m} (continuity₀ f β β-property₂)

  c₁ : ∀ α → O ≡[ f β ] α → β  ≡ β (α m)
  c₁ = continuity₀ (λ α → β (α m))

  c₂ : ∀ α → O ≡[ m ] α → β  ≡ β (α m)
  c₂ = transport (λ n → ∀ α → O ≡[ n ] α → β  ≡ β (α m)) c₀ c₁

  α : Baire
  α = m zeros-and-then (succ(M f))

  α-property₀ : α m ≡ succ(M f)
  α-property₀ = zeros-and-then-spec₀ m (succ(M f))

  α-property₁ : O ≡[ m ] α
  α-property₁ = zeros-and-then-spec₁ m (succ(M f))

  c₃ : β  ≡ β (α m)
  c₃ = c₂ α α-property₁

  c₄ : β (α m) ≡ β (succ(M f))
  c₄ = ap β {α m} {succ(M f)} α-property₀

  c₅ : β (α m) ≡ 
  c₅ = trans {β (α m)} c₄ β-property₀

  c₆ : β  ≡ 
  c₆ = trans {β } {β (α m)} {} c₃ c₅

  c₇ :  ≡ β 
  c₇ = pr₁ β-property₁

  zero-is-one :  ≡ 
  zero-is-one = trans {} {β } {} c₇ c₆