Baire space

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elif Uskuplu and Victor Blanchi.

Created on 2022-06-30.
Last modified on 2025-04-28.

module set-theory.baire-space where
Imports 
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.lawveres-fixed-point-theorem
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.empty-types
open import foundation-core.identity-types
open import foundation-core.propositions

open import set-theory.cantors-diagonal-argument
open import set-theory.countable-sets
open import set-theory.uncountable-sets

Idea

The Baire space is the set of functions ℕ → ℕ. In other words, it is the set of infinite sequences of natural numbers.

Definition

baire-space : UU lzero
baire-space = ℕ → ℕ

Properties

The Baire space is a set

is-set-baire-space : is-set baire-space
is-set-baire-space = is-set-function-type is-set-ℕ

baire-space-Set : Set lzero
baire-space-Set = (baire-space , is-set-baire-space)

The Baire space is uncountable

We give two proofs. The first proof uses that the successor function on the natural numbers has no fixed points and applies Lawvere’s fixed point theorem. The second proof uses that equality on the natural numbers is decidable, and applies Cantor’s diagonal argument.

abstract
  is-uncountable-baire-space : is-uncountable baire-space-Set
  is-uncountable-baire-space P =
    apply-universal-property-trunc-Prop
      ( is-directly-countable-is-countable baire-space-Set succ-ℕ P)
      ( empty-Prop)
      ( λ H →
        apply-universal-property-trunc-Prop
          ( fixed-point-theorem-Lawvere (pr2 H) succ-ℕ)
          ( empty-Prop)
          ( λ F →
            reductio-ad-absurdum (pr2 F) (has-no-fixed-points-succ-ℕ (pr1 F))))

abstract
  is-uncountable-baire-space' : is-uncountable baire-space-Set
  is-uncountable-baire-space' =
    is-uncountable-sequence-discrete-type-diagonal-argument-Cantor
      ( ℕ-Discrete-Type)
      ( 0)
      ( 1)
      ( is-nonzero-one-ℕ ∘ inv)

Recent changes