Martin Escardo, 9th September 2026.
This is an Agda companion for the preprint
Compact totally separated types
-------------------------------
https://arxiv.org/abs/2609.10447v3, 28th September 2026
Martín Hötzel Escardó
https://www.cs.bham.ac.uk/~mhe/
This file is
https://github.com/martinescardo/TypeTopology/blob/master/source/TypeTopology/CompactTotallySeparatedTypesArticle.lagda
Readers of earlier arXiv versions of the paper should use the Agda
companions [1] and [2] below instead.
This file follows the definitions, lemmas, propositions, theorems,
examples and remarks of the paper above, in the same order and with
the same numbering, including the mathematical discussions in its
prose, so that a reader of the paper can walk this file alongside
it. The name of each entry is the number the item has in the paper,
and the comment after it is the LaTeX label of that item.
Claims that the paper makes in running prose, outside proofs, appear
here too, under names beginning with Prose. Each of them is named in
the LaTeX source by \claim{name}, placed where the claim is made, and
the names are written out in order to the file main.claims when the
paper is typeset, so that the two lists can be compared. Claims about
models rather than about the theory, such as the ones about the
effective topos, are recorded as comments, since they are not
formalizable here.
We include all HoTT/UF assumptions as module parameters. They do not
include function extensionality because it follows from
univalence. However, the TypeTopology repository is careful to
minimize the number of assumptions for each result, and readers
interested in such foundational issues can follow the definitions
given here to find out exactly what assumptions each result uses.
[1] https://arxiv.org/abs/2609.10447v1, 9th September 2026
https://github.com/martinescardo/TypeTopology/blob/0025fb18cda5504f36b74cdbd2a05a8a4e1c1974/source/TypeTopology/CompactTotallySeparatedTypesArticle.lagda
[2] https://arxiv.org/abs/2609.10447v2, 15th September 2026
https://github.com/martinescardo/TypeTopology/blob/c3e7e439d47ab9c0dfa0849b368bd076be0a19fb/source/TypeTopology/CompactTotallySeparatedTypesArticle.lagda
Cite as
@misc{escardo2026compacttotallyseparatedtypes,
title={Compact totally separated types},
author={Mart\'{i}n H\"otzel Escard\'o},
year={2026},
eprint={2609.10447},
archivePrefix={arXiv},
primaryClass={math.LO},
url={https://arxiv.org/abs/2609.10447},
}
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import UF.PropTrunc
open import UF.Size
open import UF.Yoneda using (univalence-via-singletons←)
open import UF.EquivalenceExamples using (Σ-cong)
open import UF.Equiv-FunExt using (≃-Sym)
open import UF.Univalence
module TypeTopology.CompactTotallySeparatedTypesArticle
(ua : Univalence)
(pt : propositional-truncations-exist)
(sr : Set-Replacement pt)
where
open import MLTT.Spartan
open import UF.FunExt
open import UF.Subsingletons
open import UF.UA-FunExt
private
fe : FunExt
fe = Univalence-gives-FunExt ua
fe' : Fun-Ext
fe' {𝓤} {𝓥} = fe 𝓤 𝓥
fe₀ : funext 𝓤₀ 𝓤₀
fe₀ = fe 𝓤₀ 𝓤₀
pe : PropExt
pe = Univalence-gives-PropExt ua
pe' : Prop-Ext
pe' {𝓤} = pe 𝓤
open PropositionalTruncation pt
open import Apartness.Definition
using (module Apartness ;
is-tight ;
is-irreflexive ;
tight-types-are-¬¬-separated' ;
tight-types-are-sets')
open Apartness pt using (is-apartness ; apartness-is-irreflexive')
open import Notation.CanonicalMap
open import Rationals.Type using (ℚ)
open import DedekindReals.Type fe' pe' pt
using (ℝ ; ℝ-is-set ; canonical-map-ℚ-to-ℝ)
open import DedekindReals.Order fe' pe' pt using (ℚ-to-ℝ-is-embedding)
open import CoNaturals.UniversalProperty fe
using (PRED-is-the-homotopy-final-coalgebra ; is-homomorphism)
open import NotionsOfDecidability.Complemented
open import Taboos.LPO
open import Taboos.MarkovsPrinciple
open import Taboos.WLPO
open import TypeTopology.DecidabilityOfNonContinuity fe₀
using (continuous ;
noncontinuous-map-gives-WLPO ;
WLPO-gives-noncontinous-map ;
¬WLPO-iff-all-maps-are-¬¬-continuous ;
MP-and-¬WLPO-give-that-all-functions-are-continuous)
open import TypeTopology.Density
open import TypeTopology.DenseMapsProperties using (surjections-are-dense)
open import UF.ClassicalLogic
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.Hedberg
open import UF.ImageAndSurjection pt
open import UF.NotNotStablePropositions
open import UF.Powerset-MultiUniverse hiding (𝕋)
open import Quotient.FromSetReplacement pt fe' pe'
using (set-quotients-from-set-replacement)
open import Quotient.GivesSetReplacement
using (set-replacement-from-set-quotients-and-prop-trunc)
open import Quotient.Type using (set-quotients-exist)
open import UF.PairFun
open import UF.Retracts
open import UF.Retracts-FunExt
using (codomain-is-retract-of-function-space-with-pointed-domain)
open import UF.Sets
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import TypeTopology.FailureOfTotalSeparatedness fe₀
open import TypeTopology.GenericConvergentSequence
open import TypeTopology.SigmaDiscrete
open import TypeTopology.SimpleTypes fe pt
open import TypeTopology.TotallySeparated
open totally-separated-reflection fe pt
open total-separatedness-via-apartness pt
open import TypeTopology.CompactTypes
open CompactTypesPT pt
open import Fin.Topology using (Fin-Compact)
open import Fin.Type using (Fin)
open import MLTT.Plus-Properties using (+disjoint)
open import CantorSchroederBernstein.CSB-WLPO
using (Π-compact-types-are-Π-Compact)
open import SyntheticHomotopyTheory.Circle.Construction pt (ua 𝓤₀)
using (Tℤ ; loops-at-base-equivalent-to-ℤ)
renaming (base to base-of-Tℤ)
open import TypeTopology.Cantor using (𝟚ᴺ ; module notions-of-continuity)
open notions-of-continuity 𝟚 𝟚-is-discrete using (uniformly-continuous)
open import TypeTopology.CantorSearch
using (Cantor-uniformly-searchable ; having-root-is-decidable)
open import TypeTopology.DisconnectedTypes
open import TypeTopology.ExtendedSumCompact fe
open import TypeTopology.ExtensionTotallySeparated
open import TypeTopology.GenericConvergentSequenceCompactness fe₀
open import TypeTopology.MicroTychonoff
open import TypeTopology.WeaklyCompactTypes fe pt
open import InjectiveTypes.Blackboard fe
open import Ordinals.Arithmetic fe
open import Ordinals.CompactnessOfSuprema ua pt
open import Ordinals.Closure fe
open import Ordinals.ConvergentSequence ua using (ω+𝟙-is-⊴-ℕ∞)
open import Ordinals.Equivalence
open import Ordinals.Injectivity
open ordinals-injectivity fe
open topped-ordinals-injectivity fe using () renaming (_↗_ to _↗ᵀ_)
open import Ordinals.LexicographicOrder
open import Ordinals.Maps using (is-simulation)
open import Ordinals.Notions hiding (is-irreflexive)
open import Ordinals.OrdinalOfOrdinals ua hiding (_≾_)
open import Ordinals.OrdinalOfOrdinalsSuprema ua
open suprema pt sr
open import Ordinals.OrdinalOfTruthValues fe 𝓤₀ (pe 𝓤₀)
open import Ordinals.ShulmanTaboo fe (pe 𝓤₀)
using (shulmans-taboo)
renaming (_≺_ to _≺ˢ_)
open import Ordinals.Taboos
using (Every-Discrete-Ordinal-Is-Trichotomous ;
EM-if-Every-Discrete-Ordinal-Is-Trichotomous)
open import Ordinals.ToppedAdditionProperties ua
open import Ordinals.ToppedArithmetic fe
open import Ordinals.ToppedType fe
open import Ordinals.TotallySeparated
open import Ordinals.TrichotomousArithmetic fe
open import Ordinals.TrichotomousType fe
open import Ordinals.Type
open import Ordinals.Underlying
open import Ordinals.WellOrderArithmetic
open import TypeTopology.SquashedSum fe
open import TypeTopology.SquashedCantor fe
using (Cantor ;
𝔻-Cantor-≃-Cantor ;
is-Cantor-𝔻-coalgebra-map ;
Cantor-is-final-𝔻-coalgebra)
open import TypeTopology.DelayMonad fe
using (𝔻 ;
is-𝔻-coalgebra-map ;
𝔻-is-final-coalgebra)
open import TypeTopology.BoundedDecreasingSequences fe'
using (𝔹 ; 𝔹-is-compact∙ ; 𝔹-is-totally-separated)
open import Ordinals.BrouwerCodes
open import Ordinals.BrouwerCodesInterpretations ua pt sr
open import Ordinals.InfProperty
open import TypeTopology.LimitPoints
open import TypeTopology.MicroInfTychonoff fe
open import TypeTopology.SigmaTotallySeparated
using (Σ-indexed-by-ℕ∞-is-totally-separated-if-family-at-∞-is-prop)
import Ordinals.BrouwerCodesDiscreteAndCompactInterpretations
import Ordinals.BrouwerCodesIntoInductiveRecursiveCodes
import Ordinals.FailureOfTotalSeparatedness
import Ordinals.FailureOfTrichotomy
import Ordinals.InductiveRecursiveCodesInterpretations
import Ordinals.LimitPoints
module BDC = Ordinals.BrouwerCodesDiscreteAndCompactInterpretations fe
module IRC = Ordinals.InductiveRecursiveCodesInterpretations fe
module OLP = Ordinals.LimitPoints fe
module BtoE = Ordinals.BrouwerCodesIntoInductiveRecursiveCodes fe
module FTS = Ordinals.FailureOfTotalSeparatedness ua pt sr
module FTr = Ordinals.FailureOfTrichotomy ua pt sr
\end{code}
Section 2. Preliminaries
Labels: Section 2 = sec:foundations.
\begin{code}
Definition-2-1 : (X : 𝓤 ̇ ) → 𝓤 ̇
Definition-2-1 X = is-decidable X
Definition-2-2 : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇
Definition-2-2 = _↔_
Definition-2-3 : 𝓤 ̇ → 𝓤 ̇
Definition-2-3 = is-singleton
Definition-2-3' : {X : 𝓤 ̇ } → (X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Definition-2-3' = ∃!
Definition-2-4 : {X : 𝓤 ̇ } → X → 𝓤 ̇
Definition-2-4 = is-h-isolated
Definition-2-4' : 𝓤 ̇ → 𝓤 ̇
Definition-2-4' = is-set
Theorem-2-5 : {X : 𝓤 ̇ } (x : X)
→ ((y : X) → collapsible (x ＝ y))
→ (y : X) → is-prop (x ＝ y)
Theorem-2-5 = local-hedberg
Definition-2-6 : (𝓤 : Universe) → 𝓤 ⁺ ̇
Definition-2-6 = Ω
Definition-2-7 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → Y → 𝓤 ⊔ 𝓥 ̇
Definition-2-7 = fiber
Definition-2-8 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-8 = is-vv-equiv
Definition-2-9 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-9 = is-surjection
Definition-2-10 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-10 = is-embedding
Prose-embeddings-and-left-cancellability
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-embedding f
→ left-cancellable f
Prose-embeddings-and-left-cancellability = embeddings-are-lc
Prose-embeddings-and-left-cancellability'
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ left-cancellable f
→ is-set Y
→ is-embedding f
Prose-embeddings-and-left-cancellability' = lc-maps-into-sets-are-embeddings
\end{code}
The claim about the topological topos is about a model rather than
about the theory, and so is not formalizable here.
\begin{code}
Prose-rationals-embed-into-reals : is-embedding (canonical-map ℚ ℝ)
Prose-rationals-embed-into-reals = ℚ-to-ℝ-is-embedding
Prose-rationals-embed-into-reals' : is-set ℝ
Prose-rationals-embed-into-reals' = ℝ-is-set
Definition-2-11 : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Definition-2-11 = is-complemented
Definition-2-12 : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ⁺ ̇
Definition-2-12 {𝓤} {𝓥} = 𝓟 {𝓥} {𝓤}
Definition-2-13 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-13 = image
Definition-2-14 : 𝓤 ⁺ ̇ → 𝓤 ⁺ ̇
Definition-2-14 = is-small
Definition-2-14-locally : 𝓤 ⁺ ̇ → 𝓤 ⁺ ̇
Definition-2-14-locally = is-locally-small
Prose-smallness-and-univalence : Univalence
→ (X : 𝓤 ̇ ) (𝓥 : Universe)
→ is-prop (X is 𝓥 small)
Prose-smallness-and-univalence = being-small-is-prop
Prose-smallness-and-univalence' : ((X : 𝓤 ̇ ) → is-prop (X is 𝓤 small))
→ is-univalent 𝓤
Prose-smallness-and-univalence' {𝓤} h = univalence-via-singletons← γ
where
γ : (X : 𝓤 ̇ ) → ∃! Y ꞉ 𝓤 ̇ , X ≃ Y
γ X = pointed-props-are-singletons (X , ≃-refl X) (equiv-to-prop e (h X))
where
e : (Σ Y ꞉ 𝓤 ̇ , X ≃ Y) ≃ (Σ Y ꞉ 𝓤 ̇ , Y ≃ X)
e = Σ-cong (λ Y → ≃-Sym fe)
Definition-2-15 : 𝓤ω
Definition-2-15 = Set-Replacement pt
Definition-2-16 : 𝓤ω
Definition-2-16 = set-quotients-exist
Prose-set-replacement-and-quotients : Set-Replacement pt → set-quotients-exist
Prose-set-replacement-and-quotients = set-quotients-from-set-replacement
Prose-set-replacement-and-quotients' : set-quotients-exist → Set-Replacement pt
Prose-set-replacement-and-quotients' sq
= set-replacement-from-set-quotients-and-prop-trunc sq pt
Definition-2-17 : 𝓤 ̇ → 𝓤 ̇
Definition-2-17 = is-¬¬-separated
Lemma-2-18 : {X : 𝓤 ̇ } → is-¬¬-separated X → is-set X
Lemma-2-18 = ¬¬-separated-types-are-sets fe'
Definition-2-19 : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Definition-2-19 = is-apartness
Definition-2-19' : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Definition-2-19' = is-tight
Prose-tight-apartness-gives-set
: {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
→ is-apartness _♯_
→ (x y : X) → x ♯ y → x ≠ y
Prose-tight-apartness-gives-set = apartness-is-irreflexive'
Prose-tight-apartness-gives-¬¬-separated
: {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
→ is-irreflexive _♯_
→ is-tight _♯_
→ is-¬¬-separated X
Prose-tight-apartness-gives-¬¬-separated = tight-types-are-¬¬-separated'
Prose-tight-apartness-gives-set'
: {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
→ is-irreflexive _♯_
→ is-tight _♯_
→ is-set X
Prose-tight-apartness-gives-set' _♯_ = tight-types-are-sets' _♯_ (fe _ _)
\end{code}
What the paper calls extreme density is called density in
TypeTopology, and the names below keep the TypeTopology spelling.
\begin{code}
Definition-2-20 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-20 = is-dense
Definition-2-20' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Definition-2-20' f = is-empty (complement-of-image f)
Definition-2-20-equivalence
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-dense f ↔ is-empty (complement-of-image f)
Definition-2-20-equivalence = density-characterization pt
Definition-2-20-is-prop
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-prop (is-dense f)
Definition-2-20-is-prop = being-dense-is-prop fe'
Prose-em-dense-surjection : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-surjection f
→ is-dense f
Prose-em-dense-surjection = surjections-are-dense pt
Prose-em-dense-surjection' : EM (𝓤 ⊔ 𝓥)
→ {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-dense f
→ is-surjection f
Prose-em-dense-surjection' em f d y =
Cases (em (y ∈image f) (being-in-the-image-is-prop y f))
id
(λ (ν : ¬ (y ∈image f)) → 𝟘-elim (d (y , (λ (x , p) → ν ∣ x , p ∣))))
Lemma-2-21 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : Y → 𝓦 ̇ } {j : X → Y} {f g : Π Z}
→ is-dense j
→ ((y : Y) → is-¬¬-separated (Z y))
→ f ∘ j ∼ g ∘ j
→ f ∼ g
Lemma-2-21 = dense-maps-into-¬¬-separated-types-are-rc'
Lemma-2-21' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {j : X → Y} {f g : Y → Z}
→ is-dense j
→ is-¬¬-separated Z
→ f ∘ j ∼ g ∘ j
→ f ∼ g
Lemma-2-21' = dense-maps-into-¬¬-separated-types-are-rc
Lemma-2-22 : 𝟚 → Ω 𝓤
Lemma-2-22 = 𝟚-to-Ω
Definition-2-23 : (𝓤 : Universe) → 𝓤 ⁺ ̇
Definition-2-23 = Global-Choice
Prose-global-choice-reformulation : Global-Choice 𝓤 → Global-Choice' 𝓤
Prose-global-choice-reformulation = Global-Choice-gives-Global-Choice'
Prose-global-choice-reformulation' : Global-Choice' 𝓤 → Global-Choice 𝓤
Prose-global-choice-reformulation' = Global-Choice'-gives-Global-Choice
Definition-2-24 : (𝓤 : Universe) → 𝓤 ⁺ ̇
Definition-2-24 = EM
Definition-2-25 : 𝓤₀ ̇
Definition-2-25 = LPO
Definition-2-25' : 𝓤₀ ̇
Definition-2-25' = WLPO
Prose-compactness-of-N-is-LPO : is-compact ℕ ↔ LPO
Prose-compactness-of-N-is-LPO = compact-ℕ-gives-LPO fe₀ ,
LPO-gives-compact-ℕ fe₀
Prose-EM-LPO-WLPO : EM 𝓤₀ → LPO
Prose-EM-LPO-WLPO em = LPO'-gives-LPO
(λ u → em (is-finite u) (being-finite-is-prop fe₀ u))
Prose-EM-LPO-WLPO' : LPO → WLPO
Prose-EM-LPO-WLPO' = LPO-gives-WLPO fe₀
Prose-EM-LPO-WLPO'' : MP 𝓤₀ → WLPO → LPO
Prose-EM-LPO-WLPO'' = MP-and-WLPO-give-LPO fe₀
\end{code}
The claim that the taboos are independent of the foundation, holding
under classical logic and failing in the topological and effective
toposes, is about models rather than about the theory, and so is not
formalizable here.
\begin{code}
Remark-2-26 : WLPO ↔ (Σ f ꞉ (ℕ∞ → ℕ) , ¬ continuous f)
Remark-2-26 = WLPO-gives-noncontinous-map , noncontinuous-map-gives-WLPO
Prose-noncontinuity-and-WLPO : (Σ f ꞉ (ℕ∞ → ℕ) , ¬ continuous f) → WLPO
Prose-noncontinuity-and-WLPO = noncontinuous-map-gives-WLPO
Prose-noncontinuity-and-WLPO' : WLPO → (Σ f ꞉ (ℕ∞ → ℕ) , ¬ continuous f)
Prose-noncontinuity-and-WLPO' = WLPO-gives-noncontinous-map
Prose-noncontinuity-and-WLPO'' : ¬ WLPO ↔ ((f : ℕ∞ → ℕ) → ¬¬ continuous f)
Prose-noncontinuity-and-WLPO'' = ¬WLPO-iff-all-maps-are-¬¬-continuous
Prose-noncontinuity-and-WLPO'''
: MP 𝓤₀ → ¬ WLPO → (f : ℕ∞ → ℕ) → continuous f
Prose-noncontinuity-and-WLPO'''
= MP-and-¬WLPO-give-that-all-functions-are-continuous
Definition-2-27 : 𝓥 ̇ → 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
Definition-2-27 Y X = retract Y of X
Definition-2-28 : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {Y : 𝓦 ̇ } {B : Y → 𝓣 ̇ }
→ (f : X → Y)
→ ((x : X) → A x → B (f x))
→ Σ A → Σ B
Definition-2-28 = pair-fun
Lemma-2-29-1 : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {Y : 𝓦 ̇ } {B : Y → 𝓣 ̇ }
(f : X → Y) (g : (x : X) → A x → B (f x))
→ is-vv-equiv f
→ ((x : X) → is-vv-equiv (g x))
→ is-vv-equiv (pair-fun {A = A} {B = B} f g)
Lemma-2-29-1 = pair-fun-is-vv-equiv
Lemma-2-29-2 : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {Y : 𝓦 ̇ } {B : Y → 𝓣 ̇ }
(f : X → Y) (g : (x : X) → A x → B (f x))
→ is-embedding f
→ ((x : X) → is-embedding (g x))
→ is-embedding (pair-fun {A = A} {B = B} f g)
Lemma-2-29-2 = pair-fun-is-embedding
Lemma-2-29-3 : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {Y : 𝓦 ̇ } {B : Y → 𝓣 ̇ }
(f : X → Y) (g : (x : X) → A x → B (f x))
→ is-dense f
→ ((x : X) → is-dense (g x))
→ is-dense (pair-fun {A = A} {B = B} f g)
Lemma-2-29-3 = pair-fun-dense
Lemma-2-29-4 : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ )
→ ((x : X) → retract (A x) of (B x))
→ retract (Σ A) of (Σ B)
Lemma-2-29-4 = Σ-retract
\end{code}
Section 3. Discreteness and total separatedness
Labels: Section 3 = sec:discrete-tot-sep.
\begin{code}
Example-3-1 : 𝓤₀ ̇
Example-3-1 = ℕ∞
Example-3-1' : retract ℕ∞ of (ℕ → 𝟚)
Example-3-1' = ℕ∞-retract-of-Cantor fe₀
Example-3-1'' : {X : 𝓤 ̇ } (κ : X → 𝟙 + X)
→ ∃! h ꞉ (X → ℕ∞), is-homomorphism κ h
Example-3-1'' = PRED-is-the-homotopy-final-coalgebra
Definition-3-2 : {X : 𝓤 ̇ } → X → 𝓤 ̇
Definition-3-2 = is-isolated
Definition-3-2' : 𝓤 ̇ → 𝓤 ̇
Definition-3-2' = is-discrete
Examples-3-3-1-props : {X : 𝓤 ̇ } → is-prop X → is-discrete X
Examples-3-3-1-props = props-are-discrete
Examples-3-3-1-𝟚 : is-discrete 𝟚
Examples-3-3-1-𝟚 = 𝟚-is-discrete
Examples-3-3-2 : is-discrete ℕ
Examples-3-3-2 = ℕ-is-discrete
Examples-3-3-3 : is-discrete ℕ∞ ↔ WLPO
Examples-3-3-3 = ℕ∞-discrete-gives-WLPO , WLPO-gives-ℕ∞-discrete fe
Examples-3-3-4 : (n : ℕ) → is-isolated (ι n)
Examples-3-3-4 = finite-isolated fe₀
Examples-3-3-5 : is-isolated ∞ ↔ WLPO
Examples-3-3-5 = is-isolated-gives-is-isolated' ∞ ,
is-isolated'-gives-is-isolated ∞
Examples-3-3-6 : is-embedding ι𝟙 × is-dense ι𝟙
Examples-3-3-6 = ι𝟙-is-embedding fe₀ , ι𝟙-dense fe₀
Lemma-3-4-1 : {X : 𝓤 ̇ } → is-discrete X → is-set X
Lemma-3-4-1 = discrete-types-are-sets
Lemma-3-4-2 : {X : 𝓤 ̇ } (x : X) → is-isolated x → is-h-isolated x
Lemma-3-4-2 = isolated-points-are-h-isolated
Lemma-3-4-3 : {X : 𝓤 ̇ } (x : X) → is-prop (is-isolated x)
Lemma-3-4-3 = being-isolated-is-prop fe
Lemma-3-4-3' : {X : 𝓤 ̇ } → is-prop (is-discrete X)
Lemma-3-4-3' = being-discrete-is-prop fe
Remark-3-5 : is-set ℕ∞
Remark-3-5 = ℕ∞-is-set fe₀
Proposition-3-6-1-inl : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (x : X)
→ is-isolated x → is-isolated (inl {𝓤} {𝓥} {X} {Y} x)
Proposition-3-6-1-inl = inl-is-isolated
Proposition-3-6-1-inr : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (y : Y)
→ is-isolated y → is-isolated (inr {𝓤} {𝓥} {X} {Y} y)
Proposition-3-6-1-inr = inr-is-isolated
Proposition-3-6-1-+ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-discrete X → is-discrete Y → is-discrete (X + Y)
Proposition-3-6-1-+ = +-is-discrete
Proposition-3-6-2 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ retract Y of X → is-discrete X → is-discrete Y
Proposition-3-6-2 = retract-is-discrete
Proposition-3-6-3 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-discrete X
→ ((x : X) → is-discrete (Y x))
→ is-discrete (Σ Y)
Proposition-3-6-3 = Σ-is-discrete
Proposition-3-6-4 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {x : X} {y : Y x}
→ is-isolated x
→ is-isolated y
→ is-isolated {_} {Σ Y} (x , y)
Proposition-3-6-4 = Σ-isolated
Proposition-3-6-4' : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {x : X} {y : Y x}
→ is-set X
→ is-isolated {_} {Σ Y} (x , y)
→ is-isolated y
Proposition-3-6-4' = Σ-isolated-right
Proposition-3-6-4'' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x : X} {y : Y}
→ is-isolated (x , y)
→ is-isolated x
Proposition-3-6-4'' = ×-isolated-left
Proposition-3-6-5 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ left-cancellable f
→ (x : X) → is-isolated (f x) → is-isolated x
Proposition-3-6-5 = lc-maps-reflect-isolatedness
Proposition-3-6-5' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-equiv f
→ (x : X) → is-isolated x → is-isolated (f x)
Proposition-3-6-5' = equivs-preserve-isolatedness
Proposition-3-7-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ has-two-distinct-points Y
→ is-discrete (X → Y)
→ is-decidable (is-empty X)
Proposition-3-7-1 =
discrete-exponential-has-decidable-emptiness-of-exponent fe'
Proposition-3-7-2 : {P : 𝓤 ̇ } {X : 𝓥 ̇ } (f : P → X)
→ is-prop P
→ ((p : P) → is-h-isolated (f p))
→ is-embedding f
Proposition-3-7-2 = maps-of-props-into-h-isolated-points-are-embeddings
Proposition-3-7-2' : {P : 𝓤 ̇ } {X : 𝓥 ̇ } (f : P → X)
→ is-prop P
→ ((p : P) → is-isolated (f p))
→ is-embedding f
Proposition-3-7-2' = maps-of-props-into-isolated-points-are-embeddings
Definition-3-8 : 𝓤 ̇ → 𝓤 ̇
Definition-3-8 = is-totally-separated
Lemma-3-9-1 : {X : 𝓤 ̇ } → is-discrete X → is-totally-separated X
Lemma-3-9-1 = discrete-types-are-totally-separated
Lemma-3-9-2 : (X : 𝓤 ̇ ) → is-totally-separated X → is-¬¬-separated X
Lemma-3-9-2 = totally-separated-types-are-¬¬-separated
Lemma-3-9-3 : (X : 𝓤 ̇ ) → is-totally-separated X → is-set X
Lemma-3-9-3 = totally-separated-types-are-sets fe'
Lemma-3-9-4 : (X : 𝓤 ̇ ) → is-prop (is-totally-separated X)
Lemma-3-9-4 {𝓤} = being-totally-separated-is-prop (fe 𝓤 𝓤)
\end{code}
The circle of Examples 3.10(1) is implemented as the type Tℤ of
ℤ-torsors of SyntheticHomotopyTheory.Circle.Construction. Its loop
space at the base point is ℤ, so it is not a set, and hence not
totally separated by Lemma 3.9 above.
Labels: Examples 3.10(1) = ex:tot-sep-failures(item:circle-not-tot-sep),
Lemma 3.9 = lem:tot-sep-basic.
\begin{code}
Examples-3-10-1 : ¬ is-set Tℤ
Examples-3-10-1 s = +disjoint (loops-are-a-proposition (inl ⋆) (inr (inl 0)))
where
loops-are-a-proposition = equiv-to-prop
(≃-sym loops-at-base-equivalent-to-ℤ)
(s {base-of-Tℤ} {base-of-Tℤ})
Examples-3-10-2 : is-¬¬-separated (Ω 𝓤) → EM 𝓤
Examples-3-10-2 {𝓤} = Ω-¬¬-separated-gives-EM (pe 𝓤) (fe 𝓤 𝓤)
Examples-3-10-2' : is-totally-separated (Ω 𝓤) → EM 𝓤
Examples-3-10-2' {𝓤} = Ω-totally-separated-gives-EM (pe 𝓤) fe'
Examples-3-10-3 : is-totally-separated ℕ∞₂ → ¬¬ WLPO
Examples-3-10-3 = ℕ∞₂-is-not-totally-separated-in-general
Examples-3-10-3-index : is-totally-separated ℕ∞
Examples-3-10-3-index = ℕ∞-is-totally-separated fe₀
Examples-3-10-3-fibers : (u : ℕ∞) → is-totally-separated (u ＝ ∞ → 𝟚)
Examples-3-10-3-fibers u = Π-is-totally-separated fe₀
(λ _ → 𝟚-is-totally-separated)
Proposition-3-11-12 : {X : 𝓤 ̇ }
→ is-totally-separated X ↔ is-totally-separated₁ X
Proposition-3-11-12 = totally-separated-gives-totally-separated₁ fe' ,
totally-separated₁-types-are-totally-separated
Proposition-3-11-13 : {X : 𝓤 ̇ }
→ is-totally-separated X ↔ is-totally-separated₂ X
Proposition-3-11-13 = totally-separated-gives-totally-separated₂ fe' ,
totally-separated₂-gives-totally-separated fe'
Proposition-3-11-14 : {X : 𝓤 ̇ }
→ is-totally-separated X ↔ is-totally-separated₃ X
Proposition-3-11-14 = totally-separated-gives-totally-separated₃ ,
totally-separated₃-gives-totally-separated
Prose-boolean-apartness : {X : 𝓤 ̇ } → X → X → 𝓤 ̇
Prose-boolean-apartness = _♯₂_
Prose-boolean-apartness' : {X : 𝓤 ̇ } → is-apartness (_♯₂_ {𝓤} {X})
Prose-boolean-apartness' = ♯₂-is-apartness
Proposition-3-12-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ retract Y of X
→ is-totally-separated X
→ is-totally-separated Y
Proposition-3-12-1 = retract-of-totally-separated
Proposition-3-12-1-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ X ≃ Y
→ is-totally-separated X
→ is-totally-separated Y
Proposition-3-12-1-equiv = equiv-to-totally-separated
Proposition-3-12-2 : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
→ is-totally-separated X
→ is-totally-separated Y
→ is-totally-separated (X × Y)
Proposition-3-12-2 = ×-totally-separated
Proposition-3-12-3 : (X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ )
→ is-discrete X
→ ((x : X) → is-totally-separated (Y x))
→ is-totally-separated (Σ Y)
Proposition-3-12-3 = Σ-is-totally-separated-if-index-type-is-discrete
Proposition-3-12-3-+ : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
→ is-totally-separated X
→ is-totally-separated Y
→ is-totally-separated (X + Y)
Proposition-3-12-3-+ = +-totally-separated
Proposition-3-12-4 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ ((x : X) → is-totally-separated (Y x))
→ is-totally-separated (Π Y)
Proposition-3-12-4 = Π-is-totally-separated fe'
Examples-3-13-2 : 𝓤₀ ̇ → 𝓤₁ ̇
Examples-3-13-2 = simple-type
Examples-3-13-2' : {X : 𝓤₀ ̇ } → simple-type X → is-totally-separated X
Examples-3-13-2' = simple-types-are-totally-separated
Examples-3-13-2'' : {X : 𝓤₀ ̇ } → simple-type X → retract ℕ of X
Examples-3-13-2'' = ℕ-is-retract-of-any-simple-type
Examples-3-13-2-pointed : {X : 𝓤₀ ̇ } → simple-type X → X
Examples-3-13-2-pointed = simple-types-pointed
Examples-3-13-2-r : {X A : 𝓤₀ ̇ }
→ retract A of ℕ → simple-type X → retract A of X
Examples-3-13-2-r = simple-types-r
Examples-3-13-2-r-step : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ }
→ X → retract A of Y → retract A of (X → Y)
Examples-3-13-2-r-step x =
retracts-compose (codomain-is-retract-of-function-space-with-pointed-domain x)
Examples-3-13-3 : is-discrete (ℕ → 𝟚) → WLPO
Examples-3-13-3 = ℕ∞-discrete-gives-WLPO ∘ retract-is-discrete (ℕ∞-retract-of-Cantor fe₀)
Lemma-3-14 : (A : ℕ∞ → 𝓥 ̇ )
→ ((u : ℕ∞) → is-totally-separated (A u))
→ is-prop (A ∞)
→ is-totally-separated (Σ A)
Lemma-3-14 = Σ-indexed-by-ℕ∞-is-totally-separated-if-family-at-∞-is-prop fe₀
Theorem-3-15 : 𝓤 ̇ → 𝓤 ̇
Theorem-3-15 = 𝕋
Theorem-3-15-ts : {X : 𝓤 ̇ } → is-totally-separated (𝕋 X)
Theorem-3-15-ts = 𝕋-is-totally-separated
Theorem-3-15-1 : {X : 𝓤 ̇ } → is-surjection (ηᵀ {𝓤} {X})
Theorem-3-15-1 = ηᵀ-is-surjection
Theorem-3-15-1' : {X : 𝓤 ̇ } (P : 𝕋 X → 𝓦 ̇ )
→ ((x' : 𝕋 X) → is-prop (P x'))
→ ((x : X) → P (ηᵀ x))
→ (x' : 𝕋 X) → P x'
Theorem-3-15-1' = ηᵀ-induction
Theorem-3-15-2 : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
→ is-totally-separated A
→ (f : X → A) → ∃! f̅ ꞉ (𝕋 X → A) , f̅ ∘ ηᵀ ＝ f
Theorem-3-15-2 = totally-separated-reflection
Theorem-3-15-2' : {X : 𝓤 ̇ } → (𝕋 X → 𝟚) ≃ (X → 𝟚)
Theorem-3-15-2' = totally-separated-reflection'' 𝟚-is-totally-separated
Theorem-3-15-3 : {X : 𝓤 ̇ } {x y : X} → ηᵀ x ＝ ηᵀ y → x ＝₂ y
Theorem-3-15-3 = ηᵀ-relates-identified-points
Theorem-3-15-3' : {X : 𝓤 ̇ } {x y : X} → x ＝₂ y → ηᵀ x ＝ ηᵀ y
Theorem-3-15-3' = ηᵀ-identifies-related-points
\end{code}
Section 4. Compactness
Labels: Section 4 = sec:compact-types-theory.
\begin{code}
Definition-4-1 : 𝓤 ̇ → 𝓤 ̇
Definition-4-1 = is-compact
Definition-4-1-∃ : 𝓤 ̇ → 𝓤 ̇
Definition-4-1-∃ = is-∃-compact
Definition-4-1-Π : 𝓤 ̇ → 𝓤 ̇
Definition-4-1-Π = is-Π-compact
Lemma-4-2 : {X : 𝓤 ̇ } → is-compact X → is-Compact X {𝓥}
Lemma-4-2 = compact-types-are-Compact
Lemma-4-2' : {X : 𝓤 ̇ } → is-Compact X {𝓤₀} → is-compact X
Lemma-4-2' = Compact-types-are-compact
Lemma-4-3 : (X : 𝓤 ̇ ) → is-compact X → is-decidable X
Lemma-4-3 = compact-types-are-decidable
Lemma-4-3' : (X : 𝓤 ̇ ) → is-prop X → is-decidable X → is-compact X
Lemma-4-3' = decidable-propositions-are-compact
Proposition-4-4 : ((X : 𝓤 ̇ ) → is-Compact X {𝓤}) → Global-Choice 𝓤
Proposition-4-4 = all-types-compact-gives-global-choice
Proposition-4-4' : Global-Choice 𝓤 → ((X : 𝓤 ̇ ) → is-Compact X {𝓤})
Proposition-4-4' = global-choice-gives-all-types-compact
Prose-global-choice-univalence : Global-Choice (𝓤 ⁺) → is-univalent 𝓤 → 𝟘
Prose-global-choice-univalence = Global-Choice-is-inconsistent-with-univalence
Examples-4-5-1-Fin : ℕ → 𝓤₀ ̇
Examples-4-5-1-Fin = Fin
Examples-4-5-1 : {n : ℕ} → is-Compact (Fin n) {𝓤}
Examples-4-5-1 = Fin-Compact
Examples-4-5-2 : is-compact ℕ ↔ LPO
Examples-4-5-2 = compact-ℕ-gives-LPO fe₀ , LPO-gives-compact-ℕ fe₀
Examples-4-5-3 : is-∃-compact ℕ ↔ LPO
Examples-4-5-3 = ∃-compact-ℕ-gives-LPO , LPO-gives-∃-compact-ℕ
Examples-4-5-4 : is-Π-compact ℕ ↔ WLPO
Examples-4-5-4 = Π-compact-ℕ-gives-WLPO , WLPO-gives-Π-compact-ℕ
Lemma-4-6-1 : {X : 𝓤 ̇ } → is-compact∙ X → is-compact X
Lemma-4-6-1 = compact∙-types-are-compact
Lemma-4-6-1' : {X : 𝓤 ̇ } → is-compact∙ X → X
Lemma-4-6-1' = compact∙-types-are-pointed
Lemma-4-6-2 : {X : 𝓤 ̇ } → is-compact X → X → is-compact∙ X
Lemma-4-6-2 = compact-pointed-types-are-compact∙
Examples-4-7-1 : is-compact∙ 𝟚
Examples-4-7-1 = 𝟚-is-compact∙
Examples-4-7-2 : is-compact∙ (Ω 𝓤)
Examples-4-7-2 {𝓤} = Ω-is-compact∙ (fe 𝓤 𝓤) (pe 𝓤)
Examples-4-7-3 : is-compact∙ ℕ∞
Examples-4-7-3 = ℕ∞-compact∙
Theorem-4-8-1-𝟘 : is-Compact (𝟘 {𝓤}) {𝓥}
Theorem-4-8-1-𝟘 = 𝟘-is-Compact
Theorem-4-8-1-𝟙 : is-Compact (𝟙 {𝓤}) {𝓥}
Theorem-4-8-1-𝟙 = 𝟙-is-Compact
Theorem-4-8-1-singleton : {X : 𝓤 ̇ } → is-singleton X → is-Compact X {𝓥}
Theorem-4-8-1-singleton = singletons-are-Compact
Theorem-4-8-2 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-Compact X {𝓦} → is-Compact Y {𝓦} → is-Compact (X + Y) {𝓦}
Theorem-4-8-2 = +-is-Compact
Theorem-4-8-3 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-Compact X {𝓥 ⊔ 𝓦}
→ ((x : X) → is-Compact (Y x) {𝓦})
→ is-Compact (Σ Y) {𝓦}
Theorem-4-8-3 = Σ-is-Compact
Theorem-4-8-4 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ retract Y of X → is-Compact X {𝓦} → is-Compact Y {𝓦}
Theorem-4-8-4 = Compact-closed-under-retracts
Theorem-4-8-5 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ funext 𝓥 𝓤₀
→ is-surjection f
→ is-Compact X {𝓥}
→ is-Compact Y {𝓥}
Theorem-4-8-5 = surjection-Compact
Theorem-4-8-5' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-Compact X {𝓤 ⊔ 𝓥}
→ is-Compact (image f) {𝓤 ⊔ 𝓥}
Theorem-4-8-5' = image-Compact fe'
Proposition-4-9 : {X : 𝓤 ̇ } → is-Compact X {𝓤} → is-Compact (𝕋 X) {𝓤}
Proposition-4-9 = surjection-Compact ηᵀ fe' ηᵀ-is-surjection
Corollary-4-10-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ retract Y Of X → is-compact∙ X → is-compact∙ Y
Corollary-4-10-1 = retract-is-compact∙
Corollary-4-10-1' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ X ≃ Y → is-compact∙ X → is-compact∙ Y
Corollary-4-10-1' = compact∙-types-are-closed-under-equiv
Corollary-4-10-2 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-compact∙ X
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ (Σ Y)
Corollary-4-10-2 = Σ-is-compact∙
Corollary-4-10-2-× : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-compact∙ X → is-compact∙ Y → is-compact∙ (X × Y)
Corollary-4-10-2-× = ×-is-compact∙
Corollary-4-10-2-+ : {X₀ X₁ : 𝓤 ̇ }
→ is-compact∙ X₀ → is-compact∙ X₁ → is-compact∙ (X₀ + X₁)
Corollary-4-10-2-+ = +-is-compact∙
Corollary-4-10-3 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-surjection f → is-compact∙ X → is-compact∙ Y
Corollary-4-10-3 = codomain-of-surjection-is-compact∙ pt
Corollary-4-10-3' : {X Y : 𝓤₀ ̇ } (f : X → Y)
→ is-compact∙ X → is-compact∙ (image f)
Corollary-4-10-3' = image-is-compact∙ pt
Proposition-4-11-1 : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
→ is-Compact X {𝓥 ⊔ 𝓦}
→ is-complemented A
→ ((x : X) → is-prop (A x))
→ is-Compact (Σ x ꞉ X , A x) {𝓦}
Proposition-4-11-1 = complemented-subset-of-compact-type
Proposition-4-11-2 : (X : 𝓤 ̇ ) (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ )
→ is-compact X
→ ((x : X) → A x + B x)
→ (Σ x ꞉ X , A x) + (Π x ꞉ X , B x)
Proposition-4-11-2 = compact-gives-Σ+Π
Proposition-4-11-3 : {X : 𝓤 ̇ } → is-Σ-Compact X {𝓥} → Complemented-choice X {𝓥}
Proposition-4-11-3 = Σ-Compactness-gives-Complemented-choice
\end{code}
Remark 4.12 records that the compactness of the Cantor type is
independent of our type theory, holding in the topological topos and
in the Kleene--Vesley topos and failing in the effective topos. This
is a statement about models rather than a theorem of our type theory,
so it has no entry. What it says about finite products is Theorem 4.8(3).
Labels: Remark 4.12 = rem:tychonoff-independence,
Theorem 4.8(3) = thm:compact-closure(item:compact-sigma).
The paragraph after Remark 4.12 claims that the Brouwerian principle
that all maps of the Cantor type into a discrete type are uniformly
continuous makes the Cantor type compact. The paper does not adopt
this principle, and so the claim takes it as a hypothesis. The two
primed entries are the notions of modulus of uniform continuity and of
uniform continuity that the paragraph defines.
Labels: Remark 4.12 = rem:tychonoff-independence.
\begin{code}
Prose-uniform-continuity-gives-cantor-compact
: ((N : 𝓤₀ ̇ ) (d : is-discrete N) (p : 𝟚ᴺ → N)
→ notions-of-continuity.uniformly-continuous N d p)
→ (p : 𝟚ᴺ → 𝟚) → is-decidable (Σ α ꞉ 𝟚ᴺ , p α ＝ ₀)
Prose-uniform-continuity-gives-cantor-compact ucp p
= having-root-is-decidable p (ucp 𝟚 𝟚-is-discrete p)
Prose-uniform-continuity-gives-cantor-compact'
: (N : 𝓤 ̇ ) → is-discrete N → ℕ → (𝟚ᴺ → N) → 𝓤 ̇
Prose-uniform-continuity-gives-cantor-compact' N d
= notions-of-continuity._is-a-modulus-of-uc-of_ N d
Prose-uniform-continuity-gives-cantor-compact''
: (N : 𝓤 ̇ ) → is-discrete N → (𝟚ᴺ → N) → 𝓤 ̇
Prose-uniform-continuity-gives-cantor-compact'' N d
= notions-of-continuity.uniformly-continuous N d
Proposition-4-13 : (p : 𝟚ᴺ → 𝟚)
→ uniformly-continuous p
→ Σ α₀ ꞉ 𝟚ᴺ , (p α₀ ＝ ₁ → (α : 𝟚ᴺ) → p α ＝ ₁)
Proposition-4-13 = Cantor-uniformly-searchable
Proposition-4-13' : (p : 𝟚ᴺ → 𝟚)
→ uniformly-continuous p
→ is-decidable (Σ α ꞉ 𝟚ᴺ , p α ＝ ₀)
Proposition-4-13' = having-root-is-decidable
Proposition-4-14-1 : {X : 𝓤 ̇ } → is-prop (is-∃-compact X)
Proposition-4-14-1 = ∃-compactness-is-prop
Proposition-4-14-1' : {X : 𝓤 ̇ } → is-prop (is-Π-compact X)
Proposition-4-14-1' = Π-compactness-is-prop
Proposition-4-14-2 : {X : 𝓤 ̇ } → is-compact X → is-∃-compact X
Proposition-4-14-2 = compact-types-are-∃-compact
Proposition-4-14-3 : {X : 𝓤 ̇ } → is-∃-compact X → is-Π-compact X
Proposition-4-14-3 = ∃-compact-types-are-Π-compact
Proposition-4-14-4
: {X : 𝓤 ̇ }
→ is-∃-compact X
→ (p : X → 𝟚) → ¬¬ (∃ x ꞉ X , p x ＝ ₀) → ∃ x ꞉ X , p x ＝ ₀
Proposition-4-14-4 = ∃-compactness-gives-Markov
Proposition-4-14-5 : {X : 𝓤 ̇ } → is-Π-compact' X → is-Π-compact X
Proposition-4-14-5 = Π-compact'-types-are-Π-compact
Proposition-4-14-5' : {X : 𝓤 ̇ } → is-Π-compact X → is-Π-compact' X
Proposition-4-14-5' = Π-compact-types-are-Π-compact'
Proposition-4-14-6 : (X : 𝓤 ̇ ) → is-∃-compact X ↔ is-∃-compact (𝕋 X)
Proposition-4-14-6 X = ∃-compact-types-are-∃-compact-𝕋 X ,
∃-compact-𝕋-types-are-∃-compact X
Proposition-4-14-6' : (X : 𝓤 ̇ ) → is-Π-compact X ↔ is-Π-compact (𝕋 X)
Proposition-4-14-6' X = Π-compact-types-are-Π-compact-𝕋 X ,
Π-compact-𝕋-types-are-Π-compact X
Proposition-4-15-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-surjection f → is-∃-compact X → is-∃-compact Y
Proposition-4-15-1 = codomain-of-surjection-is-∃-compact
Proposition-4-15-1' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-surjection f → is-Π-compact X → is-Π-compact Y
Proposition-4-15-1' = codomain-of-surjection-is-Π-compact
Proposition-4-15-2 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-Π-compact X
→ ((x : X) → is-Π-compact (Y x))
→ is-Π-compact (Σ Y)
Proposition-4-15-2 = Π-compact-closed-under-Σ
Proposition-4-15-3 : {X : 𝓤 ̇ } (A : X → 𝟚)
→ is-∃-compact X → is-∃-compact (Σ x ꞉ X , A x ＝ ₀)
Proposition-4-15-3 = detachable-subset-∃-compact
Proposition-4-15-3' : {X : 𝓤 ̇ } (A : X → 𝟚)
→ is-Π-compact X → is-Π-compact (Σ x ꞉ X , A x ＝ ₁)
Proposition-4-15-3' = complemented-subtype-is-Π-compact
Proposition-4-16-1 : (X : 𝓤 ̇ ) → is-prop X → is-∃-compact X → is-decidable X
Proposition-4-16-1 = ∃-compact-propositions-are-decidable
Proposition-4-16-1' : (X : 𝓤 ̇ ) → is-prop X → is-decidable X → is-∃-compact X
Proposition-4-16-1' = decidable-propositions-are-∃-compact
Proposition-4-16-2 : {X : 𝓤 ̇ } → is-∃-compact X → is-decidable ∥ X ∥
Proposition-4-16-2 = ∃-compact-types-have-decidable-support
Proposition-4-16-3 : {X : 𝓤 ̇ } → is-∃-compact X → ¬¬ X → ∥ X ∥
Proposition-4-16-3 = ∃-compact-non-empty-types-are-inhabited
Proposition-4-16-4 : (X : 𝓤 ̇ ) → is-Π-compact X → is-decidable (¬ X)
Proposition-4-16-4 = negations-of-Π-compact-types-are-decidable
Proposition-4-17 : 𝓤 ̇ → 𝓤 ̇
Proposition-4-17 = is-∃-compact∙
Proposition-4-17-12 : {X : 𝓤 ̇ } → is-∃-compact∙ X → ∥ X ∥ × is-∃-compact X
Proposition-4-17-12 = ∃-compact∙-types-are-inhabited-and-compact
Proposition-4-17-21 : {X : 𝓤 ̇ } → ∥ X ∥ × is-∃-compact X → is-∃-compact∙ X
Proposition-4-17-21 = inhabited-and-compact-types-are-∃-compact∙
Proposition-4-17-empty : {X : 𝓤 ̇ }
→ is-∃-compact X → is-∃-compact∙ X + is-empty X
Proposition-4-17-empty = ∃-compact-types-are-∃-compact∙-or-empty
Proposition-4-17-empty' : {X : 𝓤 ̇ }
→ is-∃-compact∙ X + is-empty X → is-∃-compact X
Proposition-4-17-empty' = ∃-compact∙-or-empty-types-are-∃-compact
Proposition-4-18 : {X : 𝓤 ̇ } → is-Π-compact X → has-infs X
Proposition-4-18 = Π-compact-has-infs
Proposition-4-18' : {X : 𝓤 ̇ } → has-infs X → is-Π-compact X
Proposition-4-18' = has-infs-Π-compact
Prose-right-adjoint-characterization
: {X : 𝓤 ̇ } (A : (X → 𝟚) → 𝟚)
→ Κ⊣ A ↔ ((p : X → 𝟚) → A p ＝ ₁ ↔ p ＝ (λ x → ₁))
Prose-right-adjoint-characterization = Κ⊣-charac
Prose-right-adjoint-characterization'
: {X : 𝓤 ̇ } → is-Π-compact X ↔ (Σ A ꞉ ((X → 𝟚) → 𝟚) , Κ⊣ A)
Prose-right-adjoint-characterization' = Π-compact-iff-Κ-has-right-adjoint
Proposition-4-19 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
Proposition-4-19 = is-clopen-map
Proposition-4-19-clopen
: (X : 𝓤 ̇ )
→ is-∃-compact X
→ ({𝓥 : Universe} (A : 𝓥 ̇ ) → is-clopen-map (fst A X))
Proposition-4-19-clopen = ∃-compact-clopen-projections
Proposition-4-19-clopen'
: (X : 𝓤 ̇ )
→ ({𝓥 : Universe} (A : 𝓥 ̇ ) → is-clopen-map (fst A X))
→ is-∃-compact X
Proposition-4-19-clopen' {𝓤} = clopen-projections-∃-compact {𝓤} {𝓤₀}
Lemma-4-20 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {x : X} {y : Y x}
→ ((x : X) → is-Compact (Y x) {𝓤 ⊔ 𝓥})
→ is-isolated (x , y) → is-isolated x
Lemma-4-20 = Σ-isolated-left
Proposition-4-21-1 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-Π-compact X
→ ((x : X) → is-discrete (Y x))
→ is-discrete ((x : X) → Y x)
Proposition-4-21-1 = discrete-to-power-Compact-is-discrete' (fe _ _)
∘ Π-compact-types-are-Π-Compact
Proposition-4-21-2 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-compact X
→ ((x : X) → is-discrete (Y x))
→ (f g : (x : X) → Y x) → (f ♯ g) + (f ＝ g)
Proposition-4-21-2 = apart-or-equal (fe _ _)
Examples-4-22-1 : is-discrete (ℕ∞ → 𝟚)
Examples-4-22-1 = ℕ∞→𝟚-is-discrete
Examples-4-22-1' : is-discrete (ℕ∞ → ℕ)
Examples-4-22-1' = ℕ∞→ℕ-is-discrete
Examples-4-22-2 : WLPO → is-discrete (ℕ → 𝟚)
Examples-4-22-2 wlpo = discrete-to-power-Π-compact-is-discrete
(WLPO-gives-Π-compact-ℕ wlpo) 𝟚-is-discrete
Definition-4-23 : 𝓤 ̇ → 𝓤 ̇
Definition-4-23 = is-disconnected
Proposition-4-24 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-disconnected Y
→ is-discrete (X → Y)
→ is-Π-compact X
Proposition-4-24 = discrete-power-of-disconnected-gives-compact-exponent
Proposition-4-24' : {X : 𝓤 ̇ } → is-discrete (X → 𝟚) → is-Π-compact X
Proposition-4-24' = power-of-two-discrete-gives-compact-exponent
Proposition-4-25-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-totally-separated X
→ is-disconnected Y
→ is-Π-compact (X → Y)
→ is-discrete X
Proposition-4-25-1 = tscd₀
Proposition-4-25-1' : {X : 𝓤 ̇ }
→ is-totally-separated X
→ is-Π-compact (X → 𝟚)
→ is-discrete X
Proposition-4-25-1' = tscd
Proposition-4-25-2 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-disconnected Y
→ is-Π-compact (X → Y)
→ is-discrete (𝕋 X)
Proposition-4-25-2 = tscd₁
Examples-4-26-1 : {X : 𝓤₀ ̇ }
→ simple-type X → is-Π-compact X → is-Π-compact ℕ
Examples-4-26-1 = stcwlpo'
Examples-4-26-2 : is-Π-compact (ℕ∞ → 𝟚) → WLPO
Examples-4-26-2 = [ℕ∞→𝟚]-compact-implies-WLPO
Theorem-4-27 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-prop X
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ (Π Y)
Theorem-4-27 = micro-tychonoff fe'
Prose-micro-tychonoff-constant-family
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ is-prop X
→ (X → is-compact∙ Y)
→ is-compact∙ (X → Y)
Prose-micro-tychonoff-constant-family i c
= micro-tychonoff fe' i c
Example-4-28 : is-compact∙ (LPO → ℕ)
Example-4-28 = [LPO→ℕ]-is-compact∙ fe₀
Remark-4-29-2 : ((X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ )
→ is-prop X
→ ((x : X) → is-compact (Y x))
→ is-compact (Π Y))
→ WEM 𝓤
Remark-4-29-2 = compact-micro-tychonoff-gives-WEM
Corollary-4-30 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ (n : ℕ)
→ X ↪ Fin n
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ (Π Y)
Corollary-4-30 = subfinite-tychonoff fe' fe'
Definition-4-31 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (X → 𝓦 ̇ ) → (X → Y) → (Y → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇ )
Definition-4-31 = Π-extension
Lemma-4-32-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → 𝓦 ̇ ) (j : X → Y)
→ is-embedding j
→ (x : X) → Π-extension f j (j x) ≃ f x
Lemma-4-32-1 = Π-extension-property
Lemma-4-32-2 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → 𝓦 ̇ ) (j : X → Y) (y : Y)
→ ((x : X) → j x ≠ y)
→ Π-extension f j y ≃ 𝟙 {𝓣}
Lemma-4-32-2 f j = Π-extension-out-of-range f j
Theorem-4-33 : {X : 𝓤 ̇ } {K : 𝓥 ̇ } {Y : X → 𝓦 ̇ } (j : X → K)
→ is-embedding j
→ ((x : X) → is-compact∙ (Y x))
→ is-compact∙ K
→ is-compact∙ (Σ (Y / j))
Theorem-4-33 = extended-sum-compact∙
Lemma-4-35 : {X : 𝓤 ̇ } {A : 𝓥 ̇ } (j : X → A) (Y : X → 𝓦 ̇ )
→ ((x : X) → is-totally-separated (Y x))
→ (a : A) → is-totally-separated ((Y / j) a)
Lemma-4-35 = /-is-totally-separated fe
Lemma-4-36-1 : {X : 𝓤 ̇ } {K : 𝓥 ̇ } (Y Z : X → 𝓦 ̇ ) (j : X → K)
→ ((x : X) → retract (Y x) of (Z x))
→ (k : K) → retract ((Y / j) k) of ((Z / j) k)
Lemma-4-36-1 = retract-extension
Lemma-4-36-2 : {X : 𝓤 ̇ } {K : 𝓥 ̇ } (Y Z : X → 𝓦 ̇ ) (j : X → K)
→ ((x : X) → retract (Y x) of (Z x))
→ retract (Σ (Y / j)) of (Σ (Z / j))
Lemma-4-36-2 Y₀ Y₁ j ρ = Σ-retract (Y₀ / j) (Y₁ / j)
(retract-extension Y₀ Y₁ j ρ)
Lemma-4-37-1 : Σ¹ (λ (_ : ℕ) → Cantor) ＝ (Σ u ꞉ ℕ∞ , (is-finite u → Cantor))
Lemma-4-37-1 = refl
Lemma-4-37-2 : 𝔻 Cantor ≃ Cantor
Lemma-4-37-2 = 𝔻-Cantor-≃-Cantor
Remark-4-38 : {X : 𝓤 ̇ } (c : X → 𝔻 X) → ∃! (is-Cantor-𝔻-coalgebra-map c)
Remark-4-38 = Cantor-is-final-𝔻-coalgebra
Remark-4-38' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (k : Y → X + Y)
→ ∃! (is-𝔻-coalgebra-map k)
Remark-4-38' = 𝔻-is-final-coalgebra
Example-4-39 : (k : ℕ) → is-compact∙ (𝔹 k)
Example-4-39 = 𝔹-is-compact∙
Example-4-39' : (k : ℕ) → is-totally-separated (𝔹 k)
Example-4-39' = 𝔹-is-totally-separated
\end{code}
Section 5. Ordinals and their arithmetic
Labels: Section 5 = sec:ordinals-prelim.
\begin{code}
Lemma-5-1 : {X : 𝓤 ̇ } (_<_ : X → X → 𝓥 ̇ )
→ is-well-founded _<_
→ is-Well-founded _<_ {𝓦}
Lemma-5-1 _<_ w = transfinite-induction _<_ w
Lemma-5-1-converse : {X : 𝓤 ̇ } (_<_ : X → X → 𝓥 ̇ )
→ is-Well-founded _<_ {𝓤 ⊔ 𝓥}
→ is-well-founded _<_
Lemma-5-1-converse _<_ = transfinite-induction-converse _<_
Prose-ordinal-well-order : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-well-order = is-well-order
Prose-ordinal-well-order-Ordinal : (𝓤 : Universe) → 𝓤 ⁺ ̇
Prose-ordinal-well-order-Ordinal = Ordinal
Lemma-5-2 : {X : 𝓤 ̇ } (_<_ : X → X → 𝓥 ̇ )
→ is-prop-valued _<_
→ is-extensional _<_
→ is-set X
Lemma-5-2 _<_ = extensionally-ordered-types-are-sets _<_ fe
Examples-5-3-ω : Ordinal 𝓤₀
Examples-5-3-ω = ω
Examples-5-3-prop-ordinal : (P : 𝓤 ̇ ) → is-prop P → Ordinal 𝓤
Examples-5-3-prop-ordinal = prop-ordinal
Examples-5-3-𝟘ₒ : Ordinal 𝓤
Examples-5-3-𝟘ₒ = 𝟘ₒ
Examples-5-3-𝟙ₒ : Ordinal 𝓤
Examples-5-3-𝟙ₒ = 𝟙ₒ
Examples-5-3-𝟚ₒ : Ordinal 𝓤
Examples-5-3-𝟚ₒ = 𝟚ₒ
Examples-5-3-Ωₒ : Ordinal 𝓤₁
Examples-5-3-Ωₒ = Ωₒ
Notation-5-4 : Ordinal 𝓤 → 𝓤 ̇
Notation-5-4 = ⟨_⟩
Prose-ordinal-of-ordinals : (𝓤 : Universe) → Ordinal (𝓤 ⁺)
Prose-ordinal-of-ordinals = OO
Prose-ordinal-of-ordinals-⊲ : Ordinal 𝓤 → Ordinal 𝓤 → 𝓤 ⁺ ̇
Prose-ordinal-of-ordinals-⊲ = _⊲_
Prose-ordinal-of-ordinals-↓ : (α : Ordinal 𝓤) → ⟨ α ⟩ → Ordinal 𝓤
Prose-ordinal-of-ordinals-↓ = _↓_
Prose-ordinal-of-ordinals-is-set : {𝓤 : Universe} → is-set (Ordinal 𝓤)
Prose-ordinal-of-ordinals-is-set {𝓤} = underlying-type-is-set fe (OO 𝓤)
Prose-ordinal-of-ordinals-↓-preserves-order
: (α : Ordinal 𝓤) (a b : ⟨ α ⟩) → a ≺⟨ α ⟩ b → (α ↓ a) ⊲ (α ↓ b)
Prose-ordinal-of-ordinals-↓-preserves-order = ↓-preserves-order
Prose-ordinal-comparisons : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-comparisons = _⊴_
Prose-ordinal-comparisons-simulation
: (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-comparisons-simulation = is-simulation
Prose-ordinal-comparisons-order-preserving
: (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-comparisons-order-preserving = Ordinals.Maps.is-order-preserving
Prose-ordinal-comparisons-initial-segment
: (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-comparisons-initial-segment = Ordinals.Maps.is-initial-segment
Prose-ordinal-comparisons-⊲-gives-⊴ : (α β : Ordinal 𝓤) → α ⊲ β → α ⊴ β
Prose-ordinal-comparisons-⊲-gives-⊴ = ⊲-gives-⊴
Prose-ordinal-comparisons-⊲-⊴ : (α β γ : Ordinal 𝓤) → α ⊲ β → β ⊴ γ → α ⊲ γ
Prose-ordinal-comparisons-⊲-⊴ = ⊲-⊴-gives-⊲
Prose-ordinal-comparisons-at-most-one-simulation
: (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f f' : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-simulation α β f'
→ f ∼ f'
Prose-ordinal-comparisons-at-most-one-simulation =
Ordinals.Maps.at-most-one-simulation
Prose-ordinal-comparisons-⊴-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
→ is-prop (α ⊴ β)
Prose-ordinal-comparisons-⊴-is-prop = ⊴-is-prop-valued
Prose-ordinal-comparisons-≃ₒ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇
Prose-ordinal-comparisons-≃ₒ = _≃ₒ_
Prose-ordinal-comparisons-≃ₒ-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
→ is-prop (α ≃ₒ β)
Prose-ordinal-comparisons-≃ₒ-is-prop = ≃ₒ-is-prop-valued fe'
Lemma-5-5 : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-surjection f
→ is-order-equiv α β f
Lemma-5-5 = surjective-simulations-are-order-equivs pt fe
Definition-5-6 : Ordinal 𝓤 → 𝓤 ̇
Definition-5-6 = is-trichotomous
Definition-5-6-Ordinal₃ : (𝓤 : Universe) → 𝓤 ⁺ ̇
Definition-5-6-Ordinal₃ = Ordinal₃
Remark-5-7 : {X : 𝓤 ̇ } (_<_ : X → X → 𝓥 ̇ )
→ excluded-middle 𝓥
→ is-well-order _<_
→ is-trichotomous-order _<_
Remark-5-7 = trichotomy₃
Remark-5-7' : funext 𝓤 𝓤₀
→ Every-Discrete-Ordinal-Is-Trichotomous 𝓤
→ EM 𝓤
Remark-5-7' = EM-if-Every-Discrete-Ordinal-Is-Trichotomous
Lemma-5-8 : {X : 𝓤 ̇ } (_<_ : X → X → 𝓥 ̇ )
→ is-well-founded _<_
→ is-trichotomous-order _<_
→ is-discrete X
Lemma-5-8 = trichotomous-gives-discrete
Definition-5-9 : Ordinal 𝓤 → Ordinal 𝓤 → Ordinal 𝓤
Definition-5-9 = _+ₒ_
Lemma-5-10 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ ) (_≺_ : Y → Y → 𝓦 ̇ )
→ is-well-order _<_
→ is-well-order _≺_
→ is-well-order (plus.order _<_ _≺_)
Lemma-5-10 = plus.well-order
Definition-5-11 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ (X → X → 𝓦 ̇ )
→ ({x : X} → Y x → Y x → 𝓣 ̇ )
→ (Σ Y → Σ Y → 𝓤 ⊔ 𝓦 ⊔ 𝓣 ̇ )
Definition-5-11 = slex-order
Lemma-5-12-prop-valued
: {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ )
(_≺_ : {x : X} → Y x → Y x → 𝓣 ̇ )
→ is-prop-valued _<_
→ is-well-founded _<_
→ is-extensional _<_
→ ((x : X) → is-prop-valued (_≺_ {x}))
→ is-prop-valued (sum.order _<_ _≺_)
Lemma-5-12-prop-valued _<_ _≺_ = sum.prop-valued _<_ _≺_ fe
Lemma-5-12-transitive
: {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ )
(_≺_ : {x : X} → Y x → Y x → 𝓣 ̇ )
→ is-transitive _<_
→ ((x : X) → is-transitive (_≺_ {x}))
→ is-transitive (sum.order _<_ _≺_)
Lemma-5-12-transitive = sum.transitive
Lemma-5-12-well-founded
: {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ )
(_≺_ : {x : X} → Y x → Y x → 𝓣 ̇ )
→ is-well-founded _<_
→ ((x : X) → is-well-founded (_≺_ {x}))
→ is-well-founded (sum.order _<_ _≺_)
Lemma-5-12-well-founded = sum.well-founded
Lemma-5-12-extensional
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ ) (_≺_ : Y → Y → 𝓣 ̇ )
→ is-well-order _<_
→ is-well-order _≺_
→ is-well-order (times.order _<_ _≺_)
Lemma-5-12-extensional _<_ _≺_ = times.well-order _<_ _≺_ fe
Definition-5-13 : Ordinal 𝓤 → Ordinal 𝓥 → Ordinal (𝓤 ⊔ 𝓥)
Definition-5-13 = _×ₒ_
Lemma-5-14-1 : (τ υ : Ordᵀ) (A : ⟨ τ ⟩ → Ordᵀ) (B : ⟨ υ ⟩ → Ordᵀ)
(f : ⟨ τ ⟩ → ⟨ υ ⟩)
(g : (x : ⟨ τ ⟩) → ⟨ A x ⟩ → ⟨ B (f x) ⟩)
→ is-order-preserving τ υ f
→ ((x : ⟨ τ ⟩) → is-order-preserving (A x) (B (f x)) (g x))
→ is-order-preserving (∑ τ A) (∑ υ B) (pair-fun f g)
Lemma-5-14-1 = pair-fun-is-order-preserving
Lemma-5-14-2 : (τ υ : Ordᵀ) (A : ⟨ τ ⟩ → Ordᵀ) (B : ⟨ υ ⟩ → Ordᵀ)
(f : ⟨ τ ⟩ → ⟨ υ ⟩)
(g : (x : ⟨ τ ⟩) → ⟨ A x ⟩ → ⟨ B (f x) ⟩)
→ is-order-reflecting τ υ f
→ is-embedding f
→ ((x : ⟨ τ ⟩) → is-order-reflecting (A x) (B (f x)) (g x))
→ is-order-reflecting (∑ τ A) (∑ υ B) (pair-fun f g)
Lemma-5-14-2 = pair-fun-is-order-reflecting
Remark-5-15 : is-extensional _≺ˢ_ → EM 𝓤₀
Remark-5-15 = shulmans-taboo
Remark-5-15' : Extensionality-of-Ordinal-Indexed-Sums 𝓤₁ → EM 𝓤₀
Remark-5-15' = extensionality-of-ordinal-indexed-sums-gives-EM (pe 𝓤₀)
Lemma-5-16 : (τ : Ordinal₃ 𝓤) → (⟨ τ ⟩ → Ordinal₃ 𝓤) → Ordinal₃ 𝓤
Lemma-5-16 = ∑³
Definition-5-17 : (𝓤 : Universe) → 𝓤 ⁺ ̇
Definition-5-17 = Ordinalᵀ
Example-5-18 : ℕ∞ → ℕ∞ → 𝓤₀ ̇
Example-5-18 = _≺ℕ∞_
Example-5-18-ordinal : Ordinal 𝓤₀
Example-5-18-ordinal = ℕ∞ₒ
Example-5-18-topped : Ordinalᵀ 𝓤₀
Example-5-18-topped = ℕ∞ᵒ
Prose-topped-arithmetic : Ordinalᵀ 𝓤 → Ordinalᵀ 𝓤 → Ordinalᵀ 𝓤
Prose-topped-arithmetic = _+ᵒ_
Prose-topped-arithmetic' : Ordinalᵀ 𝓤 → Ordinalᵀ 𝓤 → Ordinalᵀ 𝓤
Prose-topped-arithmetic' = _×ᵒ_
Prose-trichotomous-arithmetic : Ordinal₃ 𝓤 → Ordinal₃ 𝓤 → Ordinal₃ 𝓤
Prose-trichotomous-arithmetic = _+₃_
Prose-trichotomous-arithmetic' : Ordinal₃ 𝓤 → Ordinal₃ 𝓤 → Ordinal₃ 𝓤
Prose-trichotomous-arithmetic' = _×₃_
Prose-trichotomous-arithmetic''
: (τ : Ordinal₃ 𝓤) → (⟨ τ ⟩ → Ordinal₃ 𝓤) → Ordinal₃ 𝓤
Prose-trichotomous-arithmetic'' = ∑³
\end{code}
That the sum of a topped-ordinal-indexed family of topped ordinals is
again topped is Lemma 5.19 below.
Labels: Lemma 5.19 = lem:topped-sum.
\begin{code}
Lemma-5-19 : (τ : Ordinalᵀ 𝓤) → (⟨ τ ⟩ → Ordinalᵀ 𝓤) → Ordinalᵀ 𝓤
Lemma-5-19 = ∑
Lemma-5-20 : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
→ (X → Ordinal 𝓦)
→ (X ↪ A)
→ (A → Ordinal (𝓤 ⊔ 𝓥 ⊔ 𝓦))
Lemma-5-20 = _↗_
Lemma-5-21 : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
→ (X → Ordinalᵀ 𝓦)
→ (X ↪ A)
→ (A → Ordinalᵀ (𝓤 ⊔ 𝓥 ⊔ 𝓦))
Lemma-5-21 = _↗ᵀ_
Lemma-5-22 : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
(α : X → Ordinal 𝓦)
(𝓮@(j , _) : X ↪ A)
(x : X)
→ (α ↗ 𝓮) (j x) ≃ₒ α x
Lemma-5-22 = ↗-propertyₒ
Lemma-5-22-ainjective : is-univalent (𝓤 ⊔ 𝓥)
→ ainjective-type (Ordinal (𝓤 ⊔ 𝓥)) 𝓤 𝓥
Lemma-5-22-ainjective = Ordinal-is-ainjective
Lemma-5-22-ainjective-TS : is-univalent (𝓤 ⊔ 𝓥)
→ ainjective-type (TSOrdinal (𝓤 ⊔ 𝓥)) 𝓤 𝓥
Lemma-5-22-ainjective-TS = TSOrdinal-is-ainjective fe
Prose-ordinals-are-ainjective : ainjective-type (Ordinal (𝓤 ⊔ 𝓥)) 𝓤 𝓥
Prose-ordinals-are-ainjective {𝓤} {𝓥} = Ordinal-is-ainjective (ua (𝓤 ⊔ 𝓥))
Prose-ordinals-are-ainjective' : ainjective-type (TSOrdinal (𝓤 ⊔ 𝓥)) 𝓤 𝓥
Prose-ordinals-are-ainjective' {𝓤} {𝓥} =
TSOrdinal-is-ainjective fe (ua (𝓤 ⊔ 𝓥))
Prose-ordinals-are-ainjective'' : (α β : Ordinal 𝓤) → α ≃ₒ β → α ＝ β
Prose-ordinals-are-ainjective'' {𝓤} = eqtoidₒ (ua 𝓤) fe'
Definition-5-23-1 : (ℕ → Ordᵀ) → Ordᵀ
Definition-5-23-1 = ∑¹
Definition-5-23-1-explicitly
: (X : ℕ → 𝓤 ̇ )
→ Σ¹ X ＝ (Σ u ꞉ ℕ∞ , ((φ : is-finite u) → X (size φ)))
Definition-5-23-1-explicitly = Σ¹-explicitly
Definition-5-23-1-compact∙ : (X : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → is-compact∙ (X n))
→ is-compact∙ (Σ¹ X)
Definition-5-23-1-compact∙ = Σ¹-compact∙
Definition-5-23-2 : (ℕ → Ordᵀ) → Ordᵀ
Definition-5-23-2 = ∑₁
Lemma-5-24-shape : (X : ℕ → 𝓤 ̇ ) → Σ₁ X ≃ (Σ n ꞉ ℕ , X n) + 𝟙 {𝓤}
Lemma-5-24-shape = Σ₁-explicitly
Lemma-5-24-shape-top : (τ : ℕ → Ordᵀ) → Σ₁-base (top (∑₁ τ)) ＝ inr ⋆
Lemma-5-24-shape-top = ∑₁-top-is-over-inr
Lemma-5-24-1 : (τ : ℕ → Ordᵀ) → [ ∑₁ τ ] ≃ₒ (∑ₒ ω τ +ₒ 𝟙ₒ)
Lemma-5-24-1 = ∑₁-is-successorₒ
Lemma-5-24-2 : {X : ℕ → 𝓤 ̇ }
→ ((n : ℕ) → retract (X n) of ℕ)
→ retract (Σ₁ X) of ℕ
Lemma-5-24-2 = Σ₁-ℕ-retract
Lemma-5-24-2-discrete : (X : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → is-discrete (X n))
→ is-discrete (Σ₁ X)
Lemma-5-24-2-discrete = Σ₁-is-discrete
Definition-5-25 : (X : ℕ → 𝓤 ̇ ) → Σ₁ X → Σ¹ X
Definition-5-25 = Σ-up
Definition-5-25-ordinals : (τ : ℕ → Ordᵀ) → ⟨ ∑₁ τ ⟩ → ⟨ ∑¹ τ ⟩
Definition-5-25-ordinals = ∑-up
Definition-5-25-lc : left-cancellable ι𝟙
Definition-5-25-lc = ι𝟙-lc
Lemma-5-26-embedding : (X : ℕ → 𝓤 ̇ ) → is-embedding (Σ-up X)
Lemma-5-26-embedding = Σ-up-embedding
Lemma-5-26-dense : (X : ℕ → 𝓤 ̇ ) → is-dense (Σ-up X)
Lemma-5-26-dense = Σ-up-dense
Lemma-5-26-order-preserving
: (τ : ℕ → Ordᵀ) → is-order-preserving (∑₁ τ) (∑¹ τ) (∑-up τ)
Lemma-5-26-order-preserving = ∑-up-is-order-preserving
Lemma-5-26-order-reflecting
: (τ : ℕ → Ordᵀ) → is-order-reflecting (∑₁ τ) (∑¹ τ) (∑-up τ)
Lemma-5-26-order-reflecting = ∑-up-is-order-reflecting
Theorem-5-27 : {I : 𝓤 ̇ } (α : I → Ordinal 𝓤)
→ (Σ i ꞉ I , ⟨ α i ⟩) → Ordinal 𝓤
Theorem-5-27 = sum-to-ordinals
Theorem-5-27-1 : {I : 𝓤 ̇ } → (I → Ordinal 𝓤) → Ordinal 𝓤
Theorem-5-27-1 = sup
Theorem-5-27-2 : {I : 𝓤 ̇ } (α : I → Ordinal 𝓤)
→ is-surjection (sum-to-sup α)
Theorem-5-27-2 = sum-to-sup-is-surjection
Theorem-5-27-3 : {I : 𝓤 ̇ } (α : I → Ordinal 𝓤) (i : I) → α i ⊴ sup α
Theorem-5-27-3 = sup-is-upper-bound
Theorem-5-27-3' : {I : 𝓤 ̇ } (α : I → Ordinal 𝓤) (β : Ordinal 𝓤)
→ ((i : I) → α i ⊴ β)
→ sup α ⊴ β
Theorem-5-27-3' = sup-is-lower-bound-of-upper-bounds
Theorem-5-27-3'' : {I : 𝓤 ̇ } (α : I → Ordinal 𝓤) (i : I) (x : ⟨ α i ⟩)
→ sup α ↓ [ α i , sup α ]⟨ sup-is-upper-bound α i ⟩ x
＝ α i ↓ x
Theorem-5-27-3'' = initial-segment-of-sup-at-component
Corollary-5-28 : {I : 𝓤 ̇ } {α : I → Ordinal 𝓤}
→ is-compact∙ I
→ ((i : I) → is-compact∙ ⟨ α i ⟩)
→ is-compact∙ ⟨ sup α ⟩
Corollary-5-28 = sup-is-compact∙ sr
Theorem-5-29 : {X K : 𝓤 ̇ } (𝓮@(j , _) : X ↪ K) (α : X → Ordinal 𝓤)
→ is-compact∙ K
→ ((x : X) → is-compact∙ ⟨ α x ⟩)
→ is-compact∙ ⟨ sup (α ↗ 𝓮) ⟩
Theorem-5-29 (j , j-is-embedding) α K-compact∙ α-compact∙ =
sup-is-compact∙ sr K-compact∙
(λ k → micro-tychonoff (fe _ _) (j-is-embedding k) (α-compact∙ ∘ pr₁))
Definition-5-30 : (ℕ → Ordinal 𝓤₀) → Ordinal 𝓤₀
Definition-5-30 α = sup (α ↗ embedding-ℕ-to-ℕ∞ fe₀)
\end{code}
Section 6. Ordinal codes
Labels: Section 6 = sec:brouwer-standard.
\begin{code}
Definition-6-1 : 𝓤₀ ̇
Definition-6-1 = B
Definition-6-1-recursion : {X : 𝓤 ̇ } → X → (X → X) → ((ℕ → X) → X) → B → X
Definition-6-1-recursion = B-rec
\end{code}
The paper denotes the interpretations with a descriptive subscript
recording how the limit constructor is read (sup for a supremum, Σ for
a sum), a superscript 1 for first extending the family along ℕ ↪ ℕ∞,
and a subscript 1 for first extending it along ℕ ↪ ℕ + 𝟙. The mixfix
names below match the paper's notation:
⟦_⟧-sup = ⟦_⟧₀ (the paper's sup)
⟦_⟧-Σ = ⟦_⟧₃ (the paper's Σ)
⟦_⟧-sup¹ = ⟦_⟧₂ (the paper's sup¹)
⟦_⟧-Σ₁ = BDC.Δ (the paper's Σ₁)
⟦_⟧-Σ¹ = ⟦_⟧₁ (the paper's Σ¹)
⟦_⟧-Σ' = BDC.Κ (again the paper's Σ¹, but redefined locally
in TypeTopology to avoid unnecessary assumptions)
Two of these, ⟦_⟧-Σ₁ and ⟦_⟧-Σ', come from a different module from the
other four, Ordinals.BrouwerCodesDiscreteAndCompactInterpretations,
where they are called Δ and Κ, the first of them Δ because it is the
discrete interpretation, and the second Κ because it is the compact
interpretation.
\begin{code}
⟦_⟧-sup : B → Ordinal 𝓤₀
⟦_⟧-sup = ⟦_⟧₀
⟦_⟧-Σ : B → Ordinal₃ 𝓤₀
⟦_⟧-Σ = ⟦_⟧₃
⟦_⟧-sup¹ : B → Ordinal 𝓤₀
⟦_⟧-sup¹ = ⟦_⟧₂
⟦_⟧-Σ₁ : B → Ordinalᵀ 𝓤₀
⟦_⟧-Σ₁ = BDC.Δ
⟦_⟧-Σ¹ : B → Ordinalᵀ 𝓤₀
⟦_⟧-Σ¹ = ⟦_⟧₁
⟦_⟧-Σ' : B → Ordinalᵀ 𝓤₀
⟦_⟧-Σ' = BDC.Κ
Definition-6-2 : B → Ordinal 𝓤₀
Definition-6-2 = ⟦_⟧-sup
Proposition-6-3 : ((b : B) → is-compact ⟨ ⟦ b ⟧-sup ⟩) → LPO
Proposition-6-3 = ⟦_⟧₀-compact-gives-LPO
Proposition-6-4 : ((b : B) → is-trichotomous ⟦ b ⟧-sup) → LPO
Proposition-6-4 = FTr.trichotomy-of-the-standard-interpretation-gives-LPO
\end{code}
The sharpened statement of Remark 6.5 is the following, in which the
code depends on the conatural number by a fixed recipe and trichotomy
is assumed of that code.
Labels: Remark 6.5 = rem:trichotomy-hypothesis-use.
\begin{code}
Remark-6-5 : (u : ℕ∞)
→ is-trichotomous ⟦ FTr.brouwer-code u ⟧-sup
→ is-decidable (is-finite u)
Remark-6-5 = FTr.main-lemma
Definition-6-6-Σ : B → Ordinal₃ 𝓤₀
Definition-6-6-Σ = ⟦_⟧-Σ
Definition-6-6-Σ¹ : B → Ordinalᵀ 𝓤₀
Definition-6-6-Σ¹ = ⟦_⟧-Σ¹
Definition-6-6-sup¹ : B → Ordinal 𝓤₀
Definition-6-6-sup¹ = ⟦_⟧-sup¹
Theorem-6-7-1 : (b : B) → is-trichotomous-order (underlying-order ⟦ b ⟧-Σ)
Theorem-6-7-1 b = 3is-trichotomous ⟦ b ⟧-Σ
Theorem-6-7-2 : (b : B) → is-compact∙ ⟨ ⟦ b ⟧-Σ¹ ⟩
Theorem-6-7-2 = ⟦_⟧₁-is-compact∙
Theorem-6-7-2' : (b : B) → is-totally-separated ⟨ ⟦ b ⟧-Σ¹ ⟩
Theorem-6-7-2' = ⟦_⟧₁-is-totally-separated
Theorem-6-7-3 : (b : B) → retract ⟨ ⟦ b ⟧-Σ' ⟩ of (ℕ → 𝟚)
Theorem-6-7-3 = BDC.Κ-Cantor-retract
Theorem-6-7-4 : (b : B) → is-compact∙ ⟨ ⟦ b ⟧-sup¹ ⟩
Theorem-6-7-4 = ⟦_⟧₂-is-compact∙
Prose-trichotomous-interpretation-is-discrete
: (b : B) → is-discrete ⟨ ⟦ b ⟧-Σ ⟩
Prose-trichotomous-interpretation-is-discrete = ⟦_⟧₃-is-discrete
Remark-6-8 : (X : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → is-totally-separated (X n))
→ is-totally-separated (Σ¹ X)
Remark-6-8 = Σ¹-is-totally-separated
Remark-6-8' : (A : ℕ∞ → 𝓥 ̇ )
→ ((u : ℕ∞) → is-totally-separated (A u))
→ is-prop (A ∞)
→ is-totally-separated (Σ A)
Remark-6-8'
= Σ-indexed-by-ℕ∞-is-totally-separated-if-family-at-∞-is-prop fe₀
Remark-6-8'' : (b : B) → is-totally-separated ⟨ ⟦ b ⟧-Σ' ⟩
Remark-6-8'' = BDC.Κ-is-totally-separated
Proposition-6-9 : ((b : B) → is-compact ⟨ ⟦ b ⟧-Σ ⟩) → LPO
Proposition-6-9 = ⟦_⟧₃-compact-gives-LPO
Proposition-6-10 : ((b : B) → is-totally-separated ⟨ ⟦ b ⟧-sup¹ ⟩) → ¬¬ WLPO
Proposition-6-10
= FTS.total-separatedness-of-the-sup-of-extension-interpretation-gives-¬¬WLPO
\end{code}
Examples 3.13(1) has no entry. That total separatedness is not closed
under sums is the example of Examples 3.10(3), whose index type and
fibers are totally separated by the two entries following
Examples-3-10-3 above. That it is not closed under surjective images
is Example 6.11 below.
Labels: Examples 3.13(1) = ex:tot-sep(item:ts-not-sigma),
Examples 3.10(3) = ex:tot-sep-failures(item:two-infinities-not-tot-sep),
Example 6.11 = ex:tot-sep-counterexample.
\begin{code}
Example-6-11 : Σ I ꞉ 𝓤₀ ̇ , Σ α ꞉ (I → Ordinal 𝓤₀) ,
is-compact∙ I
× is-totally-separated I
× ((i : I) → is-compact∙ ⟨ α i ⟩)
× ((i : I) → is-totally-separated ⟨ α i ⟩)
× (is-totally-separated ⟨ sup α ⟩ → ¬¬ WLPO)
Example-6-11 = FTS.counterexample-to-total-separatedness
Prose-extension-is-partial-boolean
: (u : ℕ∞) → ⟨ FTS.α̅ u ⟩ ＝ (is-finite u → 𝟚)
Prose-extension-is-partial-boolean u = refl
Definition-6-12 : 𝓤 ̇ → 𝓤 ̇
Definition-6-12 = FTS.is-semidecidable
Definition-6-12-𝕊 : 𝓤₁ ̇
Definition-6-12-𝕊 = FTS.𝕊
Definition-6-12-order : FTS.𝕊 → FTS.𝕊 → 𝓤₁ ̇
Definition-6-12-order = FTS._≺ₛ_
Definition-6-12-⊥ : FTS.𝕊
Definition-6-12-⊥ = FTS.⊥ₛ
Definition-6-12-⊤ : FTS.𝕊
Definition-6-12-⊤ = FTS.⊤ₛ
Definition-6-12-ordinal : Ordinal 𝓤₁
Definition-6-12-ordinal = FTS.𝓢
Lemma-6-13-prop-valued : is-prop-valued FTS._≺ₛ_
Lemma-6-13-prop-valued = FTS.≺ₛ-prop-valued
Lemma-6-13-transitive : is-transitive FTS._≺ₛ_
Lemma-6-13-transitive = FTS.≺ₛ-transitive
Lemma-6-13-extensional : is-extensional FTS._≺ₛ_
Lemma-6-13-extensional = FTS.≺ₛ-extensional
Lemma-6-13-well-founded : is-well-founded FTS._≺ₛ_
Lemma-6-13-well-founded = FTS.≺ₛ-well-founded
Lemma-6-13-identity : {t t' : FTS.𝕊}
→ (pr₁ t holds ↔ pr₁ t' holds)
→ t ＝ t'
Lemma-6-13-identity = FTS.to-𝕊-＝
Lemma-6-14 : FTS.𝓼 ≃ₒ FTS.𝓢
Lemma-6-14 = FTS.𝓼-is-𝓢
Lemma-6-14-small : is-small FTS.𝕊
Lemma-6-14-small = FTS.𝕊-is-small
Lemma-6-15 : (p : FTS.𝕊 → 𝟚) → p FTS.⊥ₛ ≠ p FTS.⊤ₛ → WLPO
Lemma-6-15 = FTS.𝕊-separation-gives-WLPO
Lemma-6-15' : is-totally-separated FTS.𝕊 → ¬¬ WLPO
Lemma-6-15' = FTS.𝕊-totally-separated-gives-¬¬WLPO
Theorem-6-16-₀₃ : Excluded-Middle → (b : B) → ⟦ b ⟧-sup ⊴ [ ⟦ b ⟧-Σ ]
Theorem-6-16-₀₃ = comparison₀₃
Theorem-6-16-₀₂ : EM 𝓤₁ → (b : B) → ⟦ b ⟧-sup ⊴ ⟦ b ⟧-sup¹
Theorem-6-16-₀₂ = comparison₀₂
Theorem-6-16-₂₁ : Excluded-Middle → (b : B) → ⟦ b ⟧-sup¹ ⊴ [ ⟦ b ⟧-Σ¹ ]
Theorem-6-16-₂₁ = comparison₂₁
Theorem-6-16-₃₁ : EM 𝓤₀ → (b : B) → [ ⟦ b ⟧-Σ ] ⊴ [ ⟦ b ⟧-Σ¹ ]
Theorem-6-16-₃₁ = comparison₃₁
Proposition-6-17-1 : ((b : B) → ⟦ b ⟧-sup ⊴ [ ⟦ b ⟧-Σ ]) → LPO
Proposition-6-17-1 = FTr.comparison₀₃-gives-LPO
Proposition-6-17-2 : ((b : B) → ⟦ b ⟧-sup¹ ⊴ [ ⟦ b ⟧-Σ¹ ]) → ¬¬ WLPO
Proposition-6-17-2 = FTS.comparison₂₁-gives-¬¬WLPO
\end{code}
Question 6.18, which is not formalizable, asks whether the remaining
two comparisons, comparison₀₂ and comparison₃₁ holding for every code,
imply a constructive taboo.
Labels: Question 6.18 = q:comparisons-taboos.
\begin{code}
Definition-6-19 : B → Ordᵀ
Definition-6-19 = ⟦_⟧-Σ₁
Theorem-6-20-1 : (b : B) → is-trichotomous [ ⟦ b ⟧-Σ₁ ]
Theorem-6-20-1 = BDC.Δ-is-trichotomous
Theorem-6-20-2 : (b : B) → retract ⟨ ⟦ b ⟧-Σ₁ ⟩ of ℕ
Theorem-6-20-2 = BDC.Δ-retract-of-ℕ
Theorem-6-20-2' : (b : B) → is-discrete ⟨ ⟦ b ⟧-Σ₁ ⟩
Theorem-6-20-2' = BDC.Δ-is-discrete
Proposition-6-21-1 : ((b : B) → is-compact ⟨ ⟦ b ⟧-Σ₁ ⟩) ↔ LPO
Proposition-6-21-1 = BDC.Δ-compact-iff-LPO
Proposition-6-21-2 : ((b : B) → is-discrete ⟨ ⟦ b ⟧-Σ' ⟩) → WLPO
Proposition-6-21-2 = BDC.Κ-discrete-gives-WLPO
Definition-6-22 : {b : B} → ⟨ ⟦ b ⟧-Σ₁ ⟩ → ⟨ ⟦ b ⟧-Σ' ⟩
Definition-6-22 {b} = BDC.ι {b}
Definition-6-22-limit-case : (X : ℕ → 𝓤 ̇ ) (Y : ℕ → 𝓤 ̇ )
→ ((n : ℕ) → X n → Y n)
→ Σ₁ X → Σ¹ Y
Definition-6-22-limit-case = Σ↑
Theorem-6-23-1 : (b : B) → is-embedding (BDC.ι {b})
Theorem-6-23-1 = BDC.ι-is-embedding
Theorem-6-23-2 : (b : B) → is-dense (BDC.ι {b})
Theorem-6-23-2 = BDC.ι-is-dense
Theorem-6-23-3 : (b : B) (x y : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ x ≺⟨ [ ⟦ b ⟧-Σ₁ ] ⟩ y
→ BDC.ι {b} x ≺⟨ [ ⟦ b ⟧-Σ' ] ⟩ BDC.ι {b} y
Theorem-6-23-3 = BDC.ι-is-order-preserving
Theorem-6-23-4 : (b : B) (x y : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ BDC.ι {b} x ≺⟨ [ ⟦ b ⟧-Σ' ] ⟩ BDC.ι {b} y
→ x ≺⟨ [ ⟦ b ⟧-Σ₁ ] ⟩ y
Theorem-6-23-4 = BDC.ι-is-order-reflecting
Example-6-24 : [ ∑₁ (λ _ → 𝟙ᵒ) ] ≃ₒ [ succₒ ω ]
Example-6-24 = ∑₁-of-𝟙ᵒ
Example-6-24' : [ ∑¹ (λ _ → 𝟙ᵒ) ] ≃ₒ [ ℕ∞ᵒ ]
Example-6-24' = ∑¹-of-𝟙ᵒ
Example-6-24'' : (τ : ℕ → Ordᵀ) → is-isolated (top (∑₁ τ))
Example-6-24'' = ∑₁-top-is-isolated
Proposition-6-25 : ((b : B) → is-equiv (BDC.ι {b})) ↔ LPO
Proposition-6-25 = BDC.ι-is-equiv-iff-LPO
Definition-6-26 : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Definition-6-26 = has-inf
Definition-6-26-1 : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → (X → 𝟚) → X → 𝓤 ̇
Definition-6-26-1 _≤_ = is-conditional-root _≤_
Definition-6-26-2 : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → (X → 𝟚) → X → 𝓤 ⊔ 𝓥 ̇
Definition-6-26-2 = is-roots-infimum
Definition-6-26-topped : Ordinalᵀ 𝓤 → 𝓤 ̇
Definition-6-26-topped = has-infs-of-complemented-subsets
Remark-6-27 : {X : 𝓤 ̇ } (_≤_ : X → X → 𝓥 ̇ ) → has-inf _≤_ → is-compact∙ X
Remark-6-27 = has-inf-gives-compact∙
Lemma-6-28 : {X : 𝓤 ̇ } (_≤_ : X → X → 𝓥 ̇ )
→ has-inf _≤_
→ (p : X → 𝟚)
→ ¬¬ (Σ x ꞉ X , p x ＝ ₀)
→ Σ x₀ ꞉ X , is-least-root _≤_ p x₀
Lemma-6-28 = has-inf-gives-least-root
Theorem-6-29 : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
→ is-prop X
→ (_≺_ : {x : X} → Y x → Y x → 𝓦 ̇ )
→ ((x : X) → has-inf (λ (y y' : Y x) → ¬ (y' ≺ y)))
→ has-inf (λ (φ γ : Π Y) → ¬ (Σ x ꞉ X , γ x ≺ φ x))
Theorem-6-29 = micro-inf-tychonoff
Theorem-6-30 : propext 𝓤₀
→ (b : B) → has-infs-of-complemented-subsets (⟦ b ⟧-Σ')
Theorem-6-30 = BDC.Κ-has-infs-of-complemented-subsets
Corollary-6-31 : propext 𝓤₀
→ (b : B) (p : ⟨ ⟦ b ⟧-Σ' ⟩ → 𝟚)
→ ¬¬ (Σ x ꞉ ⟨ ⟦ b ⟧-Σ' ⟩ , p x ＝ ₀)
→ Σ x₀ ꞉ ⟨ ⟦ b ⟧-Σ' ⟩ , is-least-root
(underlying-weak-order (⟦ b ⟧-Σ')) p x₀
Corollary-6-31 = BDC.Κ-has-least-roots-of-complemented-subsets
Proposition-6-32 : propext 𝓤₀
→ (((b : B) (p : ⟨ ⟦ b ⟧-Σ₁ ⟩ → 𝟚)
→ ¬¬ (Σ x ꞉ ⟨ ⟦ b ⟧-Σ₁ ⟩ , p x ＝ ₀)
→ Σ x₀ ꞉ ⟨ ⟦ b ⟧-Σ₁ ⟩ , is-least-root
(underlying-weak-order (⟦ b ⟧-Σ₁)) p x₀)
↔ LPO)
Proposition-6-32 = BDC.Δ-least-roots-iff-LPO
Remark-6-33 : ((p : ⟨ ⟦ (L (λ _ → Z)) ⟧-Σ₁ ⟩ → 𝟚)
→ ¬¬ (Σ x ꞉ ⟨ ⟦ (L (λ _ → Z)) ⟧-Σ₁ ⟩ , p x ＝ ₀)
→ Σ x₀ ꞉ ⟨ ⟦ (L (λ _ → Z)) ⟧-Σ₁ ⟩ ,
is-least-root
(underlying-weak-order (⟦ (L (λ _ → Z)) ⟧-Σ₁)) p x₀)
→ LPO
Remark-6-33 = BDC.Δ𝟙-least-roots-gives-LPO
\end{code}
Section 7. Codes defined by induction-recursion
Labels: Section 7 = sec:inductive-recursive.
\begin{code}
Definition-7-1 : 𝓤₀ ̇
Definition-7-1 = IRC.E
Definition-7-1-Δ : IRC.E → Ordᵀ
Definition-7-1-Δ = IRC.Δ
Theorem-7-2 : (ν : IRC.E) → retract ⟨ IRC.Δ ν ⟩ of ℕ
Theorem-7-2 = IRC.Δ-retract-of-ℕ
Theorem-7-2-discrete : (ν : IRC.E) → is-discrete ⟨ IRC.Δ ν ⟩
Theorem-7-2-discrete = IRC.Δ-is-discrete
Theorem-7-2-trichotomous : (ν : IRC.E) → is-trichotomous [ IRC.Δ ν ]
Theorem-7-2-trichotomous = IRC.Δ-is-trichotomous
Proposition-7-3 : ((ν : IRC.E) → is-compact ⟨ IRC.Δ ν ⟩) ↔ LPO
Proposition-7-3 = IRC.Δ-compact-iff-LPO
Definition-7-4 : IRC.E → Ordᵀ
Definition-7-4 = IRC.Κ
Definition-7-4-ι : (ν : IRC.E) → ⟨ IRC.Δ ν ⟩ → ⟨ IRC.Κ ν ⟩
Definition-7-4-ι = IRC.ι
Definition-7-4-extension : (ν : IRC.E) (A : ⟨ IRC.Δ ν ⟩ → IRC.E)
→ ⟨ IRC.Κ ν ⟩ → Ordᵀ
Definition-7-4-extension = IRC.𝓚
Definition-7-4-ι-is-embedding : (ν : IRC.E) → is-embedding (IRC.ι ν)
Definition-7-4-ι-is-embedding = IRC.ι-is-embedding
Theorem-7-5-1 : propext 𝓤₀
→ (ν : IRC.E) → has-infs-of-complemented-subsets (IRC.Κ ν)
Theorem-7-5-1 = IRC.K-has-infs-of-complemented-subsets
Theorem-7-5-1-compact : (ν : IRC.E) → is-Compact ⟨ IRC.Κ ν ⟩ {𝓥}
Theorem-7-5-1-compact = IRC.Κ-Compact
Theorem-7-5-1-extension : propext 𝓤₀
→ (ν : IRC.E) (A : ⟨ IRC.Δ ν ⟩ → IRC.E) (y : ⟨ IRC.Κ ν ⟩)
→ has-infs-of-complemented-subsets (IRC.𝓚 ν A y)
Theorem-7-5-1-extension = IRC.𝓚-has-infs-of-complemented-subsets
Theorem-7-5-2-dense : (ν : IRC.E) → is-dense (IRC.ι ν)
Theorem-7-5-2-dense = IRC.ι-is-dense
Theorem-7-5-2-order-preserving
: (ν : IRC.E) (x y : ⟨ IRC.Δ ν ⟩)
→ x ≺⟨ [ IRC.Δ ν ] ⟩ y
→ IRC.ι ν x ≺⟨ [ IRC.Κ ν ] ⟩ IRC.ι ν y
Theorem-7-5-2-order-preserving = IRC.ι-is-order-preserving
Theorem-7-5-2-order-reflecting
: (ν : IRC.E) (x y : ⟨ IRC.Δ ν ⟩)
→ IRC.ι ν x ≺⟨ [ IRC.Κ ν ] ⟩ IRC.ι ν y
→ x ≺⟨ [ IRC.Δ ν ] ⟩ y
Theorem-7-5-2-order-reflecting = IRC.ι-is-order-reflecting
Corollary-7-6 : propext 𝓤₀
→ (ν : IRC.E) (p : ⟨ IRC.Κ ν ⟩ → 𝟚)
→ ¬¬ (Σ x ꞉ ⟨ IRC.Κ ν ⟩ , p x ＝ ₀)
→ Σ x₀ ꞉ ⟨ IRC.Κ ν ⟩ ,
is-least-root (underlying-weak-order (IRC.Κ ν)) p x₀
Corollary-7-6 = IRC.K-has-least-roots-of-complemented-subsets
Proposition-7-7-1 : ((ν : IRC.E) → is-equiv (IRC.ι ν)) ↔ LPO
Proposition-7-7-1 = IRC.ι-is-equiv-iff-LPO
Proposition-7-7-2 : LPO → (ν : IRC.E) → is-discrete ⟨ IRC.Κ ν ⟩
Proposition-7-7-2 = IRC.LPO-gives-Κ-discrete
Proposition-7-7-2' : (ν : IRC.E)
→ is-equiv (IRC.ι ν)
→ is-discrete ⟨ IRC.Κ ν ⟩
Proposition-7-7-2' = IRC.ι-is-equiv-gives-Κ-discrete
Proposition-7-7-3 : ((ν : IRC.E) → is-discrete ⟨ IRC.Κ ν ⟩) → WLPO
Proposition-7-7-3 = IRC.Κ-discrete-gives-WLPO
Proposition-7-8 : propext 𝓤₀
→ (((ν : IRC.E) (p : ⟨ IRC.Δ ν ⟩ → 𝟚)
→ ¬¬ (Σ x ꞉ ⟨ IRC.Δ ν ⟩ , p x ＝ ₀)
→ Σ x₀ ꞉ ⟨ IRC.Δ ν ⟩ ,
is-least-root (underlying-weak-order (IRC.Δ ν)) p x₀)
↔ LPO)
Proposition-7-8 = IRC.Δ-least-roots-iff-LPO
Proposition-7-9-1 : [ IRC.Δ IRC.⌜ω+𝟙⌝ ] ⊴ [ IRC.Κ IRC.⌜ω+𝟙⌝ ]
Proposition-7-9-1 = ω+𝟙-is-⊴-ℕ∞
Proposition-7-9-2 : ((ν : IRC.E) → [ IRC.Δ ν ] ⊴ [ IRC.Κ ν ]) ↔ LPO
Proposition-7-9-2 = IRC.Δ-⊴-Κ-iff-LPO ua
Proposition-7-9-2-code : IRC.E
Proposition-7-9-2-code = IRC.⌜ω+𝟚⌝ ua
Proposition-7-9-2-instance
: [ IRC.Δ (IRC.⌜ω+𝟚⌝ ua) ] ⊴ [ IRC.Κ (IRC.⌜ω+𝟚⌝ ua) ] → LPO
Proposition-7-9-2-instance = IRC.Δ-⊴-Κ-gives-LPO ua
Definition-7-10 : B → IRC.E
Definition-7-10 = BtoE.B-to-E
Theorem-7-11-1 : is-set IRC.E
Theorem-7-11-1 = IRC.E-is-set
Theorem-7-11-2 : is-embedding BtoE.B-to-E
Theorem-7-11-2 = BtoE.B-to-E-is-embedding
Theorem-7-11-3 : (b : B) → [ ⟦ b ⟧-Σ₁ ] ≃ₒ [ IRC.Δ (BtoE.B-to-E b) ]
Theorem-7-11-3 = BtoE.Δ-agreement
Theorem-7-11-4 : (b : B) → [ ⟦ b ⟧-Σ' ] ≃ₒ [ IRC.Κ (BtoE.B-to-E b) ]
Theorem-7-11-4 = BtoE.Κ-agreement
Proposition-7-12 : ((ν : IRC.E) → is-totally-separated ⟨ IRC.Κ ν ⟩) → ¬¬ WLPO
Proposition-7-12 = IRC.Κ-totally-separated-gives-¬¬WLPO
Proposition-7-12-code : IRC.E
Proposition-7-12-code = IRC.⌜ℕ∞₂⌝
Proposition-7-12-instance
: is-totally-separated ⟨ IRC.Κ IRC.⌜ℕ∞₂⌝ ⟩ → ¬¬ WLPO
Proposition-7-12-instance = IRC.Κ⌜ℕ∞₂⌝-totally-separated-gives-¬¬WLPO
\end{code}
Remark 7.13 concludes that the ordinals witnessing the failure of
Proposition 7.12 are not in general denoted by Brouwer codes, from
Theorem 6.7(2) and Theorem 7.11. It is a comparison rather than a
further claim.
Labels: Remark 7.13 = rem:kappa-tot-sep-contrast,
Proposition 7.12 = prop:kappa-not-tot-sep,
Theorem 6.7(2) = thm:four-interp-props(item:compactsep-interp),
Theorem 7.11 = thm:brouwer-to-E.
\begin{code}
Prose-limit-points-for-brouwer-codes : (b : B) → ⟨ ⟦ b ⟧-Σ₁ ⟩ → 𝟚
Prose-limit-points-for-brouwer-codes = BDC.ℓ
Prose-limit-points-for-brouwer-codes-isolated
: (b : B) (x : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ BDC.ℓ b x ＝ ₀ → is-isolated (BDC.ι {b} x)
Prose-limit-points-for-brouwer-codes-isolated = BDC.ℓ-isolated
Prose-limit-points-for-brouwer-codes-limit
: (b : B) (x : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ BDC.ℓ b x ＝ ₁ → is-limit-point (BDC.ι {b} x)
Prose-limit-points-for-brouwer-codes-limit = BDC.ℓ-limit
Prose-limit-points-for-brouwer-codes-dichotomy
: (b : B) (x : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ is-isolated (BDC.ι {b} x) + is-limit-point (BDC.ι {b} x)
Prose-limit-points-for-brouwer-codes-dichotomy = BDC.isolatedness-decision
Prose-limit-points-for-brouwer-codes-decidable
: ¬ WLPO
→ (b : B) (x : ⟨ ⟦ b ⟧-Σ₁ ⟩)
→ is-decidable (is-isolated (BDC.ι {b} x))
Prose-limit-points-for-brouwer-codes-decidable = BDC.isolatedness-decision'
Definition-7-14 : {X : 𝓤 ̇ } → X → 𝓤 ̇
Definition-7-14 = is-limit-point
Definition-7-15 : (ν : IRC.E) → ⟨ IRC.Δ ν ⟩ → 𝟚
Definition-7-15 = IRC.ℓ
Theorem-7-16-1 : (ν : IRC.E) (x : ⟨ IRC.Δ ν ⟩)
→ IRC.ℓ ν x ＝ ₀
→ is-isolated (IRC.ι ν x)
Theorem-7-16-1 = IRC.ℓ-isolated
Theorem-7-16-2 : (ν : IRC.E) (x : ⟨ IRC.Δ ν ⟩)
→ IRC.ℓ ν x ＝ ₁
→ is-limit-point (IRC.ι ν x)
Theorem-7-16-2 = IRC.ℓ-limit
Theorem-7-16-3 : (ν : IRC.E) (x : ⟨ IRC.Δ ν ⟩)
→ is-isolated (IRC.ι ν x) + is-limit-point (IRC.ι ν x)
Theorem-7-16-3 = IRC.isolatedness-decision
Theorem-7-16-4 : ¬ WLPO
→ (ν : IRC.E) (x : ⟨ IRC.Δ ν ⟩)
→ is-decidable (is-isolated (IRC.ι ν x))
Theorem-7-16-4 = IRC.isolatedness-decision'
\end{code}
Remark 7.17 states that the order notion of limit point, a point of an
ordinal that is neither a successor of anything nor the least element,
does not agree with the topological notion of Definition 7.14, because
the point (∞ , ι 1) of the compact ordinal Κ ν₂ is a topological limit
point but not an order one.
Labels: Remark 7.17 = rem:limit-points-do-not-agree,
Definition 7.14 = def:limit-point.
\begin{code}
Remark-7-17 : Σ α ꞉ Ordinal 𝓤₀ ,
Σ x ꞉ ⟨ α ⟩ , is-limit-point x
× ¬ OLP.is-order-limit-point α x
Remark-7-17 = OLP.example-of-topological-limit-point-which-is-not-order-limit
\end{code}