Baire space
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Elif Uskuplu and Victor Blanchi.
Created on 2022-06-30.
Last modified on 2023-06-25.
module set-theory.baire-space where
Imports
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.lawveres-fixed-point-theorem open import foundation.negation open import foundation.propositional-truncations open import foundation.universe-levels open import foundation-core.empty-types open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.sets open import set-theory.countable-sets open import set-theory.uncountable-sets
Idea
The Baire space is the type of functions ℕ → ℕ
.
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 f g = is-prop-all-elements-equal ( λ p q → ( inv (is-retraction-eq-htpy p)) ∙ ( ( ap ( eq-htpy) ( eq-htpy ( λ n → eq-is-prop' ( is-set-ℕ (f n) (g n)) ( htpy-eq p n) ( htpy-eq q n)))) ∙ ( is-retraction-eq-htpy q))) baire-space-Set : Set lzero pr1 baire-space-Set = baire-space pr2 baire-space-Set = is-set-baire-space
The Baire Space is uncountable
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))))
Recent changes
- 2023-06-25. Fredrik Bakke. Fix alignment
where
blocks (#670). - 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).