module Padova2025.Explorations.Uncountability.Applications where

Applications

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Existential
import Padova2025.Explorations.Uncountability.Lawvere as L

Uncountability of the Cantor space

A premier example for an uncountable type is the Cantor space, the type of infinite binary sequences.

Cantor : Set
Cantor = ℕ → Bool

We will prove it uncountable in five senses.

-- A strong notion of two functions being distinct.
_#_ : {A B : Set} → (A → B) → (A → B) → Set
f # g = ∃[ a ] f a ≢ g a

IsSplitSurjective : {A B : Set} → (A → B) → Set
IsSplitSurjective f = (y : _) → ∃[ x ] y ≡ f x

IsWeaklySplitSurjective : {A B : Set} → (B → B → Set) → (A → B) → Set
IsWeaklySplitSurjective _≈_ f = (y : _) → ∃[ x ] y ≈ f x

fixpoint-free : {x : Bool} → not x ≡ x → ⊥
fixpoint-free = {!!}

fixpoint-free' : ¬ (∃[ x ] not x ≡ x)
fixpoint-free' = {!!}

The following is the strongest form of the result that the Cantor space is uncountable: For every potential enumeration f : ℕ → Cantor, there is a sequence α : Cantor such that for every number n, there is a position at which the sequences α and f n differ.

uncountable₀ : (f : ℕ → Cantor) → Σ[ α ∈ Cantor ] ((n : ℕ) → α # f n)
uncountable₀ = {!!}

We can then gradually weaken the result, in order to obtain statements which are more readily recognizable as uncountability assertions.

uncountable₁ : (f : ℕ → Cantor) → Σ[ α ∈ Cantor ] ¬ (∃[ n ] α ≗ f n)
uncountable₁ = {!!}

uncountable₂ : (f : ℕ → Cantor) → Σ[ α ∈ Cantor ] ¬ (∃[ n ] α ≡ f n)
uncountable₂ = {!!}

uncountable₁' : ¬ (Σ[ f ∈ (ℕ → Cantor) ] IsWeaklySplitSurjective _≗_ f)
uncountable₁' = {!!}

uncountable₂' : ¬ (Σ[ f ∈ (ℕ → Cantor) ] IsSplitSurjective f)
uncountable₂' = {!!}

Uncountability of the Baire space

Baire : Set
Baire = ℕ → ℕ

baire-uncountable₀ : (f : ℕ → Baire) → Σ[ α ∈ Baire ] ((n : ℕ) → α # f n)
baire-uncountable₀ = {!!}

Uncountability of the universe

Using similar methods, we can also show that the type Set of all small types is not countable.

Martín Escardó has explored this topic in great detail.