Compact totally separated types

Martín Hötzel Escardó

Date: September 9, 2026

Abstract.

Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel’s system $T$ to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

0 Contents

1. Introduction

We consider the following search problem for a type $X$ . Given a function $p:X\to\mathbf{2}$ into the type with elements $0$ and $1$ , we want to either exhibit a point $x:X$ with $p\,x=0$ , that is, a root of $p$ , or else determine that $p$ has no root. This problem amounts to the type

\textstyle\prod_{p\,:\,X\to\mathbf{2}}\,\Big(\big(\textstyle\Sigma_{x:X}p\,x=0\big)\;+\;\big(\textstyle\prod_{x:X}p\,x=1\big)\Big).

For a finite type $X$ this can always be done, by trying the finitely many points in turn. The question investigated in this paper is which infinite types $X$ admit such a procedure. Three related subjects view this requirement in three different ways.

(1)

Computer science reads it as a search problem. Can an infinite type be exhaustively searched mechanically in finite time? Perhaps surprisingly, there are plenty of infinite types that satisfy this searchability condition [12, 13, 14, 15].
(2)

In topology, this turns out to be a compactness problem [14]. In Johnstone’s topological topos [27], which we take as a guiding model, the types of our theory are interpreted as spaces, functions into $\mathbf{2}$ classify the clopen subspaces, and for a closed subtype of a simple type, the requirement above holds exactly when the corresponding space is compact in the sense of topology [14].
(3)

In logic it amounts to a choice problem, because the type displayed above asks for a root to be produced rather than asserted to exist. Which infinite instances of choice can be proved without being taken as axioms?

In classical mathematics, excluded middle decides whether $p$ has a root, and a choice principle produces one when it does. Asking every type $X$ of a universe $\mathcal{U}$ to satisfy the above is equivalent to global choice, the principle

\textstyle\prod_{X:\mathcal{U}}\,\big(\neg\neg X\to X\big),

which is stronger than the axiom of choice and says that we can pick an element of every non-empty type [41, Theorem 3.2.2 and Remark 3.2.5].

In this paper we work constructively in an intensional Martin-Löf type theory, rather than classically in set theory as in our previous paper [14]. As in that paper, we take inspiration from topology to develop examples and counterexamples of such types, as well as their general theory, although we do not assume previous familiarity with topology, except for the sake of motivation [45, 46, 12]. Because of this and by (2) above, we refer to the types that satisfy the searchability condition as compact.

Moreover, we adopt the univalent point of view [41], due to its direct way of capturing various notions of extensionality, as well as the distinction between data and property. Alternatively, in principle everything discussed here could be redeveloped using setoids [24, 25, 39] instead, but we leave such a reworking to interested readers.

The natural numbers fail to be compact constructively. There are nonetheless many infinite compact types, as mentioned above. Perhaps the simplest example is the type of decreasing binary sequences,

\mathbb{N}_{\infty}\;:\equiv\;\textstyle\Sigma_{\alpha\,:\,\mathbf{2}^{\mathbb{N}}}\,\textstyle\prod_{i:\mathbb{N}}\,\alpha\,(i{+}1)\leq\alpha\,i,

which satisfies the universal property of the conatural numbers, and whose topological reading is the one-point compactification of the discrete space of natural numbers with a new point at infinity. It is compact in our type theoretic sense, and we had already shown it to be so in a system as weak as Gödel’s $T$ [15].

The compactness of $\mathbb{N}_{\infty}$ has found applications outside the concerns of this paper. Normann and Tait [37] use its form in Gödel’s $T$ to fill a gap in an unpublished but widely circulated manuscript of Tait from 1958 on the computability of the fan functional. Pradic and Brown [40] use it to prove that the Cantor–Bernstein theorem implies excluded middle.

Compactness as defined above in type theory is uninformative for a type with too few functions into the type $\mathbf{2}$ of booleans. The real numbers are a standard example, where it is consistent that all functions into the booleans are constant, rendering the search problem trivial. We say that a type $X$ is totally separated when the functions into $\mathbf{2}$ separate the points, in the positive sense that

\textstyle\prod_{x,y:X}\,\big(\textstyle\prod_{p\,:\,X\to\mathbf{2}}p\,x=p\,y\big)\to x=y.

This is a Boolean Leibniz principle, whose classical topological reading is that the clopens separate the points. Our type theoretic notion of compactness is faithful to the topological notion with the same name only for types that are totally separated. We may envision obtaining a general type theoretic notion of compactness by changing the booleans to a Sierpiński-like type using dominances [21] and changing the searchability condition slightly (cf. [14]), but this is not investigated in the present work.

Totally separated types are sets in the sense of HoTT/UF, and they are closed under $\Pi$ , $+$ , $\times$ and retracts, and include the discrete types and hence the simple types, but they fail to be closed under $\Sigma$ constructively in general, and we investigate particular cases of totally separated $\Sigma$ types of interest.

All compact types we are able to construct turn out to come equipped with well-orders. Moreover, the constructions that preserve compactness discussed in the body of the paper also preserve well-orderability. We adopt the HoTT Book [41] definition of ordinal, namely a type equipped with a proposition valued order that is transitive, extensional and well-founded. (The HoTT Book also requires the underlying type to be a set, but we observe that this follows automatically from the extensionality condition.)

Trichotomy, namely the principle that $x<y$ or $x=y$ or $x>y$ for all elements $x$ and $y$ of an ordinal, is equivalent to the principle of excluded middle when required for all ordinals, but there are many trichotomous ordinals without assuming excluded middle. Any trichotomous ordinal is discrete (has decidable equality), but e.g. in the topological topos, discrete compact objects are necessarily finite, so that asking for trichotomy together with compactness gives only finite examples.

Another important classical property of ordinals is that every non-empty subset has a least element, which is known to fail in general in a constructive setting. But we do obtain the least element property constructively for a large class of compact totally separated ordinals, replacing subset by complemented subset (classically, every subset is complemented, and, topologically, complemented subsets correspond to clopen subsets).

Although the above phenomena exhibit a dichotomy between trichotomy and compactness, the two notions are related. In fact, a third phenomenon becomes visible in a constructive setting. Two ordinals that are seen to be the same classically can behave in vastly different ways constructively. An example is the classical ordinal $\omega+1$ , which has two manifestations (among others). In one, we equip the type $\mathbb{N}+\mathbf{1}$ with its natural order, which gives rise to a trichotomous ordinal. In the other, we equip $\mathbb{N}_{\infty}$ again with its natural order, which gives rise to a compact totally separated ordinal with the least element property for complemented subsets, which fails to be trichotomous constructively. In the presence of the principle of excluded middle, these two ordinals are the same (and $\mathrm{LPO}$ suffices). But, by the above discussion, in the topological topos, these two ordinals are patently different, one being discrete and the other compact totally separated (i.e. a Stone space [28]), and so are they in Hyland’s effective topos. We have the natural inclusion

which is an injection whose image has empty complement, but it is a bijection if and only if $\mathrm{LPO}$ holds. That every decreasing binary sequence is of one of the forms $1^{n}0^{\omega}$ and $1^{\omega}$ fails constructively, being equivalent to $\mathrm{LPO}$ , while that there is no decreasing binary sequence other than these always holds.

We generalize the above situation by working with ordinal codes and interpreting them in two ways, so that one interpretation gives trichotomous ordinals and a second one gives compact totally separated ordinals with the least element property for complemented subsets. We always have an embedding of the first interpretation into the second, whose image has empty complement. We also discuss the standard interpretation, which fails to produce either trichotomous or compact totally separated ordinals, along with a fourth one that arises naturally and also fails to be totally separated.

We consider two kinds of ordinal codes to obtain the above results. The first ones are Brouwer codes, inductively defined by constructors for zero, successor and countable limits. The second ones are defined together with their interpretations, by induction-recursion in the sense of [9, 10, 11], so that a limit constructor is indexed by any previously constructed ordinal, rather than just $\omega$ . A crucial ingredient of the compact totally separated interpretation is a certain squashed sum, first defined in [15, Section 10] and generalized here as an extended sum for our purposes, with the aid of the theory of injective types [18, 8].

We would like to emphasize an important methodological difference with our previous work [13, 14]. There we worked classically using set theory, with externally defined models to establish our results. Here, instead, we work constructively, reasoning internally in our type theory, where the beginning of this transition took place in [15], informally within constructive mathematics without specifying any particular formal foundation.

Finally, although the fact that computable or constructively definable functions are continuous [34, 47] plays a crucial role in the link of topology with computer science and constructive mathematics, here, as in [15], we do not assume Brouwerian continuity axioms [47, 1]. In particular, we make no continuity assumption for the boolean predicate $p:X\to\mathbf{2}$ in the definition of compactness of the type $X$ , as opposed to our previous work [13, 14], so that our results hold in all topos models of (univalent) type theory [44] and are consistent with classical principles, including excluded middle and choice (but not with global choice, due to our use of univalence).

This is a full version of the four-page abstract [17], with further results, and builds on [15]. All mathematics reported here has been formalized in Agda [35], in TypeTopology [20], and a companion Agda file [19] lists each numbered item of this paper together with what establishes it.

Organization

Section 2 describes our type theory and introduces notation and terminology. Section 3 defines and discusses discrete and totally separated types, covering their closure properties, isolated points and the totally separated reflection. Section 4 does the same for compact types, and discusses the interplay of the three notions, a certain micro-Tychonoff theorem, and the extension of a family of compact types along an embedding. Section 5 fixes our conventions for ordinals and their arithmetic, and constructs extended sums and suprema. Section 6 discusses five interpretations of Brouwer codes as ordinals satisfying various combinations of compactness, discreteness, total separation and trichotomy. Section 7 generalizes Brouwer codes to an inductive-recursive universe in which the branching of a sum may be indexed by any previously constructed discrete ordinal, rather than just $\omega$ , with two interpretations, one trichotomous and the other compact, and gives a decision procedure for telling whether a point of the compact interpretation is isolated or a topological limit point. Section 8 summarizes the results, discusses the reach of these systems and describes the formalization.

2. Preliminaries

We work constructively and we adopt the foundation described in the HoTT Book [41]. In this section, which can be consulted on demand, we fix terminology and notation, and prove some auxiliary facts. We also recall basic notions from constructive mathematics, such as apartness relations and omniscience taboos.

2.1. Our type theory

We work in intensional Martin-Löf type theory with an empty type $\mathbf{0}$ , a one-element type $\mathbf{1}$ with point $\star$ , a two-element type $\mathbf{2}$ with points $0,1$ , a type $\mathbb{N}$ of natural numbers, the type formers $+$ (binary sum or coproduct), $\Pi$ (product), $\Sigma$ (sum or disjoint union), $\mathsf{W}$ types, identity types denoted by the equality sign $=$ , and a hierarchy of universes $\mathcal{U},\mathcal{V},\mathcal{W},\dots$ closed under them, with $\mathcal{U}_{0}$ the first and $\mathcal{U}_{1}$ the next. Binary products, written $X\times Y$ , arise both as general products with index type $\mathbf{2}$ and as sums of constant families, and we choose the latter incarnation by default. We often write a function type $X\to Y$ in the exponential form $Y^{X}$ , as in the Cantor type $\mathbf{2}^{\mathbb{N}}$ .

For a family $A:X\to\mathcal{U}$ and an identification $p:x=y$ , we define $\mathrm{transport}^{A}\,p:A\,x\to A\,y$ , by induction on $p$ considering the reflexivity identification $p=\mathrm{refl}$ , with the family $A$ omitted when it is understood from the context. We say that a point $a:A\,x$ is transported along $p:x=y$ to get a point of the type $A\,y$ .

Definition 2.1 (Emptiness, negation and decidability).

We define

\text{$X$ is empty}\;:\equiv\;(X\to\mathbf{0}).

When we think of the type $X$ as a mathematical statement, the emptiness of $X$ amounts to its negation and is written $\neg X$ . We say that a type $X$ is decidable if we can decide whether it is pointed or empty:

\text{$X$ is decidable}\;:\equiv\;X+\neg X.

We remark that sometimes in the literature the terminology “ $X$ is decidable” is used to mean that $X$ has decidable equality instead. Here we say that $X$ is discrete to mean that it has decidable equality (Section 3). We also remark that we use non-empty to indicate a double negation, as opposed to the positive statement of inhabitation (Section 2.2) that is often adopted in the constructive mathematics literature [3].

Definition 2.2 (Logical equivalence).

Two types $X$ and $Y$ are logically equivalent if each maps into the other:

\text{$X$ and $Y$ are logically equivalent}\;:\equiv\;(X\to Y)\times(Y\to X).

When the types $X$ and $Y$ are mathematical statements, we often just say “equivalent” rather than “logically equivalent”, leaving the context to resolve the ambiguity with the notion of type equivalence (Definition 2.8).

2.2. Univalent foundations

To this type theory we add the univalence axiom [41, 49] and set quotients. Univalence gives function extensionality and propositional extensionality, and set quotients give propositional truncations and set replacement. The formalization behind this paper [19] records where each of the above assumptions is used, taking them as explicit hypotheses wherever they are needed. Full univalence in this paper is assumed from Section 5 onwards, although not all results need it, the earlier sections using only its extensionality consequences.

A proposition, or subsingleton, is a type with at most one element. We write $\|X\|$ for the propositional truncation of a type $X$ , and $\exists$ and $\vee$ for the truncations of $\Sigma$ and $+$ . A type is pointed when it is equipped with a point, inhabited when its truncation is pointed, and non-empty when its emptiness is contradictory, that is, when $\neg\neg X$ holds. We also read truncation in words, saying that something holds in an unspecified way, or a similar mode of expression, when what is asserted is the truncation of the type of data establishing it. For example a type is compact in an unspecified way when the type of its compactness data is inhabited. When the disjuncts of a sum are mutually exclusive propositions, the sum is already a proposition, so the truncation makes no difference and we write “or” for either, as e.g. in the trichotomy of Definition 5.6.

Definition 2.3 (Singletons).

A type $X$ is a singleton or contractible if it has a point $c:X$ , its center of contraction, to which every point is equal:

\text{$X$ is a singleton}\;:\equiv\;\textstyle\Sigma_{c:X}\,\prod_{x:X}\,c=x.

For a family $A:X\to\mathcal{V}$ , there is a unique $x:X$ with $A\,x$ when the sum of $A$ is a singleton:

\exists!\,x:X,\,A\,x\;:\equiv\;\text{the type $\Sigma_{x:X}\,A\,x$ is a singleton}.

A singleton is a proposition, and a pointed proposition is a singleton, and being a singleton is a property.

Definition 2.4 (Homotopy isolated points and sets).

A point $x:X$ is homotopy isolated if the identity type $x=y$ is a proposition for every $y:X$ :

\text{$x$ is homotopy isolated}\;:\equiv\;\textstyle\prod_{y:X}\,(\text{$x=y$ is a proposition}).

A type is a set if all of its points are homotopy isolated.

Call a function weakly constant if any two of its values are equal.

Theorem 2.5 (Hedberg [23]).

If the identity type $x=y$ admits a weakly constant endofunction for every $y:X$ , then $x$ is homotopy isolated. Hence if this holds at every $x:X$ , then $X$ is a set.

Proof.

Fix $y:X$ , and write $f$ for the weakly constant endofunction of $x=y$ , and $c:x=x$ for its value on $\mathrm{refl}$ . We first show that every $p:x=y$ is the composite of $c^{-1}$ followed by $f\,p$ , by induction on $p$ , whose endpoint $y$ varies with it: for $p=\mathrm{refl}$ this is $c^{-1}$ followed by $c$ , which is $\mathrm{refl}$ . Given $p,q:x=y$ , both are then composites of $c^{-1}$ with values of $f$ on $x=y$ , and those two values are equal by weak constancy, so $p=q$ . Thus $x=y$ is a proposition. As $y$ was arbitrary, $x$ is homotopy isolated. ∎

This formulation of the theorem is due to Kraus, Escardó, Coquand and Altenkirch [31, 32].

Definition 2.6 (The type of propositions).

We write $\Omega_{\mathcal{U}}$ for the type of propositions in a universe $\mathcal{U}$ :

\Omega_{\mathcal{U}}\;:\equiv\;\textstyle\Sigma_{P:\mathcal{U}}\,(\text{$P$ is a proposition}),

whose two canonical elements are $\bot:\equiv\mathbf{0}$ and $\top:\equiv\mathbf{1}$ . Propositional extensionality makes two elements of $\Omega_{\mathcal{U}}$ equal exactly when they are logically equivalent, and $\Omega_{\mathcal{U}}$ is a set. We omit the universe subscript when it is understood from the context.

Definition 2.7 (Base and fiber).

For a family $Y:X\to\mathcal{V}$ we call $X$ the base or index type of the sum $\Sigma Y$ , that is, $\Sigma_{x:X}\,Y\,x$ , and $Y\,x$ the fiber over $x:X$ . The fiber of a map $f:X\to Y$ over a point $y:Y$ is the type of points that $f$ sends to $y$ :

f^{-1}(y)\;:\equiv\;\textstyle\Sigma_{x:X}\,f\,x=y.

The two usages agree up to type equivalence, the fiber of the first projection $\Sigma_{x:X}\,Y\,x\to X$ over $x$ being equivalent to $Y\,x$ .

Definition 2.8 (Type equivalences).

A map $f:X\to Y$ is an equivalence if its fibers are all singletons:

\text{$f$ is an equivalence}\;:\equiv\;\textstyle\prod_{y:Y}\,(\text{$f^{-1}(y)$ is a singleton}).

With the above terminology, this says that for every $y:Y$ there is a unique $x:X$ with $f\,x=y$ . We write $X\simeq Y$ for the type of equivalences from $X$ to $Y$ :

X\simeq Y\;:\equiv\;\textstyle\Sigma_{f:X\to Y}\,(\text{$f$ is an equivalence}).

Definition 2.9 (Surjections and induction along them).

A map $f:X\to Y$ is a surjection if its fibers are all inhabited:

\text{$f:X\to Y$ is a surjection}\;:\equiv\;\textstyle\prod_{y:Y}\,\|f^{-1}(y)\|.

This amounts to saying that $\prod_{y:Y}\,\exists_{x:X}\,f\,x=y$ . A surjection supports surjection induction: in order to prove a proposition valued $P:Y\to\mathcal{V}$ at every $y:Y$ , it is enough to prove $P\,(f\,x)$ at every $x:X$ . Conversely, a map supporting this principle is a surjection.

Definition 2.10 (Embeddings).

A map $j:X\to Y$ is an embedding, written $j:X\hookrightarrow Y$ , if its fibers are all propositions:

\text{$j:X\to Y$ is an embedding}\;:\equiv\;\textstyle\prod_{y:Y}\,(\text{$j^{-1}(y)$ is a proposition}).

An embedding is left cancellable, in the sense that $j\,x=j\,x^{\prime}$ implies $x=x^{\prime}$ , and conversely a left cancellable map into a set is an embedding, so that the two notions agree for maps between sets.

We remark that embeddings in this sense are homotopical embeddings rather than topological embeddings. For example, the type of rationals is embedded into the type of Dedekind reals, but not topologically. In the topological topos the rationals get interpreted as a discrete space, and the Dedekind reals as the real line with its usual topology, and the discrete rationals are not a subspace of the real line. Moreover, the Dedekind reals are not the homotopy type of the reals, which would be a singleton, but rather a set in the above sense.

Definition 2.11 (Complemented families).

A family $A:X\to\mathcal{V}$ is complemented if $A\,x$ is decidable for every $x:X$ . A complemented family of propositions on $X$ amounts to a function $X\to\mathbf{2}$ , its characteristic function.

Definition 2.12 (Subsets).

A subset of a type $X$ is a map from $X$ to the type of propositions of Definition 2.6:

S:X\to\Omega_{\mathcal{U}}.

Equivalently, a subset is a proposition valued map $X\to\mathcal{U}$ . We write $x\in S$ , and say that $x$ is a member of $S$ , when the proposition $S\,x$ holds.

A proposition valued family $A:X\to\mathcal{V}$ is equivalently an embedding $Y\hookrightarrow X$ , the family given by its fibers, and when the family is complemented the embedding is classified by a map $X\to\mathbf{2}$ , as illustrated by the following pullback diagram:

In models such as Johnstone’s topological topos, complemented subsets get interpreted as clopens.

Definition 2.13 (Image).

A point $y:Y$ is in the image of a map $f:X\to Y$ when some $x:X$ is sent to $y$ in an unspecified way, and the image of $f$ is the type of the points of $Y$ that are in it:

y\in\mathrm{image}\,f\;:\equiv\;\|f^{-1}(y)\|,\qquad\mathrm{image}\,f\;:\equiv\;\textstyle\Sigma_{y:Y}\,(y\in\mathrm{image}\,f).

The image of a subset $S$ of $X$ along $f$ is the subset of $Y$ whose members are the points that some member of $S$ is sent to in an unspecified way:

y\in\mathrm{image}\,f\,S\;:\equiv\;\exists_{x:X}\,\big(x\in S\times(f\,x=y)\big).

The corestriction of $f$ is the map $X\to\mathrm{image}\,f$ that sends $x$ to $f\,x$ together with a witness that it is in the image, and it is a surjection.

Definition 2.14 (Small and locally small types).

A type $X$ is $\mathcal{U}$ -small if it is equivalent to a type in the universe $\mathcal{U}$ , and it is locally $\mathcal{U}$ -small if the identity type $x=y$ is $\mathcal{U}$ -small for every $x,y:X$ .

Being small is a proposition if and only if univalence holds.

Definition 2.15 (Set replacement).

Set replacement is the principle that, for a map $f:X\to Y$ , if $X$ is $\mathcal{U}$ -small and $Y$ is a locally $\mathcal{V}$ -small set, then the image of $f$ (Definition 2.13) is small.

This is the particular case for sets of a more general replacement principle first identified and studied by Rijke [42, 43].

Definition 2.16 (Set quotients).

Set quotients exist when, for every type $X:\mathcal{U}$ and every $\mathcal{V}$ -valued equivalence relation $\approx$ on $X$ , there is a set $X/\approx$ , the set quotient of $X$ by $\approx$ , with a map $\eta:X\to X/\approx$ that identifies related points and is universal: every map $f:X\to Y$ into a set $Y$ that identifies related points factors as $f=\bar{f}\circ\eta$ for a unique $\bar{f}:{X/\approx}\to Y$ .

Set replacement is equivalent to the existence of set quotients.

2.3. Constructive mathematics

Although the general principle of double negation elimination is equivalent to excluded middle, it does hold constructively in many particular examples of interest.

Definition 2.17 ( $\neg\neg$ -separatedness).

A type $X$ is $\neg\neg$ -separated if identifications in it are $\neg\neg$ -stable:

\text{$X$ is $\neg\neg$-separated}\;:\equiv\;\textstyle\prod_{x,y:X}\,\neg\neg(x=y)\to x=y.

A type with decidable equality is $\neg\neg$ -separated, because decidable types are $\neg\neg$ -stable.

Lemma 2.18.

Every $\neg\neg$ -separated type is a set.

Proof.

Compose the natural map $x=y\to\neg\neg(x=y)$ with the given $\neg\neg(x=y)\to x=y$ , obtaining an endofunction of $x=y$ . It is weakly constant, because $\neg\neg(x=y)$ is a negation and hence a proposition, so that any two intermediate values are equal. The result then follows by Theorem 2.5. ∎

Definition 2.19 (Apartness and tightness).

An apartness on a type $X$ is a proposition valued relation $\mathrel{\sharp}$ which is

(1)

irreflexive: $\neg(x\mathrel{\sharp}x)$ ,
(2)

symmetric: $x\mathrel{\sharp}y\to y\mathrel{\sharp}x$ , and
(3)

cotransitive: $x\mathrel{\sharp}y\to(x\mathrel{\sharp}z)\vee(y\mathrel{\sharp}z)$ .

It is tight if $\neg(x\mathrel{\sharp}y)$ implies $x=y$ , for all $x,y:X$ .

An apartness is the positive counterpart of the negation of equality, in that $x\mathrel{\sharp}y$ asserts a difference where $\neg(x=y)$ only denies equality [4]. Irreflexivity makes an apartness imply negation of equality, and hence makes equality imply the negation of apartness. Tightness asks for the converse of the latter. It follows that a type carrying a tight apartness is $\neg\neg$ -separated, and hence a set by Lemma 2.18.

Definition 2.20 (Extreme density).

For a map $f:X\to Y$ the following are equivalent.

(1)

The complement of the image of $f$ is empty:

$\neg\,\Sigma_{y:Y}\,\neg\,(y\in\mathrm{image}\,f).$
(2)

No point of $Y$ lies outside the image of $f$ :

$\neg\,\Sigma_{y:Y}\,\neg\,\Sigma_{x:X}\,f\,x=y.$

A map satisfying either, and hence both, of these conditions is called extremely dense, and extreme density is a proposition. An alternative terminology, not adopted here, is $\neg\neg$ -density.

Proof.

For any type $A$ the negations $\neg\|A\|$ and $\neg A$ are logically equivalent, so the truncation in $y\in\mathrm{image}\,f$ can be dropped under the inner negation. Extreme density is a proposition, being a negation. ∎

In the presence of the principle of excluded middle, a map is extremely dense if and only if it is a surjection. Extreme density is stronger than density in the topological sense. The rationals are dense in the reals in the usual sense, but the inclusion of the rationals into the Dedekind reals is not extremely dense, since irrational numbers lie outside its image.

Lemma 2.21.

An extremely dense map into a family of $\neg\neg$ -separated types is right-cancellable: if $j:X\to Y$ is extremely dense, if $Z:Y\to\mathcal{U}$ has $Z\,y$ $\neg\neg$ -separated for every $y:Y$ , and if $f,g:\prod_{y:Y}Z\,y$ satisfy $f\,(j\,x)=g\,(j\,x)$ for every $x:X$ , then $f=g$ .

In particular, taking $Z$ constant, two maps $Y\to Z$ into a $\neg\neg$ -separated type that agree after composition with $j$ are equal.

Proof.

For $y:Y$ it is enough to prove $\neg\neg(f\,y=g\,y)$ , $\neg\neg$ -separatedness of $Z\,y$ supplying $f\,y=g\,y$ and function extensionality supplying $f=g$ . If $f\,y\neq g\,y$ then no $x:X$ satisfies $j\,x=y$ , since an identification $p:j\,x=y$ transports the hypothesis $f\,(j\,x)=g\,(j\,x)$ to $f\,y=g\,y$ , so $y$ lies outside the image of $j$ , contradicting extreme density. ∎

Lemma 2.22.

The embedding $\mathbf{2}\to\Omega_{\mathcal{U}}$ that sends $0$ to $\bot$ and $1$ to $\top$ is extremely dense.

Proof.

The map is an embedding because its fiber over $P$ is $\neg P+P$ , a sum of two propositions that exclude each other. Let $P:\Omega_{\mathcal{U}}$ lie outside the image, so that $P\neq\bot$ and $P\neq\top$ , these being the two values of the map. Logically equivalent propositions are equal, so $\neg P$ would give $P=\bot$ , and $P$ would give $P=\top$ . Hence $\neg\neg P$ and $\neg P$ , which is a contradiction. So no point of $\Omega_{\mathcal{U}}$ lies outside the image. ∎

The fiber of this map over $P$ is the decidability of $P$ , so its extreme density says that no proposition can fail to be decidable, whereas excluded middle would say that every proposition is decidable.

Definition 2.23 (Global choice).

Global choice for a universe $\mathcal{U}$ is the principle that every type in $\mathcal{U}$ is decidable, so that given any type $X:\mathcal{U}$ we can either produce a point of $X$ or establish that $X$ is empty, that is,

\textstyle\prod_{X:\mathcal{U}}\,(X+\neg X).

Equivalently, global choice says that we can choose a point of every non-empty type in $\mathcal{U}$ ,

\textstyle\prod_{X:\mathcal{U}}\,(\neg\neg X\to X),

since a decidable type is $\neg\neg$ -stable and, conversely, the type $X+\neg X$ is non-empty for every $X$ . It is a classical principle, stronger than the axiom of choice, and we do not assume it, but it arises as a so-called constructive taboo in the conclusion of some statements.

Definition 2.24 (Excluded middle).

Excluded middle for a universe $\mathcal{U}$ says that every proposition in $\mathcal{U}$ is decidable:

\textstyle\prod_{P:\mathcal{U}}\,\big(\text{$P$ is a proposition}\to P+\neg P\big).

The following taboos also arise in some of the mathematical questions considered in this paper.

Definition 2.25 (Bishop’s principles of omniscience [2]).

Bishop’s $\mathrm{LPO}$ (limited principle of omniscience) decides whether a binary sequence takes the value $0$ somewhere, and $\mathrm{WLPO}$ (weak limited principle of omniscience) decides whether it has value $1$ everywhere:

	$\displaystyle\mathrm{LPO}$	$\displaystyle:\equiv\textstyle\prod_{p:\mathbf{2}^{\mathbb{N}}}\,\big(\text{the type $\Sigma_{n:\mathbb{N}}\,p\,n=0$ is decidable}\big),$
	$\displaystyle\mathrm{WLPO}$	$\displaystyle:\equiv\textstyle\prod_{p:\mathbf{2}^{\mathbb{N}}}\,\big(\text{the type $\prod_{n:\mathbb{N}}\,p\,n=1$ is decidable}\big).$

Equivalently, the principle $\mathrm{LPO}$ says that the finiteness of every conatural number is decidable, and $\mathrm{WLPO}$ says that it is decidable whether a conatural number is the point at infinity (Example 3.1). We use whichever formulation is convenient. In the vocabulary of this paper, $\Sigma$ -compactness of $\mathbb{N}$ is $\mathrm{LPO}$ and $\Pi$ -compactness of $\mathbb{N}$ is $\mathrm{WLPO}$ (Examples 4.5).

Excluded middle gives $\mathrm{LPO}$ , which gives $\mathrm{WLPO}$ . The converse of the latter follows from Markov’s principle (namely that if a complemented family over $\mathbb{N}$ has non-empty sum then its sum is pointed). All of these are independent of our type theory. They hold under classical logic and fail in models where all functions are continuous or computable, such as Johnstone’s topological topos [27] or Hyland’s effective topos [26] respectively. We neither assume nor deny them. When we say that something fails constructively, we mean that it implies a taboo. Saying instead that it is false would be an implication into the empty type, which is a stronger statement. The same applies to the doubly negated forms, such as $\neg\neg\mathrm{WLPO}$ , which are weaker but still independent. Global choice (Definition 2.23) is stronger than all of them, since it decides every type.

We do not assume any Brouwerian continuity axiom. Assuming continuity would settle the above taboos negatively, since it refutes $\mathrm{WLPO}$ and hence $\mathrm{LPO}$ , whereas we keep them undecided in order to stay compatible with classical mathematics, so that our results hold in every model of our foundation, in particular $\infty$ -toposes [44], the boolean ones included.

Remark 2.26 (Weak topological toposes).

The statement $\neg\mathrm{WLPO}$ is independent of our type theory and can be seen as a weak continuity principle [16]. We have that $\mathrm{WLPO}$ is equivalent to the existence of a function $\mathbb{N}_{\infty}\to\mathbb{N}$ that is not continuous, and $\neg\mathrm{WLPO}$ to every function $\mathbb{N}_{\infty}\to\mathbb{N}$ being $\neg\neg$ -continuous, the double negation being removable under Markov’s principle (which we are not assuming). We think of toposes in which $\neg\mathrm{WLPO}$ holds as weak topological toposes.

This remark is the inspiration behind Definition 7.13.

2.4. Retracts and maps of sums

Definition 2.27 (Retracts).

A type $Y$ is a retract of a type $X$ if there are specified maps $r:X\to Y$ and $s:Y\to X$ with $r\circ s$ the identity. We call $r$ a retraction and $s$ a section.

Definition 2.28 (Maps of sums).

Let $A:X\to\mathcal{U}$ and $B:Y\to\mathcal{U}$ be families of types, let $f:X\to Y$ be a map, and let $g\,x:A\,x\to B\,(f\,x)$ be a map for every $x:X$ . The map of the sums induced by $f$ and $g$ applies $f$ to the index and $g$ to the fiber component:

\Sigma(f,g):\Sigma A\to\Sigma B,\qquad\Sigma(f,g)\,(x,a)\;=\;(f\,x,\,g\,x\,a).

Lemma 2.29.

The map $\Sigma(f,g)$ is

(1)

an equivalence if $f$ is one and every $g\,x$ is,
(2)

an embedding if $f$ is one and every $g\,x$ is,
(3)

extremely dense if $f$ is and every $g\,x$ is,
(4)

a retraction if $f$ is the identity and every $g\,x$ is.

Proof.

The fiber of $\Sigma(f,g)$ over a point $(y,b)$ of $\Sigma B$ is the sum, over the points $(x,p)$ of the fiber of $f$ over $y$ , of the fiber of $g\,x$ over the point of $B\,(f\,x)$ obtained from $b$ by transport along $p$ . If the fibers of $f$ and of every $g\,x$ are singletons, then so are these, a sum of singleton types over a singleton type being a singleton, which gives (1). If they are propositions, then so are these, a sum of propositions over a proposition being a proposition, which gives (2).

For (3), let $(y,b)$ be a point of $\Sigma B$ and assume that no point of $\Sigma A$ is sent to it. The assumption to be contradicted is itself a negation, so we may reason under a double negation, and extreme density of $f$ supplies $x:X$ with $p:f\,x=y$ . Transporting $b$ along $p$ backwards gives a point of $B\,(f\,x)$ , and extreme density of $g\,x$ supplies $a:A\,x$ mapped to it, so that $\Sigma(f,g)\,(x,a)=(y,b)$ , which is the required contradiction.

For (4), let $s\,x$ be a section of $g\,x$ for every $x$ . Then $\Sigma(\mathrm{id},s)$ is a section of $\Sigma(\mathrm{id},g)$ , the two composing to $\Sigma(\mathrm{id},g\circ s)$ , which is the identity. ∎

3. Totally separated types

This section studies the notions of discrete type, isolated point, and totally separated type. Compactness, which interacts with all of them, is discussed in Section 4.

The following type, already mentioned in Section 1, plays a major role in this paper and also illustrates many concepts.

Example 3.1.

The type $\mathbb{N}_{\infty}$ of conaturals, equivalently the final coalgebra of $X\mapsto\mathbf{1}+X$ , is the type of decreasing binary sequences,

\mathbb{N}_{\infty}\;:\equiv\;\Sigma_{\alpha\,:\,\mathbf{2}^{\mathbb{N}}}\,\textstyle\prod_{i:\mathbb{N}}\,\alpha\,(i{+}1)\leq\alpha\,i.

Being decreasing is a proposition, so the first projection embeds $\mathbb{N}_{\infty}$ into the Cantor type $\mathbf{2}^{\mathbb{N}}$ , and we write $u_{i}$ for the $i$ -th digit of $u:\mathbb{N}_{\infty}$ . This embedding is a section of the map $\beta\mapsto\big(i\mapsto\min\{\beta\,0,\dots,\beta\,i\}\big)$ that forces a binary sequence to be decreasing and leaves the decreasing sequences unchanged, so $\mathbb{N}_{\infty}$ is a retract of the Cantor type. Write $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ for the inclusion and $\underline{k}=\iota\,k$ for its value at $k$ , the sequence of $k$ ones followed by zeros,

\underline{k}\;=\;\big(i\mapsto\text{$1$ if $i<k$, and $0$ otherwise}\big),

so that $\underline{0}$ is constantly $0$ and $\underline{k{+}1}$ prefixes a $1$ to $\underline{k}$ . We let $\infty:\mathbb{N}_{\infty}$ be the constantly $1$ sequence. For $n:\mathbb{N}$ and $u:\mathbb{N}_{\infty}$ we write $n\mathrel{\sqsubset}u$ to say that the $n$ -th digit of $u$ is $1$ , and $u\mathrel{\sqsubseteq}n$ to say that it is $0$ , so that the two are negations of each other. We say that $u$ is finite when $u=\underline{k}$ for some $k$ , equivalently when $u\mathrel{\sqsubseteq}i$ for some $i$ .

3.1. Discrete types and isolated points

Definition 3.2 (Isolatedness and discreteness).

A point $x:X$ is isolated if we can decide, for every $y:X$ , whether $x$ and $y$ are equal:

\text{$x$ is isolated}\;:\equiv\;\textstyle\prod_{y:X}\,(\text{$x=y$ is decidable}).

A type $X$ is discrete if every point of $X$ is isolated, which amounts to saying that $X$ has decidable equality.

Examples 3.3.

(1)

The types $\mathbf{0}$ , $\mathbf{1}$ and $\mathbf{2}$ are discrete, and so is every proposition.
(2)

The type of natural numbers is discrete.
(3)

The type $\mathbb{N}_{\infty}$ is discrete if and only if $\mathrm{WLPO}$ holds.
(4)

The finite points of $\mathbb{N}_{\infty}$ of the form $\underline{n}$ are isolated.
(5)

The point $\infty$ of $\mathbb{N}_{\infty}$ is isolated if and only if $\mathrm{WLPO}$ holds.
(6)

The map $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ sending $\mathrm{inl}\,n$ to $\underline{n}$ and the added point to $\infty$ is an extremely dense embedding (Definition 2.20).

Proof.

Every proposition is discrete, since any two of its points are equal. The types $\mathbf{0}$ and $\mathbf{1}$ are propositions, and $\mathbf{2}$ is discrete, its two points being distinct.

The natural numbers are discrete, with equality decided by induction.

A finite point $\underline{n}$ is isolated, because $u=\underline{n}$ holds exactly when $u_{i}=1$ for $i<n$ and $u_{n}=0$ , which is decided by inspecting finitely many digits.

If $\mathbb{N}_{\infty}$ is discrete then in particular $\infty$ is isolated, and if $\infty$ is isolated then $\mathrm{WLPO}$ holds, because a binary sequence $p$ gives the conatural number $u$ with digits $u_{i}=\min\{p\,0,\dots,p\,i\}$ (Example 3.1), and $u=\infty$ exactly when $p$ is constantly $1$ . Conversely, $\mathrm{WLPO}$ makes $\mathbb{N}_{\infty}$ discrete, because being decreasing is a proposition, so that two points are equal exactly when their digits agree, which is to say that the sequence $i\mapsto(\text{$u_{i}$ equals $v_{i}$})$ is constantly $1$ .

The map $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ is an embedding, its fibers being propositions because $\underline{(-)}$ is an embedding, because $\mathbb{N}_{\infty}$ is a set, which makes the constant map at $\infty$ an embedding, and because $\infty$ is not finite, so that no fiber meets both cases, and it is extremely dense, because a point of $\mathbb{N}_{\infty}$ outside its image would be neither finite nor equal to $\infty$ , which is contradictory. ∎

Lemma 3.4.

(1)

Every discrete type is a set.
(2)

Every isolated point is homotopy isolated (Definition 2.4).
(3)

Being isolated and being discrete are propositions.

Proof.

From decidability of $x=y$ we get an endofunction of $x=y$ that returns a fixed identification in the positive case and is vacuous in the negative one, hence is weakly constant, so Hedberg’s Theorem 2.5 applies, at a single point for (2) and at every point for (1).

For the last item, being isolated at $x$ is a $\Pi$ -type of decidability statements about identity types, and to show that it is a proposition we may assume a witness, since a type is a proposition as soon as it is one under the assumption of a point. That assumption makes each type $x=y$ a proposition, by (2), so each decidability statement is a binary sum of two propositions that exclude each other, hence a proposition, and so is the $\Pi$ -type. Being discrete is then a $\Pi$ -type of propositions. ∎

Remark 3.5.

Classically, isolatedness and homotopy isolatedness (Definition 2.4) coincide. One direction is constructive, every isolated point being homotopy isolated (Lemma 3.4(2)), and for the other, excluded middle makes the proposition $x=y$ decidable. Constructively the two differ: $\mathbb{N}_{\infty}$ is a set, so every point is homotopy isolated, whereas $\infty$ is isolated if and only if $\mathrm{WLPO}$ holds (Examples 3.3).

Proposition 3.6.

(1)

Isolatedness is preserved by $\mathrm{inl}$ , $\mathrm{inr}$ , and hence discreteness is closed under binary sums.
(2)

Discreteness is closed under retracts.
(3)

A subtype of a discrete type is discrete, and, more generally, at a discrete index type the $\Sigma$ -types of discrete types are discrete, so that in particular binary products are.
(4)

At any index type $X$ , if $x:X$ and $y:Y\,x$ are isolated then so is $(x,y)$ , and conversely, isolatedness of $(x,y)$ gives isolatedness of $y$ when $X$ is a set, and for products also of $x$ , with no hypothesis. (Isolatedness of the first component of a general sum needs the fibers to be compact (Lemma 4.19).)
(5)

Left-cancellable maps, embeddings and equivalences reflect isolatedness, and equivalences also preserve isolatedness, and preserve and reflect discreteness.

Proof.

(1) $\mathrm{inl}\,x$ is isolated when $x$ is, because an element of $X+Y$ is either of the form $\mathrm{inl}\,x^{\prime}$ , and then equality with $\mathrm{inl}\,x$ reduces to $x^{\prime}=x$ , or of the form $\mathrm{inr}\,y$ , and then the two are distinct, and symmetrically for $\mathrm{inr}$ . Discreteness of $X+Y$ follows by cases. (2) For a retraction $r$ with section $s$ , decide $s\,y=s\,y^{\prime}$ in the discrete type. Equality of these two values gives $y=y^{\prime}$ after applying the retraction $r$ and using $r\circ s\sim\mathrm{id}$ , and their inequality gives $y\neq y^{\prime}$ .

(3) A proposition valued subtype of a discrete type is discrete because equality of pairs reduces to equality of first components, the second being a proposition. For $\Sigma$ -types with a discrete index, decide first components. If they differ, the pairs differ, and if they agree, transport and decide the second.

(4) For a pair $(x,y)$ of isolated points, the same case analysis works at any index type. Isolatedness of $x$ decides the first components, and when they agree the identification between them is $\mathrm{refl}$ , an isolated point being homotopy isolated (Lemma 3.4(2)), so that the second components are compared without transport. Conversely, from isolatedness of $(x,y)$ we recover isolatedness of $y$ by pairing an arbitrary $y^{\prime}$ with $x$ , for which we need the identification of first components to be unique, that is, for $X$ to be a set. For $\times$ the set hypothesis is unnecessary, the fiber not depending on the first component, and there isolatedness of $x$ is recovered as well, by pairing an arbitrary $x^{\prime}$ with $y$ .

(5) A left-cancellable $f$ reflects isolatedness, since to decide $x^{\prime}=x$ we decide $f\,x^{\prime}=f\,x$ and cancel. Embeddings and equivalences are left cancellable. An equivalence also preserves isolatedness, being left cancellable in the other direction as well. ∎

Lemma 3.7.

(1)

If a type $Y$ has two distinct points, then discreteness of $Y^{X}$ implies that the emptiness of $X$ is decidable.
(2)

A map out of a proposition into homotopy isolated points, in particular into isolated points, is always an embedding.

Proof.

For the first claim, let $y_{0}\neq y_{1}$ in $Y$ and decide, in the discrete type $Y^{X}$ , whether the two constant maps $\lambda x.\,y_{0}$ and $\lambda x.\,y_{1}$ are equal. If they are, then $y_{0}=y_{1}$ at every $x:X$ , so $X$ must be empty. If they are not, then $X$ cannot be empty, since over an empty $X$ any two maps are equal.

For the second, let $P$ be a proposition and $f:P\to Y$ land in homotopy isolated points. The fiber of $f$ over $y$ is $\Sigma_{p:P}(f\,p=y)$ , and any two of its elements have equal first components, since $P$ is a proposition, and equal second components, since $f\,p=y$ is a proposition by homotopy isolatedness. So the fibers are propositions, and hence $f$ is an embedding. Isolated points are homotopy isolated (Lemma 3.4(2)), which gives the statement for maps into isolated points. ∎

3.2. Totally separated types

The following is a Boolean Leibniz principle, whose classical topological reading is that the clopens separate the points.

Definition 3.8 (Total separatedness).

A type $X$ is totally separated if the maps $X\to\mathbf{2}$ separate the points of $X$ , in the positive sense that for all $x,y:X$ , if $p\,x=p\,y$ for every $p:X\to\mathbf{2}$ , then $x=y$ . Write

x=_{2}y\,:\equiv\,\prod_{p:\mathbf{2}^{X}}p\,x=p\,y

for the equivalence relation that $x$ and $y$ are indistinguishable by $\mathbf{2}$ -valued maps, so that total separatedness amounts to $x=_{2}y\to x=y$ .

This notion is classically uninteresting, because excluded middle implies that every set is totally separated, in view of Lemma 3.9(1).

Lemma 3.9.

(1)

Every discrete type is totally separated.
(2)

Every totally separated type is $\neg\neg$ -separated.
(3)

Every totally separated type is a set.
(4)

Being totally separated is a proposition.

Proof.

If $X$ is discrete and $x=_{2}y$ , apply the hypothesis to the characteristic function of $x$ , which sends $x$ to $0$ . It must then send $y$ to $0$ as well, which for that particular function means $x=y$ .

For $\neg\neg$ -separatedness, suppose $\neg\neg(x=y)$ . For each $p:X\to\mathbf{2}$ we get $\neg\neg(p\,x=p\,y)$ by applying $p$ , and $\mathbf{2}$ is $\neg\neg$ -separated because equality in it is decidable. So $x=_{2}y$ , and total separatedness gives $x=y$ . Being a set then follows, since $\neg\neg$ -separated types are sets by Lemma 2.18.

For the last item, given a witness of total separatedness the type is a set by (3), so total separatedness is a $\Pi$ -type of identity types of a set, hence a proposition, and a type is a proposition as soon as it is one under the assumption of a point of it. ∎

Examples 3.10.

(1)

The homotopical circle fails to be totally separated for homotopical reasons, because it is not a set [41, Section 6.4], and totally separated types are sets by Lemma 3.9(3).
(2)

The type $\Omega_{\mathcal{U}}$ of propositions fails to be totally separated for constructive reasons: if $\Omega_{\mathcal{U}}$ is $\neg\neg$ -separated (in particular, if it is totally separated), then excluded middle holds for $\mathcal{U}$ (Definition 2.24).
(3)

More relevantly for us, the type $\Sigma_{x:\mathbb{N}_{\infty}}\,\mathbf{2}^{x=\infty}$ fails to be totally separated constructively, namely its total separatedness implies $\neg\neg\mathrm{WLPO}$ . This example is [22, Theorem 2.7], and is the prototype here for the failure of total separatedness proved in Section 6.2 below.

We can visualise the type $\Sigma_{x:\mathbb{N}_{\infty}}\,\mathbf{2}^{x=\infty}$ of item (3) as a sequence that converges to two distinct points at infinity:

In classical topology, in a Hausdorff space, and hence in a totally separated space (the clopens separate the points), the intersection of two compact subsets is compact. The type $\Sigma_{x:\mathbb{N}_{\infty}}\,\mathbf{2}^{x=\infty}$ gives a counterexample:

Proof of Examples 3.10(2,3).

(2) Let $P$ be a proposition with $\neg\neg P$ , and regard it as a point $p:\Omega_{\mathcal{U}}$ . Then $P$ holds if and only if $p=\top$ , so $\neg\neg P$ gives $\neg\neg(p=\top)$ , and $\neg\neg$ -separatedness of $\Omega_{\mathcal{U}}$ gives $p=\top$ , hence $P$ . That is double negation elimination, which is equivalent to excluded middle. Total separatedness gives $\neg\neg$ -separatedness by Lemma 3.9(2).

(3) The type has two copies of the point at infinity, namely the pairs $\infty_{0}=(\infty,\lambda\_.\,0)$ and $\infty_{1}=(\infty,\lambda\_.\,1)$ , which are distinct because $\mathbb{N}_{\infty}$ is a set, so that the fibers over $\infty$ are compared without transport. A map $p$ separating them gives the two maps $u\mapsto p\,(u,\lambda\_.\,0)$ and $u\mapsto p\,(u,\lambda\_.\,1)$ from $\mathbb{N}_{\infty}$ to $\mathbf{2}$ , which agree at every finite point, the type $\underline{n}=\infty$ being empty, and differ at $\infty$ , and deciding whether a conatural number is $\infty$ amounts to $\mathrm{WLPO}$ (Definition 2.25). So $\neg\mathrm{WLPO}$ leaves the two points indistinguishable by $\mathbf{2}$ -valued maps, and total separatedness would then identify them, so total separatedness of the sum gives $\neg\neg\mathrm{WLPO}$ . ∎

Write

x\mathrel{\sharp}_{2}y:\equiv\exists_{p:\mathbf{2}^{X}}\,p\,x\neq p\,y

for the relation that some $\mathbf{2}$ -valued map separates $x$ from $y$ . For every type $X$ , whether or not it is totally separated, this is an apartness: irreflexivity says that $p\,x\neq p\,x$ is impossible, symmetry is clear, and for cotransitivity, given $p$ with $p\,x\neq p\,y$ and any $z$ , decide $p\,x=p\,z$ in $\mathbf{2}$ , which gives $p\,z\neq p\,y$ in one case and $p\,x\neq p\,z$ in the other.

Proposition 3.11.

The following are equivalent for any type $X$ .

(1)

$X$ is totally separated, meaning that $x=_{2}y\to x=y$ .
(2)

The quasi-component $\Sigma_{y}\,x=_{2}y$ of every point $x:X$ is a singleton.
(3)

The evaluation function $\mathrm{eval}_{X}:X\to\mathbf{2}^{\mathbf{2}^{X}}$ that maps $x:X$ to the function $(p\mapsto p\,x):\mathbf{2}^{X}\to\mathbf{2}$ is an embedding.
(4)

The apartness relation $\mathrel{\sharp}_{2}$ is tight.

Proof.

(1) $\Leftrightarrow$ (2). The quasi-component of a point $x$ has the point $(x,\mathrm{refl}_{2})$ , where $\mathrm{refl}_{2}$ witnesses the reflexivity of $=_{2}$ . Assuming (1), any point $(y,e)$ of the quasi-component has $y=x$ , and the second components then agree because $x=_{2}y$ is a proposition, being a $\Pi$ -type of identity types in the set $\mathbf{2}$ . So the quasi-component of $x$ is a singleton, with center $(x,\mathrm{refl}_{2})$ . Conversely, assume (2) and let $e$ witness $x=_{2}y$ . The points $(x,\mathrm{refl}_{2})$ and $(y,e)$ of the quasi-component of $x$ are equal, and their first components give $x=y$ .

(1) $\Leftrightarrow$ (3). An embedding is a map whose fibers are propositions, and the fiber of $\mathrm{eval}_{X}$ over a point $\Phi$ of $\mathbf{2}^{\mathbf{2}^{X}}$ is the type

\Sigma_{x:X}\,(\mathrm{eval}_{X}\,x=\Phi).

By function extensionality, an identification $\mathrm{eval}_{X}\,x=\mathrm{eval}_{X}\,y$ amounts to $x=_{2}y$ . Assuming (3), if $x=_{2}y$ then the points $(x,\mathrm{refl})$ and $(y,e)$ , where $e$ is the identification that $x=_{2}y$ gives in this way, lie in the fiber over $\mathrm{eval}_{X}\,x$ , which is a proposition, so they are equal and their first components give $x=y$ . Conversely, assuming (1), any two points of a fiber have equal first components, and their second components then agree because $\mathbf{2}^{\mathbf{2}^{X}}$ is a set, being a product of copies of the set $\mathbf{2}$ .

(1) $\Leftrightarrow$ (4). Tightness of $\mathrel{\sharp}_{2}$ says that $\neg(x\mathrel{\sharp}_{2}y)$ implies $x=y$ , and the hypothesis says that no $p$ separates $x$ from $y$ . The truncation in $\mathrel{\sharp}_{2}$ can be dropped, because the statement is negated and hence a proposition. Since $p\,x\neq p\,y$ is decidable in $\mathbf{2}$ , the hypothesis is equivalent to $p\,x=p\,y$ for every $p$ , that is, to $x=_{2}y$ . So tightness of $\mathrel{\sharp}_{2}$ and total separatedness are the same assertion. ∎

Proposition 3.12.

Total separatedness is closed under

(1)

retracts, hence under equivalence,
(2)

binary products,
(3)

sums when the index type is discrete, and, as the special case of this indexed by $\mathbf{2}$ , under binary sums,
(4)

arbitrary products.

Proof.

For retracts, let $r:X\to Y$ be a retraction with section $s$ , and let $y=_{2}y^{\prime}$ in $Y$ . Testing $y$ and $y^{\prime}$ against the predicates of the form $q\circ s$ with $q:X\to\mathbf{2}$ gives $s\,y=_{2}s\,y^{\prime}$ , hence $s\,y=s\,y^{\prime}$ by the total separatedness of $X$ , and applying $r$ gives $y=y^{\prime}$ .

For sums over a discrete index, let $(a,b)=_{2}(x,y)$ in $\Sigma\,Y$ . Testing against the predicates that ignore the second component gives $a=_{2}x$ in the index, and hence $a=x$ by discreteness and Lemma 3.9(1). Let $b^{\prime}$ be the transport of $b$ along this identification. Given $q:Y\,x\to\mathbf{2}$ , define a predicate on $\Sigma\,Y$ by deciding, for each index $u$ , whether $u=x$ , which discreteness allows, and sending $(u,v)$ to the value of $q$ at the transport of $v$ along the identification $u=x$ when there is one, and to $0$ when there is not. A discrete type is a set (Lemma 3.4(1)), so the identification decided at $x$ itself is $\mathrm{refl}$ , and the predicate takes the value $q\,y$ at $(x,y)$ . Testing $(a,b)$ and $(x,y)$ against it gives $q\,b^{\prime}=q\,y$ . So $b^{\prime}=_{2}y$ , and the total separatedness of $Y\,x$ gives $b^{\prime}=y$ , which together with $a=x$ gives $(a,b)=(x,y)$ . Binary sums are the case of a two-element discrete index.

For products, let $\varphi=_{2}\psi$ in $\prod_{x}Y\,x$ , and fix $x:X$ and $q:Y\,x\to\mathbf{2}$ . Testing $\varphi$ and $\psi$ against the predicate $\lambda\gamma.\,q\,(\gamma\,x)$ gives $q\,(\varphi\,x)=q\,(\psi\,x)$ , so that $\varphi\,x=_{2}\psi\,x$ , and the total separatedness of $Y\,x$ gives $\varphi\,x=\psi\,x$ . Since $x$ was arbitrary, the functions $\varphi$ and $\psi$ agree at every point and hence are equal. Binary products are the case of a two-element index. ∎

Examples 3.13.

(1)

Total separatedness fails constructively to be closed under $\Sigma$ . The index type and the fibers of the type $\Sigma_{x:\mathbb{N}_{\infty}}\,\mathbf{2}^{x=\infty}$ are totally separated, whereas its own total separatedness implies $\neg\neg\mathrm{WLPO}$ (Examples 3.10(3)).
(2)

The simple types are the smallest collection of types containing $\mathbb{N}$ and closed under function types, and the Baire type $\mathbb{N}^{\mathbb{N}}$ is one of them. Every simple type is totally separated and pointed, and has $\mathbb{N}$ as a retract. More generally, every retract of $\mathbb{N}$ , such as the type $\mathbf{2}$ , is a retract of every simple type.
(3)

The converse of Lemma 3.9(1) fails constructively: the Cantor type $\mathbf{2}^{\mathbb{N}}$ is totally separated, and its discreteness implies $\mathrm{WLPO}$ .

Total separatedness also fails constructively to be closed under surjective images, as we will see in Example 6.10.

Proof.

(1) The index type $\mathbb{N}_{\infty}$ is a retract of $\mathbf{2}^{\mathbb{N}}$ (Example 3.1), and the Cantor type and the fibers $\mathbf{2}^{x=\infty}$ are products of copies of $\mathbf{2}$ , which is totally separated, being discrete (Lemma 3.9(1)). So the index type and the fibers are totally separated, because total separatedness is closed under products and retracts (Proposition 3.12).

(2) All three claims are proved by induction on the construction of the simple types. The type $\mathbb{N}$ is discrete and hence totally separated, and total separatedness is closed under $\Pi$ (Proposition 3.12(4)). Pointedness holds at the base type and passes to function types by taking constant functions. For the retract claim, the induction step is that if $A$ is a retract of $Y$ and $X$ is pointed, then $A$ is a retract of $Y^{X}$ , sending a point of $A$ to the constant function at its image in $Y$ , and recovering it from a function $X\to Y$ by evaluating at the point of $X$ and retracting. A retract of $\mathbb{N}$ is a retract of the base type, so this step carries it through the function types, and the type $\mathbf{2}$ is a retract of $\mathbb{N}$ .

(3) The Cantor type $\mathbf{2}^{\mathbb{N}}$ is a product of copies of $\mathbf{2}$ , and so is totally separated by the same reasoning as in (1). Two of its points are equal exactly when they agree at every index, so its discreteness decides, for any binary sequence, whether it is equal to the constant sequence $1$ , that is, whether it is constantly $1$ , which is $\mathrm{WLPO}$ in the formulation of Definition 2.25. ∎

We have seen that totally separated types are not in general closed under sums. The following is a sufficient condition for a sum to be totally separated, which will be useful for our purposes (Theorem 6.7(2)).

Lemma 3.14.

For any family $A:\mathbb{N}_{\infty}\to\mathcal{V}$ with $A\,u$ totally separated for every $u$ and with $A\,\infty$ a proposition, its sum $\Sigma A$ is totally separated.

Proof.

Let $(u,a)=_{2}(v,b)$ . Testing against the predicates that ignore the second component gives $u=_{2}v$ , and $\mathbb{N}_{\infty}$ is totally separated, being a retract (Example 3.1) of the totally separated type $\mathbf{2}^{\mathbb{N}}$ (Examples 3.13(3)), so $u=v$ . Transport $a$ along this identification to $a^{\prime}:A\,v$ , so that $(u,a)=(v,a^{\prime})$ , and it remains to show that $a^{\prime}=b$ , for which, $A\,v$ being totally separated, it is enough to show that $a^{\prime}=_{2}b$ . So let $r:A\,v\to\mathbf{2}$ . As $\mathbf{2}$ is $\neg\neg$ -separated it is enough to rule out $r\,a^{\prime}\neq r\,b$ , so suppose that it holds. If $v$ were a finite point $\underline{n}$ , then, that point being isolated (Examples 3.3), $r$ would extend to a predicate on $\Sigma A$ by deciding, for each index $w$ , whether $w=\underline{n}$ , applying $r$ after transport when it is and taking the value $0$ when it is not, as in the proof of Proposition 3.12 for a discrete index, and testing $(u,a)$ and $(v,b)$ against it would give $r\,a^{\prime}=r\,b$ . So $v$ is not a finite point. If $v$ were $\infty$ , then $a^{\prime}=b$ , since $A\,\infty$ is a proposition, and again $r\,a^{\prime}=r\,b$ . So $v\neq\infty$ . But a conatural number that is not finite is $\infty$ , which is a contradiction. ∎

Every type can be turned into a totally separated type in a universal way.

Theorem 3.15.

Every type $X$ has a totally separated reflection $\mathbb{T}\,X$ , constructed as the image of the evaluation map $\mathrm{eval}_{X}:X\to\mathbf{2}^{\mathbf{2}^{X}}$ defined in Proposition 3.11(3), together with a reflector $\eta^{\mathbb{T}}:X\to\mathbb{T}\,X$ , such that

(1)

$\mathbb{T}\,X$ is totally separated, and $\eta^{\mathbb{T}}$ is a surjection,
(2)

for every totally separated $A$ and $f:X\to A$ , there is a unique $\bar{f}:\mathbb{T}\,X\to A$ with $\bar{f}\circ\eta^{\mathbb{T}}=f$ , or, equivalently, precomposition with $\eta^{\mathbb{T}}$ is an equivalence $A^{\mathbb{T}\,X}\simeq A^{X}$ ,
(3)

the reflector identifies $x$ and $y$ if and only if $x=_{2}y$ .

Proof.

Put $\mathbb{T}\,X:\equiv\mathrm{image}(\mathrm{eval}_{X})$ , a subtype of $\mathbf{2}^{\mathbf{2}^{X}}$ , and let $\eta^{\mathbb{T}}$ be the corestriction of $\mathrm{eval}_{X}$ , which is a surjection onto its image, so that surjection induction (Definition 2.9) is available for $\eta^{\mathbb{T}}$ .

(1) $\mathbb{T}\,X$ is totally separated, since its elements are pairs $(\varphi,w)$ with $w$ a truncated witness of being in the image, hence a proposition, so two elements are equal as soon as their first components are. Given $(\varphi,w)=_{2}(\gamma,w^{\prime})$ , test against the predicates $x^{\prime}\mapsto\mathrm{pr}_{1}x^{\prime}\,p$ for each $p:X\to\mathbf{2}$ , which gives $\varphi\,p=\gamma\,p$ for every $p$ , so $\varphi=\gamma$ .

(2) Let $A$ be totally separated and $f:X\to A$ . Uniqueness is immediate from $\eta^{\mathbb{T}}$ being a surjection and $A$ a set (Lemma 3.9(3)). For existence, note that by Proposition 3.11(3) the map $\mathrm{eval}_{A}$ is an embedding, so the fibers $\Sigma_{a}\,\mathrm{eval}_{A}\,a=\gamma$ are propositions, and this lets us define $\bar{f}(\varphi,w)$ by untruncating $w$ , because the target is a proposition, and taking the unique $a$ with $\mathrm{eval}_{A}\,a=\lambda q.\,\varphi(q\circ f)$ . By construction, $q\,(\bar{f}\,(\varphi,w))=\varphi\,(q\circ f)$ for every $q:A\to\mathbf{2}$ , so that $q\,(\bar{f}\,(\eta^{\mathbb{T}}\,x))=q\,(f\,x)$ at every $x:X$ , and the total separatedness of $A$ gives $\bar{f}\circ\eta^{\mathbb{T}}=f$ .

(3) If $\eta^{\mathbb{T}}\,x=\eta^{\mathbb{T}}\,y$ then their first components agree, which is exactly $x=_{2}y$ . Conversely $x=_{2}y$ gives equality of first components, and the second components are propositions. ∎

A special case of interest of Theorem 3.15(2) is $A=\mathbf{2}$ , which shows that the boolean valued predicates on $X$ are in canonical bijection with those on $\mathbb{T}\,X$ .

4. Compact types

This section studies the notion of compact type, including its closure properties, its interplay with the notions of discreteness and total separatedness, as well as the extension of families of compact types along embeddings, which is crucial for the purposes of Sections 6 and 7.

4.1. Definitions and first examples

Definition 4.1 (Compactness).

A type $X$ is $\Sigma$ -compact, or compact for short, if it is decidable, for every $p:X\to\mathbf{2}$ , whether $p$ has a root:

\textstyle\prod_{p:\mathbf{2}^{X}}\,\big(\text{the type $\Sigma_{x:X}\,p\,x=0$ is decidable}\big).

We also consider the weaker notions of $\exists$ -compactness and $\Pi$ -compactness, obtained by replacing $\Sigma_{x:X}\,p\,x=0$ by $\exists_{x:X}\,p\,x=0$ and by $\Pi_{x:X}\,p\,x=1$ respectively.

The same notions can be equivalently formulated with an arbitrary complemented family in place of a $\mathbf{2}$ -valued predicate.

Lemma 4.2.

For any type $X$ and any universe $\mathcal{V}$ , the compactness of $X$ is logically equivalent to the statement that the sum $\Sigma_{x:X}\,A\,x$ is decidable for every complemented family $A:X\to\mathcal{V}$ , and also to the restriction of this to proposition valued families $A$ .

Proof.

A complemented family $A$ has a characteristic function $p:X\to\mathbf{2}$ , with $p\,x=0$ giving $A\,x$ and $p\,x=1$ refuting it, and then $A\,x$ and $p\,x=0$ are logically equivalent for every $x$ , because $A\,x$ rules out $p\,x=1$ . In the other direction, a predicate $p:X\to\mathbf{2}$ gives the family sending $x$ to $\mathbf{1}$ when $p\,x=0$ and to $\mathbf{0}$ when $p\,x=1$ , which is complemented and proposition valued, and which lives in any universe, because $\mathbf{0}$ and $\mathbf{1}$ do. Pointwise logically equivalent families have logically equivalent $\Sigma$ -types, and decidability is invariant under logical equivalence. ∎

The notions of $\exists$ -compactness and $\Pi$ -compactness, and the pointed compactness of Lemma 4.6 below, can be treated by the same argument. In view of Lemma 4.2, we say simply that a type is compact, using whichever of these formulations is convenient for proofs, and saying which one when this matters. In particular, compactness does not depend on the universe $\mathcal{V}$ .

Lemma 4.3.

Every compact type is decidable, and every decidable proposition is compact.

Proof.

For the first claim, apply compactness of $X$ to the constantly $0$ predicate. Either it has a root, which in particular supplies a point of $X$ , or else $0=1$ for every point of $X$ , which gives $\neg X$ .

For the second, let $X$ be a decidable proposition and let $p:X\to\mathbf{2}$ . If $\neg X$ then $p\,x=1$ for every $x:X$ vacuously. If $x:X$ , decide the value of $p\,x$ . If $p\,x=0$ then $p$ has a root. If $p\,x=1$ then, since $X$ is a proposition, every $y:X$ is equal to $x$ , so $p\,y=1$ . ∎

Proposition 4.4.

Every type in a universe $\mathcal{U}$ is compact if and only if global choice holds for $\mathcal{U}$ (Definition 2.23).

Proof.

Assume global choice, let $X:\mathcal{U}$ and let $p:X\to\mathbf{2}$ . Then $\Sigma_{x:X}\,p\,x=0$ is a type in $\mathcal{U}$ , so it is decidable by global choice, which amounts to the compactness of $X$ . Conversely, if every type in $\mathcal{U}$ is compact then every type in $\mathcal{U}$ is decidable by Lemma 4.3. ∎

Global choice is not only constructively unacceptable, but also inconsistent with univalence [41, Corollary 3.2.7]. Nevertheless, in this paper we build many compact types in a constructive type theory compatible with univalence. We start from a trivial example and some basic, but important counterexamples.

Examples 4.5.

(1)

Every finite type is compact, a finite type being one of the form $\mathbf{1}+\cdots+\mathbf{1}$ , which includes the base case $\mathbf{0}$ in the obvious inductive definition.
(2)

$\mathbb{N}$ is compact if and only if $\mathrm{LPO}$ holds.
(3)

$\mathbb{N}$ is $\exists$ -compact if and only if $\mathrm{LPO}$ holds.
(4)

$\mathbb{N}$ is $\Pi$ -compact if and only if $\mathrm{WLPO}$ holds.

Compact types are closed under retracts, finite disjoint unions, images, and, when the index type is compact, under arbitrary sums (Section 4.3). Compactness, discreteness and total separatedness interact with function types much as their topological namesakes do, with arbitrary functions of type theory playing the role that continuous maps play in topology, but without any Brouwerian continuity axiom (Section 4.5). Under classical logic in the metatheory, the notions coincide with topological compactness in the model of simple types given by Kleene–Kreisel spaces [14, 29].

4.2. Compact pointed types

For reasons pertaining to constructivity, a number of definitions and theorems need to assume that the compact types under consideration are pointed. Moreover, it is convenient to work with the following characterization of compact pointed types, which we apply tacitly in the development that follows.

Lemma 4.6.

The following are equivalent for any type $X$ .

(1)

$X$ is compact and pointed.
(2)

For every $p:X\to\mathbf{2}$ we can find $x_{0}:X$ such that $p\,x_{0}=1$ implies $p\,x=1$ for all $x:X$ :

$\prod_{p:\mathbf{2}^{X}}\Sigma_{x_{0}:X}\,\big(p\,x_{0}=1\to\forall x.\,p\,x=1\big).$

We call such an $x_{0}$ a universal witness for $p$ . It is a root of $p$ if and only if $p$ has some root.

We call a function $\varepsilon:\mathbf{2}^{X}\to X$ assigning a universal witness to each $p$ a selection function for $X$ . In (2), a candidate root is produced before it is known whether a root exists.

Proof.

(1) implies (2). Let $X$ be compact and $x_{\star}:X$ , and let $p:X\to\mathbf{2}$ . By compactness, either $p$ has a root $x$ , and we take $x_{0}=x$ , so that the implication $p\,x_{0}=1\to\forall x.\,p\,x=1$ holds vacuously because $p\,x_{0}=0$ , or else $p\,x=1$ for every $x$ , and we take $x_{0}=x_{\star}$ , the conclusion of the implication being the assumption of this case.

(2) implies (1). Let $p:X\to\mathbf{2}$ , with universal witness $x_{0}$ . If $p\,x_{0}=0$ then $x_{0}$ is a root of $p$ . If $p\,x_{0}=1$ then $p\,x=1$ for every $x$ by the universality of $x_{0}$ . This is precisely the case distinction required by compactness. For pointedness, apply the hypothesis to e.g. the constantly $0$ predicate, which gives a point of $X$ .

A universal witness is a candidate root. With $x_{0}$ a universal witness for $p$ , one direction is trivial, since if $x_{0}$ is a root then $p$ has a root. For the other, suppose $p\,x=0$ for some $x$ . Then it is not the case that $p\,x^{\prime}=1$ for every $x^{\prime}$ , since that would give $p\,x=1$ , contradicting $p\,x=0$ . By the contrapositive of the universality of $x_{0}$ , we conclude $p\,x_{0}\neq 1$ and so $x_{0}$ is a root. ∎

Examples 4.7.

(1)

The type $\mathbf{2}$ is compact pointed, with a selection function given by $\varepsilon\,p=p\,0$ for any $p:\mathbf{2}^{\mathbf{2}}$ .
(2)

The type $\Omega_{\mathcal{U}}$ of propositions in a universe $\mathcal{U}$ is compact pointed too, despite excluded middle being undecided in our type theory.
(3)

The type $\mathbb{N}_{\infty}$ of Example 3.1 is an infinite compact type, with a root selection function $\varepsilon\,p=(n\mapsto\min\{p(\underline{k})\mid k\leq n\})$ (cf. Section 4.2). Moreover, $\varepsilon\,p$ is the infimum of the set of roots of $p$ , which may or may not be a root, but is a root if and only if $p$ has some root.

Proof.

For $\mathbf{2}$ , take $x_{0}=p\,0$ and suppose $p\,(p\,0)=1$ . We first get $p\,0=1$ by cases on $p\,0$ : it is immediate when $p\,0=1$ , and when $p\,0=0$ , substituting that equation into $p\,(p\,0)=1$ gives $p\,0=1$ , a contradiction. Substituting $p\,0=1$ into $p\,(p\,0)=1$ then gives $p\,1=1$ , so $p$ is constantly $1$ .

For $\Omega_{\mathcal{U}}$ , decide the value of $p\,\bot$ . If $p\,\bot=0$ , take $\bot$ as a universal witness, the implication holding vacuously. If $p\,\bot=1$ , take $\top$ , and we must show that if also $p\,\top=1$ then $p$ is constantly $1$ . Two maps $\Omega_{\mathcal{U}}\to\mathbf{2}$ that agree at $\bot$ and $\top$ agree everywhere, because the map $\mathbf{2}\to\Omega_{\mathcal{U}}$ is extremely dense (Lemma 2.22) and an extremely dense map into a $\neg\neg$ -separated type is right-cancellable (Lemma 2.21), while $\mathbf{2}$ is $\neg\neg$ -separated, being discrete. Applying this to $p$ and the map constantly $1$ gives $p\,P=1$ for every $P$ .

For $\mathbb{N}_{\infty}$ , see [15] or the companion formalization file [19]. ∎

4.3. Closure properties of compact types

Theorem 4.8.

(1)

The types $\mathbf{0}$ and $\mathbf{1}$ are compact, and so is every singleton.
(2)

If $X$ and $Y$ are compact, so is $X+Y$ .
(3)

If $X$ is compact and $Y\,x$ is compact for every $x:X$ , then $\Sigma\,Y$ is compact. In particular, the product $X\times Y$ is compact when both $X$ and $Y$ are.
(4)

If $Y$ is a retract of $X$ and $X$ is compact, then so is $Y$ . In particular, compactness is invariant under equivalence.
(5)

If $f:X\to Y$ is a surjection and $X$ is compact, then so is $Y$ , and hence so is the image of any map out of a compact type.

Proof.

By Lemma 4.2 we may take the given data to be a complemented family $A$ on the type under consideration rather than a $\mathbf{2}$ -valued predicate, so that the task is to decide the sum of $A$ .

Items (2), (4) and (5) follow one pattern, which we record first. If $f:X\to Y$ is a map and $A$ is a complemented family on $Y$ , then the composite $A\circ f$ is a complemented family on $X$ , and a point $(x,a)$ of $\Sigma\,(A\circ f)$ gives the point $(f\,x,a)$ of $\Sigma A$ . So when $X$ is compact, the sum of $A\circ f$ is decidable, and what remains is to show that $\Sigma A$ is empty in the case that $\Sigma\,(A\circ f)$ is. This is where the hypothesis on $f$ is used.

(1) The types $\mathbf{0}$ and $\mathbf{1}$ are decidable propositions, and so is any singleton, so this is an instance of Lemma 4.3.

(2) Apply the pattern to the injections $\mathrm{inl}:X\to X+Y$ and $\mathrm{inr}:Y\to X+Y$ , whose domains are compact by hypothesis. If either of $\Sigma\,(A\circ\mathrm{inl})$ and $\Sigma\,(A\circ\mathrm{inr})$ has a point, then so does $\Sigma A$ . If both are empty, then so is $\Sigma A$ , because every point of $X+Y$ is of the form $\mathrm{inl}\,x$ or $\mathrm{inr}\,y$ .

(3) For each $x:X$ , the family $y\mapsto A\,(x,y)$ on $Y\,x$ is complemented, and so the compactness of the fibers makes the family

B\,x\;:\equiv\;\textstyle\Sigma_{y:Y\,x}\,A\,(x,y)

on $X$ complemented. The compactness of $X$ then decides the sum of $B$ , which is the sum of $A$ up to reassociation, and decidability is invariant under logical equivalence. Binary products are the case of a constant family $Y$ .

(4) Apply the pattern to the retraction $r:X\to Y$ , whose section $s:Y\to X$ satisfies $r\,(s\,y)=y$ for every $y:Y$ . A point $(y,a)$ of $\Sigma A$ gives the point $(s\,y,a^{\prime})$ of $\Sigma\,(A\circ r)$ , where $a^{\prime}$ is obtained from $a$ by transport along $r\,(s\,y)=y$ , and so $\Sigma A$ is empty when $\Sigma\,(A\circ r)$ is. An equivalence is in particular a retraction.

(5) Apply the pattern to the surjection $f$ . If $\Sigma\,(A\circ f)$ is empty, then $\neg\,A\,(f\,x)$ holds for every $x:X$ , and hence $\neg\,A\,y$ holds for every $y:Y$ by surjection induction (Definition 2.9), which is available because negations are propositions. Therefore $\Sigma A$ is empty. The image of a map $g$ out of a compact type is covered by applying this to the corestriction of $g$ , which is a surjection. ∎

Proposition 4.9.

If $X$ is compact, then so is its totally separated reflection $\mathbb{T}\,X$ constructed in Theorem 3.15.

Proof.

The reflector $\eta^{\mathbb{T}}$ is a surjection (Theorem 3.15(1)), and compactness passes to surjective images (Theorem 4.8(5)). ∎

Corollary 4.10.

Pointed compactness is closed under

(1)

retracts, and hence equivalence ,
(2)

sums, and hence binary products and coproducts ,
(3)

surjective images .

Proof.

A compact pointed type is a compact type with a point (Lemma 4.6), and each of the three constructions preserves compactness by Theorem 4.8. What remains is to produce a point in each case.

(1) A retraction $X\to Y$ sends a point of $X$ to a point of $Y$ , and an equivalence is in particular a retraction.

(2) A point $x$ of the base together with a point of the fiber $Y\,x$ is a point of $\Sigma\,Y$ . Binary products are the case of a constant family. Binary coproducts are compact by Theorem 4.8(2), and a point $x$ of $X_{0}$ gives the point $\mathrm{inl}\,x$ of $X_{0}+X_{1}$ .

(3) A surjection $X\to Y$ sends a point of $X$ to a point of $Y$ . ∎

Proposition 4.11.

Let $X$ be a compact type.

(1)

If $A$ is a complemented, proposition valued family on $X$ , then the subtype $\Sigma_{x:X}\,A\,x$ is compact.
(2)

If $A$ and $B$ are families on $X$ and $\prod_{x:X}\,(A\,x+B\,x)$ holds, then we can decide between $\Sigma_{x:X}\,A\,x$ and $\prod_{x:X}\,B\,x$ .
(3)

If $A$ is a complemented family on $X$ and $\Sigma_{x:X}\,A\,x$ is non-empty, then it is pointed.

Proof.

(1) Let $B$ be a complemented family on the subtype $\Sigma_{x:X}\,A\,x$ , so that what has to be decided is the sum of $B$ . The family

C\,x\;:\equiv\;\textstyle\Sigma_{a:A\,x}\,B\,(x,a)

on $X$ is complemented. Indeed, decide $A\,x$ . If $A\,x$ is empty then so is $C\,x$ . If $a:A\,x$ , decide $B\,(x,a)$ . A point $b$ of $B\,(x,a)$ gives the point $(a,b)$ of $C\,x$ , and if $B\,(x,a)$ is empty then so is $C\,x$ , because $A\,x$ is a proposition, so that any $a^{\prime}:A\,x$ is equal to $a$ and a point of $B\,(x,a^{\prime})$ transports to a point of $B\,(x,a)$ . The compactness of $X$ now decides the sum of $C$ , which is the sum of $B$ up to reassociation.

(2) Write $q$ for the given point of $\prod_{x:X}\,(A\,x+B\,x)$ and let $p:X\to\mathbf{2}$ be its indicator, with $p\,x=0$ when $q\,x$ lands in $A\,x$ and $p\,x=1$ when it lands in $B\,x$ . The compactness of $X$ decides whether $p$ has a root. A root $x$ comes with a point of $A\,x$ , and so gives a point of $\Sigma_{x:X}\,A\,x$ . If there is no root, then $p\,x=1$ , and hence $B\,x$ , for every $x$ .

(3) The compactness of $X$ decides the sum of $A$ , and a decidable type is $\neg\neg$ -stable. ∎

Remark 4.12.

Tychonoff’s theorem in classical topology says that arbitrary products of compact spaces are compact. In our case, Theorem 4.8(3) gives this for binary, and hence finite, products of compact types. Without further axioms, it is not possible to prove an infinite generalization in our type theory, not even a countable one. With our type theoretical counterparts of the topological notions, the compactness of the Cantor type $\mathbf{2}^{\mathbb{N}}$ , the countable product of copies of $\mathbf{2}$ , is independent, as it holds in the topological topos and in the Kleene–Vesley topos [48], but fails in the effective topos [26] due to the presence of Kleene trees (infinite binary trees with no computable paths, which give recursive counterexamples to König’s Lemma and hence the compactness of the Cantor space [30]).

4.4. $\exists$ -compactness and $\Pi$ -compactness

Proposition 4.13.

(1)

Each of $\exists$ -compactness and $\Pi$ -compactness is a proposition.
(2)

Any compact type is $\exists$ -compact.
(3)

Any $\exists$ -compact type is $\Pi$ -compact.
(4)

If $X$ is $\exists$ -compact then $\exists_{x:X}\,p\,x=0$ is $\neg\neg$ -stable.
(5)

A type $X$ is $\Pi$ -compact if and only if the constant map $\lambda x.\,1$ is isolated in $\mathbf{2}^{X}$ .
(6)

A type $X$ is $\exists$ -compact, respectively $\Pi$ -compact, if and only if its totally separated reflection $\mathbb{T}\,X$ constructed in Theorem 3.15 is.

Proof.

(1) For each $p$ , the types $\exists_{x}p\,x=0$ and $\prod_{x}p\,x=1$ are propositions, and so is the decidability of a proposition.

(2) Compactness gives, for each predicate $p$ , either a root, whose truncation gives $\exists_{x}p\,x=0$ , or a proof that $p$ is constantly $1$ , which refutes it.

(3) Decide $\exists_{x}p\,x=0$ . In the positive case, $\prod_{x}p\,x=1$ is refuted, because a root of $p$ contradicts it, and this conclusion, being a negation, may be drawn from the truncated existence. In the negative case, no $x$ has $p\,x=0$ , and hence $p\,x=1$ for every $x$ , as $\mathbf{2}$ has only two points.

(4) The proposition $\exists_{x}p\,x=0$ is decidable, and hence $\neg\neg$ -elimination is applicable to get $\neg\neg$ -stability.

(5) The $\Pi$ -compactness of $X$ says that $\prod_{x}p\,x=1$ is decidable for every $p$ , while the isolatedness of $\lambda x.\,1$ says that $p=\lambda x.\,1$ is decidable for every $p$ . The type $\prod_{x}p\,x=1$ is pointwise equality of $p$ with the constant map, so the two types are equivalent and decidability is invariant under logical equivalence.

(6) Let $q$ and $p=q\circ\eta^{\mathbb{T}}$ be corresponding predicates on $\mathbb{T}\,X$ and on $X$ , using Theorem 3.15(2) with $A=\mathbf{2}$ . Decidability transfers along a logical equivalence, so it is enough to prove

\exists_{x:X}\,p\,x=0\iff\exists_{y:\mathbb{T}\,X}\,q\,y=0,\qquad\prod_{x:X}\,p\,x=1\iff\prod_{y:\mathbb{T}\,X}\,q\,y=1.

A root $x$ of $p$ gives the root $\eta^{\mathbb{T}}\,x$ of $q$ . Conversely, the reflector is a surjection, so a root of $q$ has a preimage in an unspecified way, and any such preimage is a root of $p$ . If $q\,y=1$ for every $y$ , then $p\,x=1$ for every $x$ by composition with the reflector. Conversely, if $p\,x=1$ for every $x$ , then $q\,y=1$ for every $y$ by surjection induction along the reflector, the equations being propositions. ∎

The following are some closure properties of the two weaker notions of compactness.

Proposition 4.14.

(1)

Both $\exists$ -compactness and $\Pi$ -compactness pass to surjective images, and hence to retracts.
(2)

If $X$ is $\Pi$ -compact and $Y\,x$ is $\Pi$ -compact for every $x:X$ , then the sum $\Sigma\,Y$ is $\Pi$ -compact.
(3)

Both notions pass to complemented subtypes.

Proof.

(1) Let $f:X\to Y$ be a surjection and let $q:Y\to\mathbf{2}$ , and apply the compactness hypothesis on $X$ to the predicate $q\circ f$ .

For $\exists$ -compactness, a root of $q\circ f$ gives a root of $q$ , and so the truncated existence of the former gives that of the latter. If $q\circ f$ has no root, then neither has $q$ , because a root of $q$ has a preimage under $f$ in an unspecified way, and that preimage is a root of $q\circ f$ . This conclusion, being a negation, may be drawn from the truncated existence.

For $\Pi$ -compactness, if $q\,(f\,x)=1$ for every $x:X$ , then $q\,y=1$ for every $y:Y$ by surjection induction along $f$ , the equations being propositions, and conversely by composition with $f$ . So the two universal statements are logically equivalent, and decidability transfers along a logical equivalence.

Images are the case of the corestriction, which is a surjection, and a retraction is a surjection.

(2) Let $p:\Sigma\,Y\to\mathbf{2}$ . For each $x:X$ , the $\Pi$ -compactness of the fiber $Y\,x$ decides $\prod_{y}p\,(x,y)=1$ , and so there is a predicate $q:X\to\mathbf{2}$ with $q\,x=1$ if and only if $\prod_{y}p\,(x,y)=1$ . The $\Pi$ -compactness of $X$ decides $\prod_{x}q\,x=1$ , which is logically equivalent to $\prod_{x}\prod_{y}p\,(x,y)=1$ , and this is $\prod_{(x,y)}p\,(x,y)=1$ after currying.

(3) Let $S$ be a complemented subset of $X$ , with subtype $\Sigma_{x:X}\,x\in S$ .

If $X$ is $\exists$ -compact, apply $\exists$ -compactness to the characteristic function of $S$ , which decides whether the subtype is inhabited. If it is not, then the subtype is empty, and an empty type is $\exists$ -compact. If it is, then a point of the subtype makes it a retract of $X$ , the points outside $S$ being sent to that point, and so the subtype is $\exists$ -compact by (1). This conclusion may be drawn from the inhabitedness of the subtype, because $\exists$ -compactness is a proposition (Proposition 4.13(1)).

If $X$ is $\Pi$ -compact, a predicate on the subtype extends to a predicate on $X$ that takes the value $1$ outside $S$ , and the extension is constantly $1$ if and only if the given predicate is. So the $\Pi$ -compactness of $X$ decides whether the extension is constantly $1$ , and hence whether the given predicate is. ∎

Proposition 4.15.

(1)

A proposition is $\exists$ -compact if and only if it is decidable.
(2)

The truncation $\|X\|$ of an $\exists$ -compact type $X$ is decidable.
(3)

A non-empty $\exists$ -compact type is inhabited.
(4)

A $\Pi$ -compact type has decidable negation.

Proof.

(1) and (2) Apply $\exists$ -compactness to the constantly $0$ predicate. Every point of $X$ is a root of it, so that what is decided is the truncation $\|X\|$ , which gives (2). When $X$ is a proposition, the truncation is equivalent to $X$ , and so an $\exists$ -compact proposition is decidable. Conversely, a decidable proposition is $\exists$ -compact, by the argument of Lemma 4.3 with $\exists$ in place of $\Sigma$ .

(3) The truncation $\|X\|$ is decidable by (2). Its negation is logically equivalent to $\neg X$ , which is ruled out by the non-emptiness of $X$ , and so the truncation holds, which says that $X$ is inhabited.

(4) Apply $\Pi$ -compactness to the constantly $0$ predicate. What is decided is $\prod_{x}0=1$ , which is logically equivalent to $\neg X$ , because the type $0=1$ is empty. ∎

The following truncated form of Lemma 4.6(2), being a product of propositions, is a proposition.

Proposition 4.16.

The following are equivalent for any type $X$ .

(1)

$X$ is $\exists$ -compact and inhabited.
(2)

Every $p:\mathbf{2}^{X}$ has a universal witness in an unspecified way:

$\textstyle\prod_{p:\mathbf{2}^{X}}\,\exists_{x_{0}:X}\,\big(p\,x_{0}=1\to\forall x.\,p\,x=1\big).$

Moreover, the type $X$ is $\exists$ -compact if and only if it is empty or satisfies (2).

Proof.

(2) implies (1). Taking $p$ constantly $0$ gives a point of $X$ in an unspecified way, so that $X$ is inhabited. For $\exists$ -compactness, let $p:X\to\mathbf{2}$ and let $x_{0}$ be a universal witness for $p$ , available in an unspecified way. Deciding the value of $p\,x_{0}$ either produces a root of $p$ or shows that $p$ is constantly $1$ , and so decides $\exists_{x}p\,x=0$ . This decision may be made under the truncation, because the decidability of a proposition is a proposition.

(1) implies (2). Let $p:X\to\mathbf{2}$ . By $\exists$ -compactness, either $p$ has a root in an unspecified way, and that root is a universal witness, the implication holding vacuously, or $p$ is constantly $1$ , and then any point of $X$ is a universal witness, one being available in an unspecified way from the inhabitedness of $X$ .

The final claim. An $\exists$ -compact type has decidable truncation by Proposition 4.15(2), and so is either inhabited, in which case it satisfies (2) by the equivalence just proved, or empty. Conversely, a type satisfying (2) is $\exists$ -compact by that equivalence, and so is an empty type, no predicate on it having a root. ∎

Proposition 4.17.

A type $X$ is $\Pi$ -compact if and only if every $p:X\to\mathbf{2}$ has an infimum, that is, a greatest $n:\mathbf{2}$ such that $n\leq p\,x$ for every $x:X$ .

Proof.

Let $X$ be $\Pi$ -compact and let $p:X\to\mathbf{2}$ . Decide whether $p$ is constantly $1$ . If it is, then $1$ is a lower bound of its values, and it is the greatest element of $\mathbf{2}$ , so that it is the infimum. If it is not, then $0$ is a lower bound, being the least element of $\mathbf{2}$ , and $1$ is not a lower bound, as that would make $p$ constantly $1$ , so that $0$ is the infimum.

Conversely, suppose that every $p:X\to\mathbf{2}$ has an infimum, and consider the two possible values of $\inf p$ . If it is $1$ , then $1\leq p\,x$ , and hence $p\,x=1$ , for every $x$ . If it is $0$ , then $p$ is not constantly $1$ , because that would make $1$ a lower bound of its values and so force $1\leq\inf p$ . ∎

The infimum operator sends $p$ to a boolean $\inf p$ that is $1$ precisely when $p$ has value $1$ everywhere, so that it defines a boolean universal quantifier $\mathsf{A}:\mathbf{2}^{X}\to\mathbf{2}$ with $\mathsf{A}\,p=\inf p$ . This is compactness in the sense of synthetic topology with dominance $\mathbf{2}$ . In fact, writing $\mathsf{K}:\mathbf{2}\to\mathbf{2}^{X}$ for the map sending a boolean to the constant predicate at it, an infimum operator is precisely an order theoretic right adjoint $\mathsf{A}$ to $\mathsf{K}$ , since the adjunction says that $\mathsf{K}\,n\leq p$ pointwise if and only if $n\leq\mathsf{A}\,p$ , which is to say that $\mathsf{A}\,p$ is the greatest lower bound of the values of $p$ .

In classical topology a space $X$ is compact if and only if every projection $Y\times X\to Y$ is a closed map. The notion appropriate here is that of a clopen map, one sending complemented subsets to complemented subsets, with the image of a subset along a map as in Definition 2.13.

Proposition 4.18.

A type $X$ is $\exists$ -compact if and only if every projection $Y\times X\to Y$ is a clopen map.

Proof.

Let $X$ be $\exists$ -compact, let $p:Y\times X\to\mathbf{2}$ be the characteristic function of a complemented subset, and let $y:Y$ . Membership of $y$ in the image of that subset along the projection amounts to $\exists_{x:X}\,p\,(y,x)=0$ , which $\exists$ -compactness decides.

Conversely, take $Y$ to be the one-element type and let $p:X\to\mathbf{2}$ . Consider the subset of $\mathbf{1}\times X$ with characteristic function $p\circ\mathrm{pr}_{2}$ . Membership of the point of $\mathbf{1}$ in the image of that subset along the projection $\mathbf{1}\times X\to\mathbf{1}$ amounts to $\exists_{x:X}\,p\,x=0$ , so that the clopenness of this single projection gives the $\exists$ -compactness of $X$ . ∎

4.5. Interplay between the notions

We collect results that combine compactness, discreteness and total separatedness.

Lemma 4.19.

If $Y\,x$ is compact for every $x:X$ and the point $(x,y)$ of $\Sigma\,Y$ is isolated, then $x$ is isolated.

Proof.

Let $x^{\prime}:X$ , so that what has to be decided is $x=x^{\prime}$ . The family

A\,y^{\prime}:\equiv\big((x,y)=(x^{\prime},y^{\prime})\big)

on $Y\,x^{\prime}$ is complemented, because $(x,y)$ is isolated, and so the compactness of $Y\,x^{\prime}$ decides the sum of $A$ . If some $y^{\prime}$ has $(x,y)=(x^{\prime},y^{\prime})$ , then $x=x^{\prime}$ by taking first components. If none does, then $x\neq x^{\prime}$ , because an identification $x=x^{\prime}$ would give such a $y^{\prime}$ by transporting $y$ along it. ∎

Proposition 4.20.

(1)

If $X$ is $\Pi$ -compact and $Y\,x$ is discrete for every $x:X$ , then $\prod_{x}Y\,x$ is discrete.
(2)

If $X$ is compact, the discreteness of $\prod_{x}Y\,x$ can be strengthened to $\big(\Sigma_{x:X}\,f\,x\neq g\,x\big)+\big(f=g\big)$ for all $f,g:\prod_{x}Y\,x$ .

Proof.

Given $f,g:\prod_{x}Y\,x$ , the discreteness of each $Y\,x$ decides $f\,x=g\,x$ , so there is an indicator $p:X\to\mathbf{2}$ with $p\,x=0$ if $f\,x\neq g\,x$ and $p\,x=1$ otherwise.

(1) $\Pi$ -compactness decides whether $p\,x=1$ for every $x$ , which amounts to deciding $f=g$ , by function extensionality.

(2) Compactness decides whether $p$ has a root, and a root of $p$ is a point $x$ with $f\,x\neq g\,x$ , and the absence of one gives $f\,x=g\,x$ everywhere, and hence $f=g$ . ∎

Example 4.21.

The principle $\mathrm{WLPO}$ , the $\Pi$ -compactness of $\mathbb{N}$ (Examples 4.5(4)), gives the discreteness of the Cantor type $\mathbf{2}^{\mathbb{N}}$ by Proposition 4.20(1). Together with Examples 3.13(3), this makes the discreteness of $\mathbf{2}^{\mathbb{N}}$ equivalent to $\mathrm{WLPO}$ .

Definition 4.22 (Disconnectedness).

A type $X$ is disconnected if $\mathbf{2}$ is a retract of it, or, equivalently, if some $p:X\to\mathbf{2}$ takes both values.

Proposition 4.20 has a partial converse.

Proposition 4.23.

If $Y$ is disconnected and $Y^{X}$ is discrete, then $X$ is $\Pi$ -compact.

Proof.

Take first $Y=\mathbf{2}$ . The $\Pi$ -compactness of $X$ is the isolatedness of the constant map $\lambda x.\,1$ in $\mathbf{2}^{X}$ (Proposition 4.13(5)), and in a discrete type every point is isolated. A disconnected $Y$ comes with a retraction onto $\mathbf{2}$ , and composing with it and with its section makes $\mathbf{2}^{X}$ a retract of $Y^{X}$ , and discreteness passes to retracts (Proposition 3.6(2)). ∎

Proposition 4.24.

Let $Y$ be disconnected.

(1)

If $X$ is totally separated and $Y^{X}$ is $\Pi$ -compact, then $X$ is discrete.
(2)

For arbitrary $X$ , if $Y^{X}$ is $\Pi$ -compact, then the totally separated reflection $\mathbb{T}\,X$ of Theorem 3.15 is discrete.

Proof.

(1) Take first $Y=\mathbf{2}$ , and let $x,y:X$ . Since $\mathbf{2}$ is discrete, there is a map $q:\mathbf{2}^{X}\to\mathbf{2}$ with $q\,p=1$ when $p\,x=p\,y$ and $q\,p=0$ when the two values differ. Applying the $\Pi$ -compactness of $\mathbf{2}^{X}$ to $q$ decides $\prod_{p}q\,p=1$ , which says that $x$ and $y$ agree at every $\mathbf{2}$ -valued predicate, that is, that $x=_{2}y$ . If $x=_{2}y$ , then $x=y$ by total separatedness, and if not, then $x\neq y$ , because $x=y$ would give $p\,x=p\,y$ for every $p$ . So $X$ is discrete.

For a disconnected $Y$ , a retraction of $Y$ onto $\mathbf{2}$ makes $\mathbf{2}^{X}$ a retract of $Y^{X}$ , and $\Pi$ -compactness passes to retracts (Proposition 4.14(1)), so that the case just proved applies.

(2) A retraction of $Y$ onto $\mathbf{2}$ makes $\mathbf{2}^{X}$ a retract of $Y^{X}$ , as in (1), and $\mathbf{2}^{\mathbb{T}\,X}$ is equivalent to $\mathbf{2}^{X}$ because $X$ and $\mathbb{T}\,X$ have the same $\mathbf{2}$ -valued predicates (Theorem 3.15(2) with $A=\mathbf{2}$ ). So $\mathbf{2}^{\mathbb{T}\,X}$ is a retract of $Y^{X}$ and hence $\Pi$ -compact (Proposition 4.14(1)). Now apply (1) to $\mathbb{T}\,X$ , which is totally separated (Theorem 3.15(1)). ∎

Examples 4.25.

The results of this subsection show that some types fail to be compact constructively.

(1)

A $\Pi$ -compact simple type (Examples 3.13(2)) gives $\mathrm{WLPO}$ .
(2)

The $\Pi$ -compactness of $\mathbf{2}^{\mathbb{N}_{\infty}}$ gives $\mathrm{WLPO}$ .

Proof.

(1) The type $\mathbb{N}$ is a retract of every simple type (Examples 3.13(2)), and $\Pi$ -compactness is inherited by retracts (Proposition 4.14 (1)), so $\mathbb{N}$ is $\Pi$ -compact, which is $\mathrm{WLPO}$ (Examples 4.5(4)).

(2) The type $\mathbb{N}_{\infty}$ is totally separated, being a retract of $\mathbf{2}^{\mathbb{N}}$ (Example 3.1), which is totally separated (Examples 3.13(3)), and total separatedness passing to retracts (Proposition 3.12(1)), so Proposition 4.24(1) turns the $\Pi$ -compactness of $\mathbf{2}^{\mathbb{N}_{\infty}}$ into the discreteness of $\mathbb{N}_{\infty}$ , which is $\mathrm{WLPO}$ (Examples 3.3(3)). ∎

4.6. The micro-Tychonoff theorem

We now formulate and prove the smallest possible instance of Tychonoff’s theorem for our notion of compactness (cf. Remark 4.12) by restricting the index type to be a subsingleton and the indexed compact types to be pointed. A crucial application is the compactness of extended sums (Theorem 4.32), on which the main results of Sections 6 and 7 are based.

Theorem 4.26 (Micro-Tychonoff).

If $X$ is a proposition and $Y\,x$ is compact pointed for every $x:X$ , then $\prod_{x}Y\,x$ is compact pointed.

Proof.

Let $X$ be a proposition, let $\varepsilon_{x}$ be a selection function witnessing that $Y\,x$ is compact pointed for each $x:X$ , and let $p:\prod_{x}Y\,x\to\mathbf{2}$ . For each $x:X$ , evaluation at $x$ ,

f_{x}:\textstyle\prod_{x^{\prime}}Y\,x^{\prime}\to Y\,x,\qquad f_{x}\,\varphi=\varphi\,x,

is an equivalence, because a product indexed by a proposition is the value at any point of that proposition. Carry the predicate across by setting $q_{x}\,y=p\,(f_{x}^{-1}\,y)$ , and define the candidate witness pointwise:

\varphi_{0}\,x\;=\;\varepsilon_{x}\,q_{x}.

We claim $\varphi_{0}$ is a universal witness for $p$ . So assume $p\,\varphi_{0}=1$ , and we must show $p\,\varphi=1$ for an arbitrary $\varphi$ .

(1) The conclusion follows from $X$ . Suppose $x:X$ . The universality of $\varphi_{0}\,x$ for $q_{x}$ says that $p\,(f_{x}^{-1}(\varphi_{0}\,x))=1$ implies $p\,(f_{x}^{-1}\,y)=1$ for every $y:Y\,x$ . Since $f_{x}\,\varphi_{0}=\varphi_{0}\,x$ and $f_{x}^{-1}$ is a section of $f_{x}$ , the hypothesis is our assumption $p\,\varphi_{0}=1$ . Instantiating $y=\varphi\,x$ and using $f_{x}^{-1}(\varphi\,x)=\varphi$ , we get $p\,\varphi=1$ . This conclusion no longer mentions the point $x$ , so that $X\to p\,\varphi=1$ .

(2) The conclusion also follows from $\neg X$ . If $X$ is empty then any two points of $\prod_{x}Y\,x$ are equal, in particular $\varphi=\varphi_{0}$ , and so $p\,\varphi=p\,\varphi_{0}=1$ .

(3) Combining (1) and (2). Excluded middle, if it were available, would now finish the argument, since $X$ is a proposition, but it is not needed. Suppose $p\,\varphi=0$ . Then $p\,\varphi\neq 1$ , so contraposing (1) gives $\neg X$ , and then (2) gives $p\,\varphi=1$ . Thus $p\,\varphi=0$ implies $p\,\varphi=1$ . The value of $p\,\varphi$ is $0$ or $1$ , and in the first case it is also $1$ , so $p\,\varphi=1$ . ∎

Specializing to a constant family, this says that $Y^{X}$ is compact pointed for any proposition $X$ and any type $Y$ such that the pointedness of $X$ implies the compact pointedness of $Y$ , whether or not $X$ holds.

Example 4.27.

The function type $\mathbb{N}^{\mathrm{LPO}}$ is compact pointed. Indeed $\mathrm{LPO}$ is a proposition that implies the compact pointedness of $\mathbb{N}$ , so Theorem 4.26 applies. The exponential is compact whether or not $\mathrm{LPO}$ holds, even though the compactness of $\mathbb{N}$ is $\mathrm{LPO}$ itself, which is independent of our type theory (Examples 4.5(2)).

Remark 4.28.

(1)

The proof of Theorem 4.26 does not go through the equivalence $\prod_{x}Y\,x\simeq Y\,x_{0}$ , which holds once a point $x_{0}:X$ is given and would transfer compact pointedness directly. Such a point is at hand only under the hypothesis that $X$ holds, whereas the universal witness has to be produced without deciding $X$ .
(2)

The pointedness hypothesis is essential, since the corresponding statement for plain compactness fails constructively. Indeed, take $Y\,x:\equiv\mathbf{0}$ , which is compact but not pointed. Then $\prod_{x}Y\,x$ is $\neg X$ , so the unpointed statement would make $\neg X$ compact, and hence decidable (Lemma 4.3), for every proposition $X$ , which is the principle of weak excluded middle. Pointedness enters the proof of Theorem 4.26 in the definition of $\varphi_{0}$ , which has to be a point of $\prod_{x}Y\,x$ whether or not $X$ holds, and plain compactness provides no such point.

The hypothesis on the index type can be generalized from a proposition to a subtype of a finite type, because such a subtype is a finite sum of propositions.

Corollary 4.29.

Let $F$ be a finite type and $j:X\hookrightarrow F$ an embedding. If the type $Y\,x$ is compact pointed for every $x:X$ , then so is $\prod_{x}Y\,x$ .

Proof.

The embedding decomposes $X$ as the sum of its fibers, and currying the product over that sum gives

\textstyle\prod_{x:X}Y\,x\;\simeq\;\prod_{i:F}\ \prod_{w:j^{-1}(i)}Y\,(\mathrm{pr}_{1}w).

Each fiber is a proposition, $j$ being an embedding, so each inner product is compact pointed by Theorem 4.26. The outer product is a finite product of compact pointed types, which is compact pointed by Corollary 4.10(2), and pointed compactness is invariant under equivalence (Corollary 4.10(1)). ∎

4.7. Extension of families of compact types along embeddings

The above closure properties of compact types allow us to construct new compact types starting from examples such as finite types and $\mathbb{N}_{\infty}$ . However, they do not reach far. To construct more compact types, we develop a generalization of a certain squashed sum constructed in [15], with the aid of the theory of algebraically injective types developed in [18]. It works by extending a family of types along an embedding and then summing the extended family. The extension operation witnesses the algebraic injectivity of the universe, and what makes the sum compact is that the fibers of an embedding are propositions, so that the micro-Tychonoff Theorem 4.26 is applicable.

Definition 4.30 ( $\Pi$ -extension).

Let $Y:X\to\mathcal{U}$ be a family of types and $j:X\to K$ an arbitrary map. The $\Pi$ -extension of $Y$ along $j$ is the family $Y\mathbin{/}j:K\to\mathcal{U}$ given by

(Y\mathbin{/}j)\,k\;:\equiv\;\prod_{(x,p)\,:\,j^{-1}(k)}Y\,x,

where $j^{-1}(k):\equiv\Sigma_{x:X}(j\,x=k)$ is the fiber of $j$ over $k$ .

This is illustrated by the following diagram, with the general case on the left, used in Section 7, and the special case of the embedding $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ on the right, used in Section 6:

The point of the above construction is that we can extend $Y$ from $\mathbb{N}$ to $\mathbb{N}_{\infty}$ without checking whether the argument of the desired extension $Y\mathbin{/}\iota$ is $\infty$ or not, which is not available in our constructive setting, as it amounts to $\mathrm{WLPO}$ (Examples 3.3(5)).

Lemma 4.31.

Let $Y:X\to\mathcal{U}$ and $j:X\to K$ .

(1)

If $j$ is an embedding, the $\Pi$ -extension restricts back to $Y$ along $j$ up to type equivalence: for every $x:X$ we have $(Y\mathbin{/}j)(j\,x)\simeq Y\,x$ .
(2)

If $j\,x\neq k$ for every $x:X$ , then $(Y\mathbin{/}j)\,k\simeq\mathbf{1}$ .

Proof.

(1) If $j$ is an embedding then $j^{-1}(j\,x)$ is a proposition, and it contains the point $(x,\mathrm{refl})$ , so it is a singleton. A product indexed by a singleton is equivalent to its value at the center, whence $(Y\mathbin{/}j)(j\,x)\simeq Y\,x$ .

(2) If $j\,x\neq k$ for every $x:X$ then $j^{-1}(k)$ is empty, and a product indexed by the empty type is equivalent to the type $\mathbf{1}$ . ∎

We refer to the sum $\Sigma(Y\mathbin{/}j)$ of the family as the extended sum of the family $Y$ .

Theorem 4.32 (Compactness of extended sums).

For any embedding $j:X\to K$ into a compact pointed type and any family $Y:X\to\mathcal{U}$ of compact pointed types, the extended sum $\Sigma(Y\mathbin{/}j)$ is compact pointed.

Proof.

By the closure of pointed compactness under $\Sigma$ (Corollary 4.10(2)) applied to the family $Y\mathbin{/}j$ over the compact pointed base $K$ , it suffices to show that $(Y\mathbin{/}j)\,k$ is compact pointed for every $k:K$ . By definition this is the product of the types $Y\,x$ over the index type $j^{-1}(k)$ , all of which are compact pointed by hypothesis, and $j^{-1}(k)$ is a proposition precisely because $j$ is an embedding. So the micro-Tychonoff Theorem 4.26 applies. ∎

Remark 4.33.

Theorem 4.32 is a type theoretic generalization of the fact that the squashed sum constructed in [15, Section 10] produces compact sets. In loc. cit., given countably many compact pointed subsets $X_{n}\subseteq\mathbf{2}^{\mathbb{N}}$ , we rescaled $X_{n}$ by prefixing the finite sequence $1^{n}0$ , making the pieces disjoint, smaller in diameter, close together, and converging to the point $\infty=1^{\omega}$ as $n$ increases, and defined their squashed sum to be the set of those $\alpha$ such that if $1^{n}0$ is a prefix of $\alpha$ then $\alpha\in 1^{n}0X_{n}$ . This set is the closure of $\bigcup_{n}1^{n}0X_{n}$ , which classically is this union together with $\{\infty\}$ . Constructively, it can be described as the union of the $\mathbb{N}_{\infty}$ -indexed family

Y_{x}=\{\alpha\in\mathbf{2}^{\mathbb{N}}\mid\forall n\in\mathbb{N}\,(x=n\Rightarrow\alpha\in 1^{n}0X_{n})\text{ and }(x=\infty\Rightarrow\alpha=\infty)\}.

The defining formula for $Y_{x}$ corresponds to the $\Pi$ -extension formula of Definition 4.30, for the family $n\mapsto 1^{n}0X_{n}$ along the embedding $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ . Thus, the extended sum generalizes the squashed sum to any embedding $X\hookrightarrow K$ into a compact pointed type and any $X$ -indexed family of compact pointed types.

Lemma 4.34.

For any map $j:X\to K$ , not necessarily an embedding, and any family $Y:X\to\mathcal{U}$ of totally separated types, the type $(Y\mathbin{/}j)\,k$ is totally separated for every $k:K$ .

Proof.

The type $(Y\mathbin{/}j)\,k$ is the product of the types $Y\,x$ over the index type $j^{-1}(k)$ , each of which is totally separated by hypothesis, and total separatedness is closed under arbitrary products (Proposition 3.12). ∎

Lemma 4.35.

For any map $j:X\to K$ and any families $Y,Z:X\to\mathcal{U}$ such that $Y\,x$ is a retract of $Z\,x$ for every $x:X$ ,

(1)

the type $(Y\mathbin{/}j)\,k$ is a retract of $(Z\mathbin{/}j)\,k$ for every $k:K$ ,
(2)

the extended sum $\Sigma\,(Y\mathbin{/}j)$ is a retract of the extended sum $\Sigma\,(Z\mathbin{/}j)$ .

Proof.

(1) By Definition 4.30, the two types are products over the index type $j^{-1}(k)$ , and a product of retractions is a retraction of the corresponding products, the retraction and the section acting pointwise. (2) follows by Lemma 2.29(4), applied to the identity on $K$ and to the retractions of (1). ∎

Classically, every point of $\mathbf{2}^{\mathbb{N}}$ is of one of the forms $1^{n}0\alpha$ , with $\alpha:\mathbf{2}^{\mathbb{N}}$ , or $1^{\omega}$ . The following gives a constructive version of this.

Lemma 4.36 (Delayed binary sequences).

(1)

The extended sum of the constant family at $\mathbf{2}^{\mathbb{N}}$ along the embedding $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ is the type of delayed binary sequences, consisting of a time $u:\mathbb{N}_{\infty}$ together with a binary sequence made available when $u$ is finite,

$\textstyle\Sigma_{u\,:\,\mathbb{N}_{\infty}}\,\big(\text{$u$ is finite}\to\mathbf{2}^{\mathbb{N}}\big).$
(2)

This type is equivalent to $\mathbf{2}^{\mathbb{N}}$ .

Proof.

(1) By Definition 4.30, the extension of the constant family at $\mathbf{2}^{\mathbb{N}}$ along the embedding $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ evaluates at a point $u:\mathbb{N}_{\infty}$ to the type of functions from the fiber $\iota^{-1}(u)$ to $\mathbf{2}^{\mathbb{N}}$ , so that the extended sum is the sum of these function types over $u:\mathbb{N}_{\infty}$ . A point of the fiber is a natural number $n$ together with an identification $\underline{n}=u$ , which is what it means for $u$ to be finite (Example 3.1).

(2) In one direction, we define a map

\mathrm{Cons}\;:\;\big(\textstyle\Sigma_{u\,:\,\mathbb{N}_{\infty}}\,\big(\text{$u$ is finite}\to\mathbf{2}^{\mathbb{N}}\big)\big)\to\mathbf{2}^{\mathbb{N}}.

A delayed binary sequence is encoded as the run of $1$ s prescribed by its time, followed by a $0$ and the delayed value. A conatural number is either $\underline{0}$ or the result of prefixing a $1$ to a conatural number, decided by its first digit, and a binary sequence is a digit followed by a binary sequence, so that corecursion on $\mathbf{2}^{\mathbb{N}}$ defines $\mathrm{Cons}$ by the two clauses: the sequence $\mathrm{Cons}(\underline{0},\pi)$ begins with $0$ and continues as $\pi$ applied to the witness that $\underline{0}$ is finite, and, for $u$ prefixing a $1$ to $v$ , the sequence $\mathrm{Cons}(u,\pi)$ begins with $1$ and continues as $\mathrm{Cons}(v,\pi^{\prime})$ , where $\pi^{\prime}$ is $\pi$ composed with the passage from finiteness of $v$ to finiteness of $u$ .

In the other direction, we first define two maps

\begin{array}[]{lll}\mathrm{Head}&:&\mathbf{2}^{\mathbb{N}}\to\mathbb{N}_{\infty}\\ \mathrm{Tail}&:&\textstyle\prod_{\alpha:\mathbf{2}^{\mathbb{N}}}\,\big(\text{$\mathrm{Head}\,\alpha$ is finite}\to\mathbf{2}^{\mathbb{N}}\big)\end{array}

as follows. A binary sequence is turned into a delayed one by taking its initial run of $1$ s as the time and what follows as the delayed value. For a sequence $\alpha$ , let $\mathrm{Head}\,\alpha$ be that initial run, read as a conatural number and defined by the final-coalgebra presentation of Example 3.1: it is $\underline{0}$ when $\alpha$ begins with $0$ , and it prefixes a $1$ to the head of the tail of $\alpha$ when $\alpha$ begins with $1$ . When $\mathrm{Head}\,\alpha$ is finite, witnessed by $n:\mathbb{N}$ together with an identification $p$ of $\underline{n}$ with $\mathrm{Head}\,\alpha$ , the delayed value is the suffix of $\alpha$ after that run,

\mathrm{Tail}\,\alpha\,(n,p)\,k\;=\;\alpha\,(k{+}n{+}1).

The two together give the map

\mathrm{Cons}^{-1}\,\alpha=(\mathrm{Head}\,\alpha,\mathrm{Tail}\,\alpha)

from $\mathbf{2}^{\mathbb{N}}$ to the type of delayed binary sequences.

The composite $\mathrm{Cons}^{-1}\circ\mathrm{Cons}$ is the identity. Its first component asks for $\mathrm{Head}(\mathrm{Cons}(u,\pi))=u$ , which holds for $u=\underline{n}$ by induction on $n$ from the two clauses, and for $u=\infty$ because $\mathrm{Cons}(\infty,\pi)$ begins with $1$ and continues as $\mathrm{Cons}(\infty,\pi^{\prime})$ , so that $\mathrm{Head}(\mathrm{Cons}(\infty,\pi))$ is a fixed point of prefixing a $1$ , and $\infty$ is the unique such point. This proves the two cases $u=\underline{n}$ and $u=\infty$ . These suffice by Lemma 2.21, applied to the two functions of $u:\mathbb{N}_{\infty}$ that send $\pi$ to $\mathrm{Head}(\mathrm{Cons}(u,\pi))$ and to $u$ , because the map $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ is extremely dense (Examples 3.3(6)) and the values of the two functions at $u$ lie in a $\neg\neg$ -separated type. That type is the type of functions from finiteness of $u$ to $\mathbb{N}_{\infty}$ , which is totally separated, since $\mathbb{N}_{\infty}$ is, being a retract of $\mathbf{2}^{\mathbb{N}}$ (Example 3.1, Examples 3.13(3), Proposition 3.12(1, 4)), and totally separated types are $\neg\neg$ -separated (Lemma 3.9(2)). The second component asks that $\mathrm{Tail}(\mathrm{Cons}(u,\pi))$ , transported along the identification just established, be $\pi$ , and this follows from the two clauses by cases on the finiteness witness, the case of a positive witness using that $\mathrm{Cons}(\underline{n{+}1},\pi)$ is $\pi$ applied to the witness of finiteness of $\underline{n{+}1}$ once its first $n{+}1$ digits are removed.

The composite $\mathrm{Cons}\circ\mathrm{Cons}^{-1}$ is the identity as well. When $\alpha$ begins with $0$ , the head of $\alpha$ is $\underline{0}$ , and the first clause gives $\mathrm{Cons}(\mathrm{Cons}^{-1}\,\alpha)=\alpha$ , because the finiteness witness obtained by transporting along $\mathrm{Head}\,\alpha=\underline{0}$ has size $0$ , which makes $\mathrm{Tail}\,\alpha$ at that witness the tail of $\alpha$ . When $\alpha$ begins with $1$ , the head of $\alpha$ prefixes a $1$ to the head of the tail of $\alpha$ , and the second clause gives that $\mathrm{Cons}(\mathrm{Cons}^{-1}\,\alpha)$ begins with $1$ and continues as $\mathrm{Cons}(\mathrm{Cons}^{-1}(\text{the tail of $\alpha$}))$ , the transported witness again having the size that makes $\mathrm{Tail}\,\alpha$ agree with $\mathrm{Tail}$ of the tail of $\alpha$ . Induction on the digit index, with $\alpha$ generalized, settles all digits: the first case does so at one stroke, and the second reduces the digit of index $k{+}1$ to the digit of index $k$ of the tail. The two composites being the identity, the map $\mathrm{Cons}$ is an equivalence. ∎

Remark 4.37.

Notice that, more generally, for any type $X$ , the extended sum of the constant family at $X$ along the embedding $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ is the type $\textstyle\Sigma_{u\,:\,\mathbb{N}_{\infty}}\,\big(\text{$u$ is finite}\to X\big).$ This type satisfies the universal property of the delay monad [5], and, moreover, $\mathbf{2}^{\mathbb{N}}$ is the final coalgebra of the functor part of this monad, but we will not prove these two facts here. Hence the extended sum along $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ of an arbitrary countable family $X:\mathbb{N}\to\mathcal{U}$ generalizes the delay monad, the type $X\,n$ of the result being allowed to depend on the time $u=\underline{n}$ at which it arrives.

5. Equipping compact types with well-orders

The compact types we construct in this paper all come equipped with well-orders, in the sense of [41, Section 10.3], because the operations used to build them, discussed in the previous section, preserve well-orders.

5.1. Ordinals in type theory

Let ${\mathrel{<}}$ be a binary relation on a type $X$ . We say that an element $x:X$ is accessible whenever every $y\mathrel{<}x$ is accessible. In particular, if an element has no predecessors, then it is vacuously accessible. This is an inductive definition with a constructor of type

\textstyle\prod_{x:X}\big(\textstyle\prod_{y:X}(y\mathrel{<}x\to\text{$y$ is accessible})\big)\to\text{$x$ is accessible},

which we leave unnamed. We say that the relation ${\mathrel{<}}$ is well-founded if every element is accessible.

Lemma 5.1.

A binary relation ${\mathrel{<}}$ on a type $X$ is well-founded if and only if the principle of transfinite induction holds: for every family $P:X\to\mathcal{U}$ ,

\big(\textstyle\prod_{x:X}\big(\textstyle\prod_{y:X}y\mathrel{<}x\to P\,y\big)\to P\,x\big)\to\textstyle\prod_{x:X}P\,x.

Proof.

The accessibility elimination rule turns a step

\big(\textstyle\prod_{y:X}(y\mathrel{<}x\to P\,y)\big)\to P\,x

into a witness of $P\,x$ for every accessible $x$ , so accessibility of every element gives transfinite induction for every family $P:X\to\mathcal{U}$ . Conversely, the constructor of the accessibility predicate is a step for the family $P={}$ accessibility, so transfinite induction applied to accessibility gives accessibility of every element. ∎

We say that the relation ${\mathrel{<}}$ is extensional if any two elements with the same predecessors are equal: $\big(u\mathrel{<}x\leftrightarrow u\mathrel{<}y\text{ for all }u\big)\to x=y$ . An ordinal is a type $X$ equipped with a proposition valued binary relation ${\mathrel{<}}:X\to X\to\mathcal{U}$ which is transitive, well-founded and extensional. Such a relation is called a well-order on $X$ . We write $\mathrm{Ord}_{\mathcal{U}}$ for the type of ordinals with underlying type in $\mathcal{U}$ , where we omit the subscript when it can be inferred from the context. The HoTT Book additionally requires the type $X$ to be a set, but this is automatic:

Lemma 5.2.

Any type equipped with a proposition valued extensional relation is a set.

Proof.

Let ${\mathrel{<}}$ be a proposition valued extensional relation on a type $X$ . Consider the derived relation $x\preccurlyeq y:\equiv\prod_{z}(z\mathrel{<}x\to z\mathrel{<}y)$ , that every predecessor of $x$ is a predecessor of $y$ . It is reflexive, and it is proposition valued because $\mathrel{<}$ is. Extensionality of $\mathrel{<}$ says exactly that it is antisymmetric, since $x\preccurlyeq y$ and $y\preccurlyeq x$ together say that $x$ and $y$ have the same predecessors. Now a type carrying a reflexive, antisymmetric, proposition valued relation is a set, since the relation lets us define, from an identification $x=y$ , a weakly constant endofunction of $x=y$ : transport the reflexivity of $\preccurlyeq$ along the identification to get $x\preccurlyeq y$ and $y\preccurlyeq x$ , and apply antisymmetry, the constancy coming from $\preccurlyeq$ being proposition valued. So Hedberg’s Theorem 2.5 applies. ∎

Examples 5.3.

(1)

The type of natural numbers under its natural order is well-ordered, giving rise to an ordinal written $\omega$ .
(2)

Any proposition ordered by the relation with empty graph is an ordinal, and in particular we get ordinals $\mathbf{0}$ and $\mathbf{1}$ .
(3)

The two-element type $\mathbf{2}$ ordered by $0\mathrel{<}1$ is an ordinal.
(4)

The type $\Omega$ of propositions is an ordinal under the order $p\mathrel{<}q$ when $p=\bot$ and $q=\top$ .

Notation 5.4.

An ordinal is written with the symbol of its underlying type, so that $x:\alpha$ is a point of the underlying type of the ordinal $\alpha$ , a map $\alpha\to\beta$ is a map between the underlying types, and a notion such as compactness is a notion about the underlying type. This is the same convention by which a group is identified by its carrier. The order of an ordinal is written ${\mathrel{<}}$ , the same symbol for every ordinal, with a subscript naming the ordinal only when several orders occur together, as in the definitions of the arithmetic operations below. The subscript on $\mathrm{Ord}$ , and on the variants of it introduced later, names the universe of the underlying types, as it does on $\Omega_{\mathcal{U}}$ , and is left out where the context determines it.

By univalence, the type $\mathrm{Ord}$ is itself an ordinal in the next universe, under the relation

\alpha\mathrel{<}\beta\;:\equiv\;\Sigma_{b:\beta}\,\alpha=\beta\mathbin{\downarrow}b,

where $\beta\mathbin{\downarrow}b$ is the initial segment (lower set, or downward closure) of $\beta$ at $b$ , which is again an ordinal, with the points of $\beta$ below $b$ as its underlying type and the order inherited from $\beta$ :

\beta\mathbin{\downarrow}b\;:\equiv\;\textstyle\Sigma_{y:\beta}\,y\mathrel{<_{\beta}}b,\qquad(y,l)\mathrel{<}(z,m)\;:\equiv\;y\mathrel{<_{\beta}}z.

In particular, being well-ordered, $\mathrm{Ord}$ is a set by Lemma 5.2. Passing to initial segments preserves the order, in the sense that $y\mathrel{<_{\beta}}y^{\prime}$ implies $\beta\mathbin{\downarrow}y\mathrel{<}\beta\mathbin{\downarrow}y^{\prime}$ . We also use the initial-segment embedding order

\alpha\mathrel{\leq}\beta\;:\equiv\;\Sigma_{f:\alpha\to\beta}\,\text{$f$ is a simulation of $\alpha$ into $\beta$},

where a simulation of $\alpha$ into $\beta$ is a map $f:\alpha\to\beta$ that is order-preserving and initial-segment-preserving, the latter meaning that every point of $\beta$ below $f\,x$ is the image of a point of $\alpha$ below $x$ :

x\mathrel{<_{\alpha}}y\to f\,x\mathrel{<_{\beta}}f\,y\qquad\text{and}\qquad z\mathrel{<_{\beta}}f\,x\to\textstyle\Sigma_{x^{\prime}:\alpha}\,(x^{\prime}\mathrel{<_{\alpha}}x)\times(f\,x^{\prime}=z).

The two conditions together say that $f$ maps the initial segment of $x$ onto the initial segment of $f\,x$ , and $\alpha\mathrel{<}\beta$ implies $\alpha\mathrel{\leq}\beta$ , while $\alpha\mathrel{<}\beta\mathrel{\leq}\gamma$ implies $\alpha\mathrel{<}\gamma$ . There is at most one simulation of $\alpha$ into $\beta$ , so that $\alpha\mathrel{\leq}\beta$ is a proposition. Two ordinals $\alpha,\beta$ are order equivalent, written $\alpha\simeq_{o}\beta$ , when there is an order-preserving equivalence $\alpha\simeq\beta$ with order-preserving inverse. This relation is a proposition, as there is at most one such equivalence.

Lemma 5.5.

If $f:\alpha\to\beta$ is a surjective simulation, then $f$ is an equivalence with order-preserving inverse.

Proof.

A simulation is left cancellable, which is proved by transfinite induction on the two points (Lemma 5.1). Let $f\,x=f\,x^{\prime}$ and $u\mathrel{<}x$ . Order preservation gives $f\,u\mathrel{<}f\,x^{\prime}$ , and initial-segment preservation gives $v\mathrel{<}x^{\prime}$ with $f\,v=f\,u$ , so $u=v\mathrel{<}x^{\prime}$ by the induction hypothesis. Symmetrically, every point below $x^{\prime}$ is below $x$ , and extensionality identifies $x$ with $x^{\prime}$ . The underlying type of an ordinal is a set by Lemma 5.2, and a left-cancellable map into a set is an embedding (Definition 2.10), so the fibers of $f$ are propositions. Surjectivity makes them inhabited (Definition 2.9), and an inhabited proposition is a singleton, so $f$ is an equivalence (Definition 2.8).

The map $f$ is also order-reflecting. If $f\,x\mathrel{<}f\,y$ , then $f\,x$ lies in the initial segment of $f\,y$ , which initial-segment preservation identifies with the image of the initial segment of $y$ , so $f\,x=f\,x^{\prime}$ for some $x^{\prime}\mathrel{<}y$ , and left cancellability gives $x=x^{\prime}\mathrel{<}y$ . The inverse of an order-preserving order-reflecting equivalence is order-preserving. ∎

5.2. Trichotomy

Definition 5.6 (Trichotomy).

An ordinal $\alpha$ is trichotomous if for all $x,y:\alpha$ we have $x\mathrel{<}y$ or $x=y$ or $x\mathrel{>}y$ . We write $\mathrm{Ord}_{3}$ for the type of trichotomous ordinals in a universe left implicit.

Remark 5.7.

Asking that every discrete ordinal be trichotomous is equivalent to excluded middle.

Proof.

Excluded middle decides $x\mathrel{<}y$ for all $x,y:\alpha$ , and a well-order whose order is decidable is trichotomous.

Conversely, let $P$ be a proposition with $\neg\neg P$ , and order the two-element type by

0\mathrel{<}1\;:\equiv\;P,\qquad 0\mathrel{<}0\;:\equiv\;1\mathrel{<}0\;:\equiv\;1\mathrel{<}1\;:\equiv\;\mathbf{0}.

This order is proposition valued, transitive and well-founded with no assumption on $P$ , and $\neg\neg P$ makes it extensional, so it is an ordinal, whose underlying type $\mathbf{2}$ is discrete. Trichotomy at $0$ and $1$ then gives $P$ , since $0=1$ is false and $1\mathrel{<}0$ is empty. This is double negation elimination, and hence excluded middle. ∎

Trichotomous ordinals are nevertheless abundant without excluded middle, and Section 6.2 interprets every Brouwer code as a trichotomous ordinal under an interpretation that dominates the standard one.

Lemma 5.8.

Trichotomy implies discreteness.

Proof.

Given $x$ and $y$ , the two order cases of trichotomy decide $x\neq y$ , because a well-founded relation is irreflexive, and the middle case decides $x=y$ . ∎

5.3. Ordinal arithmetic

Definition 5.9 (Ordinal addition).

The sum $\alpha\mathbin{+}\beta$ has as underlying type the binary sum of those of $\alpha$ and $\beta$ , ordered so that every element of $\alpha$ precedes every element of $\beta$ :

	$\displaystyle\mathrm{inl}\,x\mathrel{<}\mathrm{inl}\,x^{\prime}$	$\displaystyle:\equiv x\mathrel{<_{\alpha}}x^{\prime},$	$\displaystyle\mathrm{inl}\,x\mathrel{<}\mathrm{inr}\,y^{\prime}$	$\displaystyle:\equiv\mathbf{1},$
	$\displaystyle\mathrm{inr}\,y\mathrel{<}\mathrm{inr}\,y^{\prime}$	$\displaystyle:\equiv y\mathrel{<_{\beta}}y^{\prime},$	$\displaystyle\mathrm{inr}\,y\mathrel{<}\mathrm{inl}\,x^{\prime}$	$\displaystyle:\equiv\mathbf{0}.$

Lemma 5.10.

The order of Definition 5.9 is a well-order, so that $\alpha\mathbin{+}\beta$ is an ordinal.

Proof.

The order is proposition valued because each of its two cases is and the two exclude each other. The first case is the order of $\tau$ . The second is a sum whose index type $x=x^{\prime}$ is a proposition, the underlying type of an ordinal being a set (Lemma 5.2), and whose fibers are given by the order of $\upsilon\,x^{\prime}$ . The two cases exclude each other, because $x\mathrel{<}x^{\prime}$ together with $x=x^{\prime}$ would make $x$ precede itself, which well-foundedness forbids. A binary sum of two propositions that exclude each other is a proposition.

For transitivity, consider two consecutive steps. If both move the index, then so does their composite, by the transitivity of the order of $\tau$ . If exactly one of them moves the index, then so does the composite, by transporting its index comparison along the identification supplied by the other. If neither does, the three indices agree and the fiber order is transitive.

For well-foundedness, we show that $(x,a)$ is accessible by induction on the accessibility of $x$ and then on that of $a$ . Its predecessors are the $(x^{\prime},a^{\prime})$ with $x^{\prime}\mathrel{<}x$ , accessible by the induction hypothesis on $x$ , and the $(x,a^{\prime})$ with $a^{\prime}\mathrel{<}a$ , accessible by the induction hypothesis on $a$ .

Now let the family be constant, say $\upsilon\,x=\alpha$ for every $x$ , and let $(x,a)$ and $(x^{\prime},a^{\prime})$ have the same predecessors. Given $u\mathrel{<}x$ , we have $(u,a)\mathrel{<}(x,a)$ and hence $(u,a)\mathrel{<}(x^{\prime},a^{\prime})$ , which gives either $u\mathrel{<}x^{\prime}$ or $u=x^{\prime}$ together with $a\mathrel{<}a^{\prime}$ . The second case is impossible, because it makes $x^{\prime}\mathrel{<}x$ , so that $(x^{\prime},a^{\prime})\mathrel{<}(x,a)$ and hence $(x^{\prime},a^{\prime})\mathrel{<}(x^{\prime},a^{\prime})$ , which well-foundedness forbids. So every predecessor of $x$ is one of $x^{\prime}$ , and by symmetry the two points have the same predecessors, which gives $x=x^{\prime}$ by the extensionality of $\tau$ .

So we may take $x^{\prime}$ to be $x$ . For $b\mathrel{<}a$ we have $(x,b)\mathrel{<}(x,a)$ and hence $(x,b)\mathrel{<}(x,a^{\prime})$ , which gives $b\mathrel{<}a^{\prime}$ , the alternative $x\mathrel{<}x$ being impossible. By symmetry and the extensionality of $\alpha$ , we get $a=a^{\prime}$ . ∎

Definition 5.11 (Lexicographic order on arbitrary sums).

For $\tau:\mathrm{Ord}$ and a family $\upsilon:\tau\to\mathrm{Ord}$ , the lexicographic order on $\Sigma_{x:\tau}\,\upsilon\,x$ has the index as the more significant coordinate:

(x,a)\mathrel{<}(x^{\prime},a^{\prime})\;:\equiv\;(x\mathrel{<_{\tau}}x^{\prime})\;+\;\textstyle\Sigma_{r\,:\,x=x^{\prime}}\,\big(\mathrm{transport}^{\upsilon}\,r\,a\mathrel{<_{\upsilon\,x^{\prime}}}a^{\prime}\big).

We write $\Sigma_{\tau}\upsilon$ for the type $\Sigma_{x:\tau}\,\upsilon\,x$ equipped with this order.

Lemma 5.12.

The lexicographic order is proposition valued, transitive and well-founded. It is moreover extensional when the family is constant.

Proof.

It is proposition valued because each of its two cases is, the second because $\tau$ is a set, so that $r$ is unique, and the fiber orders are proposition valued. The two cases exclude each other, because $x\mathrel{<}x^{\prime}$ together with $x=x^{\prime}$ would make $x$ precede itself. A binary sum of two propositions that exclude each other is a proposition.

For transitivity, if either of two consecutive steps moves the index then so does their composite, by the transitivity of $\mathrel{<}$ after transporting, and if neither does, the three indices agree and the fiber order is transitive.

Now let the family be constant, say $\upsilon\,x=\alpha$ for every $x$ , and let $(x,a)$ and $(x^{\prime},a^{\prime})$ have the same predecessors. Given $u\mathrel{<}x$ we have $(u,a)\mathrel{<}(x,a)$ , so $(u,a)\mathrel{<}(x^{\prime},a^{\prime})$ , which gives either $u\mathrel{<}x^{\prime}$ , as wanted, or $u=x^{\prime}$ together with $a\mathrel{<}a^{\prime}$ . In the second case $x^{\prime}\mathrel{<}x$ , so $(x^{\prime},a^{\prime})\mathrel{<}(x,a)$ and hence $(x^{\prime},a^{\prime})\mathrel{<}(x^{\prime},a^{\prime})$ , which well-foundedness forbids. By symmetry $x$ and $x^{\prime}$ have the same predecessors, so $x=x^{\prime}$ by the extensionality of $\tau$ , and we may assume $x=x^{\prime}$ . Then for $b\mathrel{<}a$ we have $(x,b)\mathrel{<}(x,a)$ , hence $(x,b)\mathrel{<}(x,a^{\prime})$ , which gives $b\mathrel{<}a^{\prime}$ , since $x\mathrel{<}x$ is impossible, and by symmetry and the extensionality of the fiber, we get $a=a^{\prime}$ . ∎

Definition 5.13 (Ordinal multiplication).

Ordinal multiplication $\alpha\mathbin{\times}\beta$ is the lexicographic order of Definition 5.11 in the case of a constant family: the sum over $\beta$ of the family constantly $\alpha$ , so that $\beta$ is the more significant coordinate. The operands are thus written in the opposite order from their sum, $\alpha$ before $\beta$ , as in the classical definition. It is an ordinal by Lemma 5.12.

Lemma 5.14 (Maps of lexicographic sums).

For $\tau,\tau^{\prime}:\mathrm{Ord}$ with families $\upsilon:\tau\to\mathrm{Ord}$ and $\upsilon^{\prime}:\tau^{\prime}\to\mathrm{Ord}$ , a map $f:\tau\to\tau^{\prime}$ and maps $g\,x:\upsilon\,x\to\upsilon^{\prime}\,(f\,x)$ , the map $\Sigma(f,g):\Sigma_{\tau}\upsilon\to\Sigma_{\tau^{\prime}}\upsilon^{\prime}$ of Definition 2.28 is

(1)

order-preserving if $f$ is and every $g\,x$ is,
(2)

order-reflecting if $f$ is and every $g\,x$ is and $f$ is in addition an embedding.

Proof.

A comparison in the lexicographic order of Definition 5.11 is of one of two kinds, a comparison of the indices, or an identification of the indices together with a comparison in the fiber.

(1) A comparison of the first kind is preserved by $f$ . One of the second kind is preserved by $g\,x$ , after transporting the fiber component along the image under $f$ of the identification of the indices.

(2) A comparison of the images of the first kind is reflected by $f$ . One of the second kind comes with an identification $f\,x=f\,y$ of the images of the indices, and $f$ , being an embedding, is left cancellable, which identifies $x$ with $y$ . The underlying type of an ordinal is a set (Lemma 5.2), so the given identification is the image of that one, and the two transports agree. The comparison in the fiber is then reflected by $g\,x$ . ∎

Remark 5.15.

For arbitrary $\tau:\mathrm{Ord}$ and $\upsilon:\tau\to\mathrm{Ord}$ , the lexicographic order on $\Sigma_{x:\tau}\,\upsilon\,x$ fails constructively to be extensional, in that excluded middle follows if all such orders are extensional.

Proof.

Take $\tau$ to be the ordinal $\Omega$ and $\upsilon$ to be the family that sends a truth value $p$ to the proposition $p\neq\bot$ . Every proposition is an ordinal in exactly one way, under the empty order, so this is a family of ordinals. No comparison in a fiber is possible, the fibers carrying the empty order, so the lexicographic sum is the subtype

X\;:\equiv\;\textstyle\Sigma_{p:\Omega}\,p\neq\bot

of $\Omega$ with the restricted order. No element of $X$ has a predecessor in $X$ , since a predecessor would have to be $\bot$ , which $X$ excludes. So the hypothesis of extensionality is vacuous, and extensionality of $X$ says that $X$ is a proposition. Let $P$ be a proposition with $\neg\neg P$ . Both $P$ and $\neg\neg P$ are elements of $X$ , so they are equal, and $P$ follows. This is double negation elimination, and hence excluded middle. This counterexample is due to Mike Shulman (personal communication). ∎

One sufficient condition for the lexicographic order to be extensional is that the family be constant, as we have seen above. Two further sufficient conditions are that the index ordinal be trichotomous, and that the summands have top elements.

Lemma 5.16.

If $\tau$ is trichotomous and $\upsilon$ is a $\tau$ -indexed family of ordinals, then the lexicographic order is extensional, so that $\Sigma_{\tau}\upsilon$ is an ordinal.

Proof.

By Lemma 5.12, only extensionality is left to prove. Trichotomy makes the order of $\tau$ cotransitive, in the sense that $x\mathrel{<}y$ implies, for any $z$ , that $x\mathrel{<}z$ or $z\mathrel{<}y$ . Indeed, compare $z$ with $y$ . In the case $z\mathrel{<}y$ there is nothing to do, in the case $z=y$ we have $x\mathrel{<}z$ , and in the case $y\mathrel{<}z$ transitivity gives $x\mathrel{<}z$ .

Now let $(a,b)$ and $(x,y)$ have the same predecessors. Given $u\mathrel{<}a$ , cotransitivity applied to the point $x$ gives $u\mathrel{<}x$ or $x\mathrel{<}a$ . In the second case $(x,y)\mathrel{<}(a,b)$ , so that $(x,y)\mathrel{<}(x,y)$ , which the well-foundedness of the lexicographic order forbids. So every predecessor of $a$ is one of $x$ , and by symmetry the two have the same predecessors, which gives $a=x$ by the extensionality of $\tau$ .

So we may take $a$ to be $x$ . For $v\mathrel{<}b$ we have $(x,v)\mathrel{<}(x,b)$ and hence $(x,v)\mathrel{<}(x,y)$ , which gives $v\mathrel{<}y$ , the alternative $x\mathrel{<}x$ being impossible. By symmetry and the extensionality of $\upsilon\,x$ , we get $b=y$ . ∎

Definition 5.17 (Topped ordinals).

A top of an ordinal $\alpha$ is a point that no element exceeds, and $\mathrm{Ord}^{\top}$ is the type of ordinals equipped with a top:

\mathrm{Ord}^{\top}:\equiv\textstyle\Sigma_{\alpha:\mathrm{Ord}}\,\Sigma_{t:\alpha}\,\prod_{y:\alpha}\,\neg\,(t\mathrel{<}y).

A largest element is a top, because the order is well-founded and hence irreflexive, but not conversely: in the ordinal $\Omega$ no element exceeds a truth value $P$ with $\neg\neg P$ , since such a $P$ differs from $\bot$ , whereas $\top$ is the largest element. This shows that having a top element is in general data rather than property. Classically, the topped ordinals are precisely the successor ordinals (ordinals of the form $\alpha\mathbin{+}\mathbf{1}$ ).

Example 5.18.

The type $\mathbb{N}_{\infty}$ of Example 3.1 is an ordinal under its natural order, in which $u$ precedes $v$ when $u$ is a finite point $\underline{n}$ whose index is below $v$ in the sense of Example 3.1:

u\mathrel{<}v\;:\equiv\;\textstyle\Sigma_{n:\mathbb{N}}\,\big((u=\underline{n})\times(n\mathrel{\sqsubset}v)\big).

It is topped by its largest element $\infty$ , and we write $\mathbb{N}_{\infty}$ for it, as an ordinal or as a topped one according to the context.

Proof.

The predecessors of a point $v$ are exactly the finite points $\underline{n}$ with $n\mathrel{\sqsubset}v$ . One direction is the definition, which asks a predecessor to be finite, and for the other, the comparison $\underline{n}\mathrel{<}v$ holds whenever $n\mathrel{\sqsubset}v$ . Moreover, the index $n$ in the definition is determined by $u$ , because $\underline{(-)}$ is left cancellable.

The order is proposition valued, being a sum over $n$ of a product of two equations in the sets $\mathbb{N}_{\infty}$ and $\mathbf{2}$ , with the index $n$ determined as observed above.

For transitivity, let $u\mathrel{<}v$ and $v\mathrel{<}w$ , say $u=\underline{m}$ with $m\mathrel{\sqsubset}v$ and $v=\underline{n}$ with $n\mathrel{\sqsubset}w$ . From $m\mathrel{\sqsubset}\underline{n}$ we get $m<n$ , and $w$ is decreasing, so that $n\mathrel{\sqsubset}w$ gives $m\mathrel{\sqsubset}w$ . This says that $u\mathrel{<}w$ .

For well-foundedness, each finite point $\underline{n}$ is accessible by course-of-values induction on $n$ . Its predecessors are the $\underline{m}$ with $m\mathrel{\sqsubset}\underline{n}$ , that is, with $m<n$ , and these are accessible by the induction hypothesis. Any point $v$ is then accessible, its predecessors being finite points.

For extensionality, let $u$ and $v$ have the same predecessors. By the first paragraph this says that $n\mathrel{\sqsubset}u$ if and only if $n\mathrel{\sqsubset}v$ for every $n$ , and two binary digits that are $1$ in the same cases are equal, so $u$ and $v$ have the same digits. Being decreasing is a proposition, so a point of $\mathbb{N}_{\infty}$ is determined by its digits, and $u=v$ .

Finally, the point $\infty$ is a top, because $\infty\mathrel{<}v$ would make $\infty$ a finite point $\underline{n}$ , and $\infty$ is not finite, having $n\mathrel{\sqsubset}\infty$ for every $n$ whereas $\underline{n}\mathrel{\sqsubseteq}n$ . ∎

Constructively, $\mathbb{N}_{\infty}$ is topped by $\infty$ without being a successor ordinal, since $\infty$ fails to be isolated constructively (Examples 3.3(5)).

The operations on topped ordinals and on trichotomous ordinals (Definition 5.6) are written like those on plain ordinals. Addition and multiplication of ordinals restrict to topped ordinals, and the ordinal-indexed sum $\Sigma_{\tau}\upsilon$ of a topped-ordinal-indexed family of topped ordinals is again topped. They restrict to trichotomous ordinals as well, where the sum of a trichotomous-ordinal-indexed family of trichotomous ordinals is an ordinal by Lemma 5.16 and is again trichotomous.

Lemma 5.19.

If $\upsilon$ is a $\tau$ -indexed family of topped ordinals, then the lexicographi order is extensional, so that $\Sigma_{\tau}\upsilon$ is an ordinal. If moreover $\tau$ is topped, then so is $\Sigma_{\tau}\upsilon$ .

Proof.

By Lemma 5.12, only extensionality is left to prove. Write $t_{u}$ for the top of $\upsilon\,u$ , and let $(a,b)$ and $(x,y)$ have the same predecessors. Given $u\mathrel{<}a$ , we have $(u,t_{u})\mathrel{<}(a,b)$ and hence $(u,t_{u})\mathrel{<}(x,y)$ , which gives $u\mathrel{<}x$ or $u=x$ together with a comparison exceeding $t_{u}$ in the fiber, and the latter is impossible. So every predecessor of $a$ is one of $x$ , and by symmetry the two have the same predecessors, which gives $a=x$ by the extensionality of $\tau$ . The fiber components are then identified as in the proof of Lemma 5.16, which for that step uses only the irreflexivity of the two orders.

We take the top of the sum to be the pair of the top $t$ of $\tau$ with the top of $\upsilon\,t$ . A point exceeding it would either exceed $t$ in $\tau$ or exceed the top of $\upsilon\,t$ in that fiber, and neither is possible. ∎

Lemma 5.20.

If $\tau:\mathrm{Ord}^{\top}$ and $\upsilon:\tau\to\mathrm{Ord}^{\top}$ , where $\tau$ is compact pointed and $\upsilon\,x$ is compact pointed for every $x$ , then $\Sigma_{\tau}\upsilon$ is compact pointed.

Proof.

The underlying type of $\Sigma_{\tau}\upsilon$ is by definition $\Sigma_{x:\tau}\,\upsilon\,x$ , in which the order plays no part, so the claim is an instance of Corollary 4.10(2). For the underlying type of a topped ordinal, pointed compactness and compactness agree by Lemma 4.6, the designated top supplying the point. ∎

5.4. Extended sums

The extended sum of Section 4.7 becomes a construction on ordinals once the extension of a family carries an order, which we use to interpret the ordinal notations of Sections 6 and 7. For the following, recall the $\Pi$ -extension operation on families given in Definition 4.30.

Lemma 5.21.

Let $j:X\hookrightarrow K$ be an embedding and $\alpha:X\to\mathrm{Ord}$ a family of ordinals. For any $k:K$ , give the type $(\alpha\mathbin{/}j)\,k$ the relation

u\mathrel{<}v\;:\equiv\;\Sigma_{p\,:\,j^{-1}(k)}u\,p\mathrel{<_{\alpha\,(\mathrm{pr}_{1}p)}}v\,p.

This is a well-order, so we obtain the extension $\alpha\mathbin{/}j:K\to\mathrm{Ord}$ .

Proof.

Since $j$ is an embedding, the fiber $j^{-1}(k)$ is a proposition, so $(\alpha\mathbin{/}j)\,k$ is a product indexed by a proposition, and $\mathrel{<}$ is the order that such a product carries, asking the component order to hold at some point of the fiber. For each $p:j^{-1}(k)$ , evaluation at $p$ is an equivalence from the product to the component $\alpha\,(\mathrm{pr}_{1}p)$ , whose inverse sends a point of the component to the section transporting it along the identifications of the fiber.

The order is proposition valued, being a sum over a proposition of proposition valued components.

For extensionality, suppose that $u$ and $v$ have the same predecessors, and let $p:j^{-1}(k)$ . A predecessor $x$ of $u\,p$ determines a section, which is a predecessor of $u$ in the product, witnessed at $p$ . By the hypothesis it is a predecessor of $v$ , witnessed at some point of the fiber, which is $p$ because the fiber is a proposition, so $x$ is a predecessor of $v\,p$ . Symmetrically, $u\,p$ and $v\,p$ have the same predecessors, and the extensionality of $\alpha\,(\mathrm{pr}_{1}p)$ gives $u\,p=v\,p$ . Since $p$ was arbitrary, $u=v$ .

For transitivity, two consecutive comparisons come with points of the fiber, which are equal because the fiber is a proposition, so that the transitivity of the component order at that point applies.

For well-foundedness, a point $u$ of the product is accessible as soon as every $v\mathrel{<}u$ is. A witness of $v\mathrel{<}u$ supplies a point $p$ of $j^{-1}(k)$ together with $v\,p\mathrel{<}u\,p$ , and $u\,p$ is accessible because the order of $\alpha\,(\mathrm{pr}_{1}p)$ is well-founded, so that $v\,p$ is accessible as one of its predecessors. Accessibility transfers from the component back to the product along evaluation at $p$ , because a predecessor in the product of the section determined by a point $x$ of the component has its value at $p$ below $x$ . ∎

Lemma 5.22.

If every $\alpha\,x$ is topped, then so is every $(\alpha\mathbin{/}j)\,k$ , so the construction extends families of topped ordinals.

Proof.

Suppose each $\alpha\,x$ has a top element $t_{x}$ . Then $p\mapsto t_{\mathrm{pr}_{1}p}$ is a top element of $\mathrel{<}$ , since, if it were below some $\psi$ , we would have a fiber $p:j^{-1}(k)$ with $t_{\mathrm{pr}_{1}p}\mathrel{<}\psi\,p$ , contradicting the topness of $t_{\mathrm{pr}_{1}p}$ . ∎

Lemma 5.23.

The construction restricts back to $\alpha$ along $j$ , giving

(\alpha\mathbin{/}j)(j\,x)\simeq_{o}\alpha\,x

for every $x:X$ , as illustrated in the diagram below.

Proof.

For $k=j\,x$ the fiber $j^{-1}(j\,x)$ is a singleton, being an inhabited proposition, so evaluation at its center $(x,\mathrm{refl})$ is an equivalence $(\alpha\mathbin{/}j)(j\,x)\to\alpha\,x$ by Lemma 4.31(1). It is order-preserving, because a comparison $u\mathrel{<}v$ is witnessed at some point of the fiber, and that point is the center, the fiber being a proposition, so that the comparison holds at the center. It is order-reflecting, because a comparison at the center is by definition a witness of $u\mathrel{<}v$ . The inverse of an order-preserving order-reflecting equivalence is order-preserving, so this is an order equivalence. ∎

Lemma 5.24.

If every $\alpha\,x$ is totally separated, then so is every $(\alpha\mathbin{/}j)\,k$ .

Proof.

By Lemma 4.34. ∎

Under univalence, the above two lemmas show that the type of ordinals and the type of totally separated ordinals are both algebraically injective in the sense of [18], as univalence turns order equivalences into identifications.

Definition 5.25 (Countable extended sum and successor sum).

Let $\upsilon:\mathbb{N}\to\mathrm{Ord}^{\top}$ be a family of topped ordinals.

(1)

The extended sum of $\upsilon$ is the extension of $\upsilon$ along the embedding $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ , summed over the ordinal $\mathbb{N}_{\infty}$ :

$\Sigma^{1}\upsilon\;:\equiv\;\Sigma_{\mathbb{N}_{\infty}}\,\big(\upsilon\mathbin{/}\iota\big).$
(2)

The successor sum of $\upsilon$ is the extension of $\upsilon$ along the left inclusion $\mathrm{inl}:\mathbb{N}\hookrightarrow\mathbb{N}+\mathbf{1}$ , summed over the successor $\omega\mathbin{+}\mathbf{1}$ , taken as a topped ordinal with the added point as top:

$\Sigma_{1}\upsilon\;:\equiv\;\Sigma_{\omega\mathbin{+}\mathbf{1}}\,\big(\upsilon\mathbin{/}\mathrm{inl}\big).$

Lemma 5.26.

Let $\upsilon:\mathbb{N}\to\mathrm{Ord}^{\top}$ .

(1)

The successor sum is order equivalent to the successor of the countable sum:

$\Sigma_{1}\upsilon\;\simeq_{o}\;\Big(\Sigma_{\omega}\,\upsilon\Big)\mathbin{+}\mathbf{1}.$
(2)

If $\upsilon\,n$ is a retract of $\mathbb{N}$ for every $n$ , then so is $\Sigma_{1}\upsilon$ , and if $\upsilon\,n$ is discrete for every $n$ , then so is $\Sigma_{1}\upsilon$ .

Proof.

The sum is taken over $\mathbb{N}+\mathbf{1}$ , so its fibers are the extension of $\upsilon$ along $\mathrm{inl}$ . Since $\mathrm{inl}$ is an embedding, that extension gives $\upsilon\,n$ back at $\mathrm{inl}\,n$ , up to order equivalence (Lemma 5.23). At $\mathrm{inr}\,\star$ the fiber of $\mathrm{inl}$ is empty, no natural number having $\mathrm{inl}\,n=\mathrm{inr}\,\star$ , so the extension is the one-point ordinal there (Lemma 4.31(2)). Write $\upsilon^{\prime}$ for the family on $\mathbb{N}+\mathbf{1}$ so described. Taking underlying types, that of $\Sigma_{1}\upsilon$ is the binary sum $\big(\Sigma_{n:\mathbb{N}}\,\upsilon\,n\big)+\mathbf{1}$ , whose top is the one supplied by Lemma 5.19, namely the pair of the top $\mathrm{inr}\,\star$ of $\omega\mathbin{+}\mathbf{1}$ with the point of its fiber.

(1) Order equivalent families have order equivalent sums, by Lemma 2.29(1) and Lemma 5.14 with the identity on the index, so $\Sigma_{1}\upsilon$ is order equivalent to $\Sigma_{\omega\mathbin{+}\mathbf{1}}\,\upsilon^{\prime}$ . The map sending $(\mathrm{inl}\,n,x)$ to $\mathrm{inl}\,(n,x)$ and $(\mathrm{inr}\,\star,\star)$ to $\mathrm{inr}\,\star$ is an equivalence from the underlying type of that sum to that of $\big(\Sigma_{\omega}\,\upsilon\big)\mathbin{+}\mathbf{1}$ , with the evident inverse. The map and its inverse are order-preserving, as one sees by comparing the lexicographic order of the sum with the order of the addition on each of the two summands. Composing the two order equivalences gives the desired equivalence.

(2) By the description of the underlying type above, it is enough to treat $\big(\Sigma_{n:\mathbb{N}}\,\upsilon\,n\big)+\mathbf{1}$ . If each $\upsilon\,n$ is a retract of $\mathbb{N}$ , then $\Sigma_{n:\mathbb{N}}\,\upsilon\,n$ is a retract of $\mathbb{N}\times\mathbb{N}$ and hence of $\mathbb{N}$ , by a pairing function, so that its binary sum with $\mathbf{1}$ is a retract of $\mathbb{N}+\mathbf{1}$ , which is again a retract of $\mathbb{N}$ . If each $\upsilon\,n$ is discrete, then so is $\Sigma_{n:\mathbb{N}}\,\upsilon\,n$ , discreteness being closed under $\Sigma$ over the discrete index $\mathbb{N}$ , and so is its binary sum with $\mathbf{1}$ , discreteness being closed under $+$ (Proposition 3.6). ∎

Definition 5.27 (Comparison map).

We now define a comparison map

\mathfrak{c}_{\upsilon}:\Sigma_{1}\upsilon\to\Sigma^{1}\upsilon.

First we need some preparation. Let $\upsilon:\mathbb{N}\to\mathrm{Ord}^{\top}$ . The underlying type of $\Sigma_{1}\upsilon$ is $\Sigma_{z\,:\,\mathbb{N}+\mathbf{1}}\,(\upsilon\mathbin{/}\mathrm{inl})\,z$ and that of $\Sigma^{1}\upsilon$ is $\Sigma_{u\,:\,\mathbb{N}_{\infty}}\,(\upsilon\mathbin{/}\iota)\,u$ . By Lemma 5.21 the two fibers are the products

(\upsilon\mathbin{/}\mathrm{inl})\,z=\textstyle\prod_{(n,r)\,:\,\mathrm{inl}^{-1}(z)}\upsilon\,n,\qquad(\upsilon\mathbin{/}\iota)\,u=\textstyle\prod_{(n,q)\,:\,\iota^{-1}(u)}\upsilon\,n.

Write $\iota_{1}:\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ for the map that sends $\mathrm{inl}\,n$ to $\underline{n}$ and the added point to $\infty$ , so that $\iota_{1}\circ\mathrm{inl}=\iota$ . The map $\iota_{1}$ is left cancellable: if $\iota_{1}\,(\mathrm{inl}\,m)=\iota_{1}\,(\mathrm{inl}\,n)$ then $\underline{m}=\underline{n}$ and so $m=n$ . If $\iota_{1}$ takes the same value at a finite point and at the added point, in either order, then $\underline{n}=\infty$ , which is impossible. And if both are the added point, they are already equal, $\mathbf{1}$ having a single point. Hence each $z:\mathbb{N}+\mathbf{1}$ gives the map $\varphi_{z}:\iota^{-1}(\iota_{1}\,z)\to\mathrm{inl}^{-1}(z)$ defined by

\varphi_{z}\,(n,q)=(n,r_{q}),

where $r_{q}:\mathrm{inl}\,n=z$ is obtained by cancelling $\iota_{1}$ in $q$ , which has type $\iota_{1}\,(\mathrm{inl}\,n)=\iota_{1}\,z$ because $\iota_{1}\circ\mathrm{inl}=\iota$ . Since $\varphi_{z}$ keeps the first component, precomposition with it gives the map $e_{z}:(\upsilon\mathbin{/}\mathrm{inl})\,z\to(\upsilon\mathbin{/}\iota)\,(\iota_{1}\,z)$ defined by

e_{z}\,\psi\,(n,q)=\psi\,(\varphi_{z}\,(n,q)).

With this notation, we define the comparison map $\mathfrak{c}_{\upsilon}:\Sigma_{1}\upsilon\to\Sigma^{1}\upsilon$ to be the map of sums of Definition 2.28 induced by $\iota_{1}$ and the family $e$ ,

\mathfrak{c}_{\upsilon}\;=\;\Sigma(\iota_{1},e),

which amounts to $\mathfrak{c}_{\upsilon}\,(z,\psi)=(\iota_{1}\,z,\,e_{z}\,\psi)$ .

This comparison map is the countable-sum case of the comparison between the discrete and the compact interpretation of Brouwer ordinal codes, which is the subject of Section 6.4. Recall from Definition 2.20 that a map is called extremely dense when the complement of the image is empty.

Lemma 5.28.

The comparison map $\mathfrak{c}_{\upsilon}$ is an extremely dense embedding and both order-preserving and order-reflecting.

Proof.

The map $\iota_{1}$ is an embedding and is extremely dense (Examples 3.3(6)). Each $e_{z}$ is an equivalence, being precomposition with the equivalence $\varphi_{z}$ . That $\varphi_{z}$ is an equivalence holds because the two fibers are propositions, $\mathrm{inl}$ and $\iota$ being embeddings, and because $\varphi_{z}$ has a converse, sending $(n,r)$ to $(n,q)$ with $q$ obtained by applying $\iota_{1}$ to $r$ . An equivalence is in particular an embedding and extremely dense, so that Lemma 2.29(2,3), applied to $\iota_{1}$ on the indices and to the maps $e_{z}$ on the fibers, makes $\mathfrak{c}_{\upsilon}$ an extremely dense embedding.

Each $e_{z}$ is moreover order-preserving and order-reflecting. A comparison in either of the two products is a point of the fiber indexing it together with a comparison of the values there, and $\varphi_{z}$ and its converse carry such data back and forth. The map $\iota_{1}$ is order-preserving and order-reflecting from $\omega\mathbin{+}\mathbf{1}$ to $\mathbb{N}_{\infty}$ . Among the finite points, $\underline{m}\mathrel{<}\underline{n}$ says that $m\mathrel{\sqsubset}\underline{n}$ , which holds exactly when $m<n$ . A finite point precedes the added point of $\omega\mathbin{+}\mathbf{1}$ , and $\underline{n}\mathrel{<}\infty$ because $n\mathrel{\sqsubset}\infty$ . And $\infty$ precedes nothing, since $\infty\mathrel{<}v$ would make $\infty$ finite. So Lemma 5.14 applies, its embedding hypothesis for (2) being again that $\iota_{1}$ is en embedding. ∎

5.5. Extended suprema

Every family of ordinals indexed by a small type has a least upper bound, assuming set quotients, or, equivalently, set replacement (Definition 2.15).

Theorem 5.29.

Let $I:\mathcal{U}$ and $\alpha:I\to\mathrm{Ord}$ , and consider the map

\sigma:\textstyle\Sigma_{i:I}\,\alpha\,i\to\mathrm{Ord},\qquad\sigma\,(i,x)=\alpha\,i\mathbin{\downarrow}x,

which sends a point of a member of the family to its initial segment in $\mathrm{Ord}$ .

(1)

The image of the map $\sigma$ is an ordinal, written $\sup\alpha$ , under the inherited order

$(\beta,w)\mathrel{<}(\beta^{\prime},w^{\prime})\;:\equiv\;\beta\mathrel{<}\beta^{\prime}.$
(2)

The map $\Sigma_{i:I}\,\alpha\,i\to\sup\alpha$ sending $(i,x)$ to the image of $x$ is a surjection.
(3)

$\sup\alpha$ is the least upper bound of the family $\alpha$ .

The proofs of these clauses are in [7]. Set replacement makes the image of the map $\sigma$ equivalent to a type in our base universe, although $\mathrm{Ord}$ is a type in the next universe. Whether suprema of families of ordinals exist constructively was left open by Kraus, Nordvall Forsberg and Xu [33], who established the least upper bound property for weakly increasing families indexed by $\mathbb{N}$ . Tom de Jong answered it with a construction by set quotients, extending and formalizing the one of [41, Lemma 10.3.22], which is claimed there only to be an upper bound, and the author of this paper simultaneously answered it with the above construction. Both are formalized by de Jong and are presented in his thesis [7].

Corollary 5.30.

If $I$ is compact pointed and $\alpha\,i$ is compact pointed for every $i:I$ , then $\sup\alpha$ is compact pointed.

Proof.

The type $\Sigma_{i:I}\,\alpha\,i$ is compact pointed by Corollary 4.10(2), and $\sup\alpha$ is a surjective image of it by Theorem 5.29(2), so Corollary 4.10(3) applies. ∎

Theorem 5.31 (Compactness of extended suprema).

For any embedding $j:X\hookrightarrow K$ into a compact pointed type and any family $\alpha:X\to\mathrm{Ord}$ of compact pointed ordinals, the supremum of the extended family $\alpha\mathbin{/}j$ is itself compact pointed.

Proof.

By Corollary 5.30 applied to the family $\alpha\mathbin{/}j$ over the compact pointed index $K$ , it suffices to show that $(\alpha\mathbin{/}j)\,k$ is compact pointed for every $k:K$ . By Lemma 5.21 this is the product of the types $\alpha\,x$ over the index type $j^{-1}(k)$ , all of which are compact pointed by hypothesis, and $j^{-1}(k)$ is a proposition precisely because $j$ is an embedding. So the micro-Tychonoff Theorem 4.26 applies. ∎

For use in Section 6, we introduce notation for the special case of the embedding $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ .

Definition 5.32 (Countable extended supremum).

For a family $\alpha:\mathbb{N}\to\mathrm{Ord}$ of ordinals, the extended supremum is

\sup\nolimits^{1}\alpha\;:\equiv\;\sup\big(\alpha\mathbin{/}\iota\big),

the supremum of the extension of $\alpha$ along the embedding $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ . The superscript has the same meaning as in the extended sum, that the index type is $\mathbb{N}_{\infty}$ rather than $\mathbb{N}+\mathbf{1}$ .

6. Compact totally separated ordinals from Brouwer codes

In the remainder of this paper we give two notation systems, each with several interpretations of the notations as ordinals. The first occupies this section and takes a traditional system, the Brouwer ordinal codes, whose interpretation $\llbracket-\rrbracket_{\Sigma^{1}}$ is compact and totally separated and dominates the standard interpretation $\llbracket-\rrbracket_{\mathrm{sup}}$ , which is neither. The subscript on an interpretation names the operation the limit constructor is read as, a sum or a supremum, and a superscript $1$ records that the family is first extended along the embedding $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ , as in the extended sum of Definition 5.25 and the extended supremum of Definition 5.32.

We give five interpretations to Brouwer codes, obtaining different combinations of compactness, total separatedness, trichotomy and discreteness. The last of the five is the discrete interpretation of Section 6.4. It assigns to each code $b$ a discrete ordinal $\llbracket b\rrbracket_{\Sigma_{1}}$ , and the same code $b$ denotes a compact totally separated ordinal $\llbracket b\rrbracket_{\Sigma^{1}}$ . There is an extremely dense order-embedding of the discrete ordinal into the compact totally separated one, which classically is an equivalence but fails to be one constructively.

Definition 6.1 (Brouwer codes).

The type $\mathrm{B}$ of Brouwer ordinal codes (countably branching trees) is inductively generated by the constructors

\mathsf{Z}:\mathrm{B},\qquad\mathsf{S}:\mathrm{B}\to\mathrm{B},\qquad\mathsf{L}:(\mathbb{N}\to\mathrm{B})\to\mathrm{B}.

6.1. The standard interpretation

Definition 6.2.

We define an interpretation function

\llbracket-\rrbracket_{\mathrm{sup}}:\mathrm{B}\to\mathrm{Ord}\qquad\text{(standard interpretation)}

by interpreting the constructors as indicated in the following table:

	$\mathsf{Z}$	$\mathsf{S}$	$\mathsf{L}$
$\llbracket-\rrbracket_{\mathrm{sup}}$	$\mathbf{0}$	$(-)\mathbin{+}\mathbf{1}$	$\sup$

Here $\sup$ is the supremum of an $\mathbb{N}$ -indexed family of ordinals (Theorem 5.29).

The standard interpretation does not produce compact ordinals or trichotomous ordinals constructively, which motivates the alternative interpretations given in Section 6.2.

Proposition 6.3.

If the standard interpretation $\llbracket b\rrbracket_{\mathrm{sup}}$ is compact for every Brouwer code $b$ , then $\mathrm{LPO}$ holds.

Proof.

The code $\mathsf{L}(n\mapsto\mathsf{S}^{n}\,\mathsf{Z})$ is interpreted as the supremum of the finite ordinals, which is $\omega$ , and the compactness of its underlying type $\mathbb{N}$ is $\mathrm{LPO}$ (Examples 4.5(2)). ∎

Proposition 6.4.

If the standard interpretation $\llbracket b\rrbracket_{\mathrm{sup}}$ is trichotomous for every Brouwer code $b$ , then $\mathrm{LPO}$ holds.

Proof.

It suffices to decide, for an arbitrary $u:\mathbb{N}_{\infty}$ , whether $u$ is finite, because deciding finiteness for every conatural number is equivalent to $\mathrm{LPO}$ . So fix $u:\mathbb{N}_{\infty}$ and write $u_{i}:\mathbf{2}$ for its $i$ -th digit under the inclusion $\mathbb{N}_{\infty}\hookrightarrow\mathbf{2}^{\mathbb{N}}$ . From Example 3.1, we have that $u$ is finite exactly when $u\mathrel{\sqsubseteq}i$ for some $i$ .

The codes. Put

	$\displaystyle g\,i$	$\displaystyle\;=\;\mathsf{S}\big(\text{if $u_{i}=0$ then $\mathsf{S}\,\mathsf{Z}$ else $\mathsf{Z}$}\big),$
	$\displaystyle h\,0$	$\displaystyle=\mathsf{S}(\mathsf{S}\,\mathsf{Z}),$
	$\displaystyle h\,1$	$\displaystyle=\mathsf{S}(\mathsf{L}\,g),$
	$\displaystyle h\,(n{+}2)$	$\displaystyle=\mathsf{Z},$

the last clause being arbitrary. Write $\alpha\,i=\llbracket g\,i\rrbracket_{\mathrm{sup}}$ and $\beta=\llbracket\mathsf{L}\,h\rrbracket_{\mathrm{sup}}=\sup_{i}\llbracket h\,i\rrbracket_{\mathrm{sup}}$ . Unfolding Definition 6.2 and using that $\mathbf{0}$ is left neutral for $\mathbin{+}$ ,

	$\displaystyle\alpha\,i$	$\displaystyle=\begin{cases}\mathbf{2}&\text{if }u_{i}=0,\\ \mathbf{1}&\text{if }u_{i}=1,\end{cases}$
	$\displaystyle\llbracket h\,0\rrbracket_{\mathrm{sup}}$	$\displaystyle=\mathbf{2},$
	$\displaystyle\llbracket h\,1\rrbracket_{\mathrm{sup}}$	$\displaystyle=(\sup_{i}\alpha\,i)\mathbin{+}\mathbf{1}.$

The code we associate to $u$ is $\mathsf{L}\,h$ , and the hypothesis gives us that $\beta$ is trichotomous.

Two elements of $\beta$ . We have $\mathbf{1}\mathrel{<}\mathbf{2}$ , and $\llbracket h\,0\rrbracket_{\mathrm{sup}}\mathrel{\leq}\beta$ by Theorem 5.29 (3), so $\mathbf{1}\mathrel{<}\beta$ . Also $\sup_{i}\alpha\,i\mathrel{<}(\sup_{i}\alpha\,i)\mathbin{+}\mathbf{1}=\llbracket h\,1\rrbracket_{\mathrm{sup}}\mathrel{\leq}\beta$ , an ordinal being an element of its own successor, so $\sup_{i}\alpha\,i\mathrel{<}\beta$ . Let $y_{0},y_{1}:\beta$ be the witnesses of these two facts, so that

\beta\mathbin{\downarrow}y_{0}=\mathbf{1},\qquad\beta\mathbin{\downarrow}y_{1}=\sup_{i}\alpha\,i.

Three lemmas. First, the supremum $\sup_{i}\alpha\,i$ has a point: each $\alpha\,i$ , being of the form $\gamma\mathbin{+}\mathbf{1}$ , has the point contributed by the $\mathbf{1}$ summand, and the map $\alpha\,i\to\sup_{i}\alpha\,i$ carries it to a point of the supremum. Hence the inequality $\sup_{i}\alpha\,i\mathrel{<}\mathbf{1}$ is impossible, because an initial segment of $\mathbf{1}$ is $\mathbf{0}$ , which would make $\sup_{i}\alpha\,i$ empty.

Second, if $u$ is finite then $\mathbf{1}\mathrel{<}\sup_{i}\alpha\,i$ . To see this, say $u=\underline{n}$ , so that $u_{n}=0$ and hence $\alpha\,n=\mathbf{2}$ . Now $\mathbf{1}\mathrel{<}\mathbf{2}=\alpha\,n\mathrel{\leq}\sup_{i}\alpha\,i$ .

Third, conversely, the inequality $\mathbf{1}\mathrel{<}\sup_{i}\alpha\,i$ implies that $u$ is finite: being finite is a proposition, so we may use that the maps $\alpha\,i\to\sup_{i}\alpha\,i$ are jointly surjective, which is the surjectivity of the map out of the sum (Theorem 5.29(2)), hence the element of $\sup_{i}\alpha\,i$ whose initial segment is $\mathbf{1}$ comes from some $x:\alpha\,i$ , and initial segments are preserved by the maps into the supremum, which are simulations (Theorem 5.29(3)), so $\mathbf{1}=\alpha\,i\mathbin{\downarrow}x$ , which is to say that $\mathbf{1}\mathrel{<}\alpha\,i$ . Decide the value of $u_{i}$ . If $u_{i}=0$ then $u$ is bounded by $i$ , hence finite. If $u_{i}=1$ then $\alpha\,i=\mathbf{1}$ , giving $\mathbf{1}\mathrel{<}\mathbf{1}$ , which is impossible since $\mathrel{<}$ is irreflexive.

Deciding finiteness. Apply trichotomy of $\beta$ to $y_{0}$ and $y_{1}$ . Since passing to initial segments preserves the order, the three cases for trichotomy read:

(1)

$y_{0}\mathrel{<}y_{1}$ : then $\mathbf{1}\mathrel{<}\sup_{i}\alpha\,i$ , so $u$ is finite by the third lemma.
(2)

$y_{0}=y_{1}$ : then $\mathbf{1}=\sup_{i}\alpha\,i$ . So $u$ is not finite, for were it finite, the second lemma would give $\mathbf{1}\mathrel{<}\mathbf{1}$ .
(3)

$y_{1}\mathrel{<}y_{0}$ : then $\sup_{i}\alpha\,i\mathrel{<}\mathbf{1}$ , which the first lemma rules out, so this case does not arise.

In each case the finiteness of $u$ is decided. ∎

Remark 6.5.

The proof uses the hypothesis of trichotomy only at the single pair $y_{0},y_{1}$ of the single ordinal $\beta$ , and $\beta$ is built from $u$ by a fixed construction. So the statement can be sharpened to give a function assigning to each conatural number a Brouwer code such that trichotomy of the standard interpretation of the code decides the finiteness of the conatural number.

6.2. Three non-standard interpretations

We now give three further interpretations of Brouwer codes, each obtaining a different combination of compactness, total separatedness and trichotomy, and all of them dominating the standard interpretation classically (Theorem 6.15).

Definition 6.6 (Three non-standard interpretations).

We define three interpretation functions

\begin{array}[]{rcll}\llbracket-\rrbracket_{\Sigma}&:&\mathrm{B}\to\mathrm{Ord}_{3}&\text{(trichotomous interpretation)}\\ \llbracket-\rrbracket_{\Sigma^{1}}&:&\mathrm{B}\to\mathrm{Ord}^{\top}&\text{(compact totally separated interpretation)}\\ \llbracket-\rrbracket_{\mathrm{sup}^{1}}&:&\mathrm{B}\to\mathrm{Ord}&\text{(compact interpretation)}\end{array}

by interpreting the constructors as indicated in the following table:

	$\mathsf{Z}$	$\mathsf{S}$	$\mathsf{L}$
$\llbracket-\rrbracket_{\Sigma}$	$\mathbf{0}$	$(-)\mathbin{+}\mathbf{1}$	$\Sigma$
$\llbracket-\rrbracket_{\Sigma^{1}}$	$\mathbf{1}$	$(-)\mathbin{+}\mathbf{1}$	$\Sigma^{1}$
$\llbracket-\rrbracket_{\mathrm{sup}^{1}}$	$\mathbf{1}$	$(-)\mathbin{+}\mathbf{1}$	$\sup\nolimits^{1}$

Here $\Sigma$ is the lexicographic sum over $\omega$ (Definition 5.11), which is an ordinal by Lemma 5.16, the index $\omega$ being trichotomous, $\Sigma^{1}$ is the extended sum (Definition 5.25(1)), and $\sup\nolimits^{1}$ is the extended supremum (Definition 5.32).

In the compact totally separated and the compact interpretation we deliberately map $\mathsf{Z}$ to $\mathbf{1}$ rather than $\mathbf{0}$ , so that every denoted ordinal is pointed and hence the micro-Tychonoff Theorem 4.26 is applicable to get the compactness of the ordinals in their images.

Theorem 6.7.

For every Brouwer code $b$ ,

(1)

the ordinal $\llbracket b\rrbracket_{\Sigma}$ is trichotomous,
(2)

the underlying type of $\llbracket b\rrbracket_{\Sigma^{1}}$ is compact and totally separated,
(3)

the underlying type of $\llbracket b\rrbracket_{\mathrm{sup}^{1}}$ is compact.

Proof.

All by induction on $b$ , with compactness throughout in the pointed sense.

(1) The interpretation lands in $\mathrm{Ord}_{3}$ by construction, each of its clauses preserving trichotomy: $\mathbf{0}$ is trichotomous, so is the successor of a trichotomous ordinal, and so is a sum over $\omega$ of a family of trichotomous ordinals, such a sum being an ordinal by Lemma 5.16. Here $\llbracket-\rrbracket_{\Sigma}$ takes an ordinary $\mathbb{N}$ -indexed sum, with nothing added at a limit.

(2) For compactness, the type $\mathbf{1}$ is compact pointed. The successor clause is a sum over $\mathbf{1}+\mathbf{1}$ , so Corollary 4.10(2) applies. The limit clause is Theorem 4.32. For total separatedness, the type $\mathbf{1}$ is totally separated. The successor clause is a $\Sigma$ whose index type $\mathbf{1}+\mathbf{1}$ is discrete, and total separatedness is closed under $\Sigma$ over a discrete index (Proposition 3.12). For the limit clause, apply Lemma 3.14: each fiber is totally separated by Lemma 4.34 and the induction hypothesis, and the fiber at $\infty$ is $\mathbf{1}$ by Lemma 4.31(2).

(3) $\mathbf{1}$ is compact pointed and the successor clause is a coproduct. The limit clause is the one place where the argument differs from (2), because $\llbracket\mathsf{L}\,b\rrbracket_{\mathrm{sup}^{1}}$ is a supremum rather than a sum, and it is Theorem 5.31. ∎

Being trichotomous, $\llbracket b\rrbracket_{\Sigma}$ is discrete (Lemma 5.8).

Proposition 6.8.

If $\llbracket b\rrbracket_{\Sigma}$ is compact for every Brouwer code $b$ , then $\mathrm{LPO}$ holds.

Proof.

Apply the hypothesis to the code $\mathsf{L}(\lambda i.\,\mathsf{S}\,\mathsf{Z})$ , whose interpretation is the sum over $\omega$ of the constant family at $\mathbf{0}\mathbin{+}\mathbf{1}$ , so that its underlying type is $\Sigma_{i:\mathbb{N}}\,(\mathbf{0}+\mathbf{1})$ . The first projection makes $\mathbb{N}$ a retract of it, compactness is closed under retracts (Theorem 4.8(4)), and the compactness of $\mathbb{N}$ is $\mathrm{LPO}$ (Examples 4.5(2)). ∎

Unlike $\llbracket-\rrbracket_{\Sigma^{1}}$ (Theorem 6.7(2)), the compact interpretation $\llbracket-\rrbracket_{\mathrm{sup}^{1}}$ fails to give totally separated ordinals constructively:

Proposition 6.9.

If $\llbracket b\rrbracket_{\mathrm{sup}^{1}}$ is totally separated for every Brouwer code $b$ , then $\neg\neg\mathrm{WLPO}$ holds.

This follows from the following counterexample, which does not mention Brouwer codes and says that compact totally separated types fail to be closed under suprema constructively.

Example 6.10.

There are a type $I$ and a family $\beta:I\to\mathrm{Ord}$ such that $I$ is compact pointed and totally separated, $\beta\,i$ is compact pointed and totally separated for every $i:I$ , and the total separatedness of $\sup\beta$ implies $\neg\neg\mathrm{WLPO}$ .

We may take $I=\mathbb{N}_{\infty}$ and for $\beta$ the extension $\bar{\alpha}$ along $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ of the constant family $\alpha:\mathbb{N}\to\mathrm{Ord}$ with value $\mathbf{2}$ . The proof, which requires a number of lemmas, uses the following explicit description of this supremum:

\mathfrak{s}\;:\equiv\;\sup\bar{\alpha}.

By Definition 4.30, since $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ is an embedding whose fiber over $u$ is the proposition that $u$ is finite,

\bar{\alpha}\,u\;=\;\mathbf{2}^{\text{$u$ is finite}}.

Its elements are partial elements of $\mathbf{2}$ , with the finiteness of $u$ as domain of definition, so that $\mathfrak{s}$ is the type of such partial elements, which we will show to be order equivalent to the following Sierpiński ordinal.

Definition 6.11 (A Sierpiński ordinal).

Call a proposition semidecidable if it is equivalent to the finiteness of some conatural number,

\textstyle\exists_{u:\mathbb{N}_{\infty}}\,\big(P\simeq\text{$u$ is finite}\big),

which is a proposition. Let

\mathbb{S}\;:\equiv\;\Sigma_{P:\Omega_{\mathcal{U}_{0}}}\,(\text{$P$ is semidecidable}),\qquad t\mathrel{<_{\mathbb{S}}}t^{\prime}\;:\equiv\;\neg\,\delta t\times\delta t^{\prime}

where $\delta$ is the first projection, the domain of definition. Write $\bot_{\mathbb{S}}$ and $\top_{\mathbb{S}}$ for the elements given by $\mathbf{0}$ and $\mathbf{1}$ , which are semidecidable via $\infty$ and $0$ respectively.

Lemma 6.12.

The relation $\mathrel{<_{\mathbb{S}}}$ is a well-order, so $\mathbb{S}$ is an ordinal, and two of its elements are equal precisely when their domains of definition are logically equivalent.

Proof.

Being semidecidable is a proposition, so $\mathbb{S}$ is a subtype of $\Omega_{\mathcal{U}_{0}}$ , and hence two of its elements are equal exactly when their domains of definition are logically equivalent. In particular $\mathbb{S}$ is a set. The relation $\mathrel{<_{\mathbb{S}}}$ is proposition valued, being a product of two propositions, and transitive, since $t\mathrel{<_{\mathbb{S}}}t^{\prime}$ and $t^{\prime}\mathrel{<_{\mathbb{S}}}t^{\prime\prime}$ give $\neg\,\delta t$ from the first and $\delta t^{\prime\prime}$ from the second. For extensionality, suppose $t$ and $t^{\prime}$ have the same predecessors. If $\delta t$ holds then $\bot_{\mathbb{S}}\mathrel{<_{\mathbb{S}}}t$ , hence $\bot_{\mathbb{S}}\mathrel{<_{\mathbb{S}}}t^{\prime}$ , whose second component is $\delta t^{\prime}$ , and symmetrically. So the domains of definition are logically equivalent, and $t=t^{\prime}$ . For well-foundedness, if $u\mathrel{<_{\mathbb{S}}}v\mathrel{<_{\mathbb{S}}}t$ then $u\mathrel{<_{\mathbb{S}}}v$ gives $\delta v$ while $v\mathrel{<_{\mathbb{S}}}t$ gives $\neg\,\delta v$ , a contradiction, so no predecessor of $t$ has a predecessor, and every element of $\mathbb{S}$ is accessible after two steps. ∎

Lemma 6.13.

There is an order equivalence $\mathfrak{s}\simeq_{o}\mathbb{S}$ .

Proof.

For each $u:\mathbb{N}_{\infty}$ let $\theta_{u}:\bar{\alpha}\,u\to\mathfrak{s}$ be the canonical map into the supremum. These maps are simulations (Theorem 5.29(3)) and jointly surjective (Theorem 5.29(2)), and they preserve initial segments, a simulation mapping the initial segment of $\xi$ onto that of its value, so that $\mathfrak{s}\mathbin{\downarrow}\theta_{u}\,\xi=\bar{\alpha}\,u\mathbin{\downarrow}\xi$ .

Send a partial element $\xi:\mathbf{2}^{\text{$u$ finite}}$ to the proposition $\mathcal{F}\,\xi:\equiv\Sigma_{\varphi}\,\xi\,\varphi=1$ , that is, the proposition that $\xi$ is defined and takes the value $1$ . This is a proposition, because the finiteness of $u$ is a proposition and $\mathbf{2}$ is a set, and it is semidecidable, because from $\xi$ we build a decreasing binary sequence, whose value at $i$ is $1$ before $u$ is known to satisfy $u\mathrel{\sqsubseteq}i$ , and is $1$ minus the value of $\xi$ at the finiteness witness afterwards, hence a conatural number whose finiteness is equivalent to $\mathcal{F}\,\xi$ . Writing $\mathbb{F}\,\xi$ for the resulting element of $\mathbb{S}$ , we check that $\mathbb{F}$ is order-preserving and that it depends on $\xi$ only through $\theta_{u}\,\xi$ , so that it descends to the supremum. Since the $\theta_{u}$ ’s are jointly surjective and $\mathbb{S}$ is a set, there is a unique $\tau:\mathfrak{s}\to\mathbb{S}$ with $\tau\,(\theta_{u}\,\xi)=\mathbb{F}\,\xi$ . It is order-preserving, by joint surjectivity and the corresponding property of $\mathbb{F}$ . It is an initial segment inclusion, because an element of $\mathbb{S}$ below $\tau\,y$ has empty domain of definition, so it is $\bot_{\mathbb{S}}$ , and we exhibit a predecessor of $y$ mapping to $\bot_{\mathbb{S}}$ , namely the image under $\theta_{u}$ of the constantly $0$ partial element, such a predecessor being unique because $\tau$ is left cancellable at $\bot_{\mathbb{S}}$ . So $\tau$ is a simulation. It is surjective, for given $(P,w)$ with $w$ a witness of semidecidability, we may unpack $w$ , because being in the image is a truncated statement, to get $u$ with $P\simeq(\text{$u$ finite})$ , and then the constantly $1$ partial element of $\bar{\alpha}\,u$ is sent to $(P,w)$ . So $\tau$ is an order equivalence by Lemma 5.5. ∎

Lemma 6.14.

If some $p:\mathbb{S}\to\mathbf{2}$ has $p\,\bot_{\mathbb{S}}\neq p\,\top_{\mathbb{S}}$ , then $\mathrm{WLPO}$ holds. Consequently, if $\mathbb{S}$ is totally separated then $\neg\neg\mathrm{WLPO}$ holds.

Proof.

Every $u:\mathbb{N}_{\infty}$ gives an element of $\mathbb{S}$ , namely its own finiteness, which is semidecidable by definition. Write $\hat{u}$ for this element. Then $\widehat{\underline{n}}=\top_{\mathbb{S}}$ for every natural number $n$ , since a natural number is finite, and $\widehat{\infty}=\bot_{\mathbb{S}}$ , since $\infty$ is not. So, given $p$ as in the statement, the composite $q=(u\mapsto p\,\hat{u}):\mathbb{N}_{\infty}\to\mathbf{2}$ takes the constant value $p\,\top_{\mathbb{S}}$ on the natural numbers and the different value $p\,\bot_{\mathbb{S}}$ at $\infty$ . Composing with the complement if necessary, a matter decided by inspecting the two boolean values, we may assume that $q$ is constantly $0$ on $\mathbb{N}$ and takes the value $1$ at $\infty$ . Such a map decides, for an arbitrary $u:\mathbb{N}_{\infty}$ , whether $u=\infty$ , by inspecting the value $q\,u$ , which if $0$ gives $u\neq\infty$ and if $1$ makes $u$ differ from every finite point, since a conatural number that is not finite is $\infty$ . That is $\mathrm{WLPO}$ in the formulation of Definition 2.25.

For the second claim, assume $\mathbb{S}$ is totally separated and, for the sake of contradiction, that $\neg\mathrm{WLPO}$ holds. For any $p:\mathbb{S}\to\mathbf{2}$ we cannot have $p\,\bot_{\mathbb{S}}\neq p\,\top_{\mathbb{S}}$ , by the first part. Deciding the two values, we conclude $p\,\bot_{\mathbb{S}}=p\,\top_{\mathbb{S}}$ . As this holds for every $p$ , total separatedness gives $\bot_{\mathbb{S}}=\top_{\mathbb{S}}$ , which is a contradiction. So $\neg\neg\mathrm{WLPO}$ . ∎

Proof of Example 6.10.

Take $I=\mathbb{N}_{\infty}$ and $\beta=\bar{\alpha}$ . Then $\mathbb{N}_{\infty}$ is compact pointed (Examples 4.7(3)) and totally separated, being a retract of $\mathbf{2}^{\mathbb{N}}$ (Example 3.1), which is totally separated (Examples 3.13(3)), and total separatedness passing to retracts (Proposition 3.12(1)). Each $\bar{\alpha}\,u$ is $\mathbf{2}^{\text{$u$ finite}}$ , which is compact pointed by the micro-Tychonoff Theorem 4.26, and totally separated by closure of total separatedness under products (Proposition 3.12). Finally, if $\sup\bar{\alpha}=\mathfrak{s}$ is totally separated then so is $\mathbb{S}$ , by Lemma 6.13 and closure of total separatedness under equivalence (Proposition 3.12(1)), and then Lemma 6.14 gives $\neg\neg\mathrm{WLPO}$ . ∎

Proof of Proposition 6.9.

Apply the hypothesis to the code $b=\mathsf{L}(\lambda\_.\,\mathsf{S}\,\mathsf{Z})$ . By Definition 6.6, we have that $\llbracket\mathsf{S}\,\mathsf{Z}\rrbracket_{\mathrm{sup}^{1}}=\llbracket\mathsf{Z}\rrbracket_{\mathrm{sup}^{1}}\mathbin{+}\mathbf{1}=\mathbf{1}\mathbin{+}\mathbf{1}$ , which is $\mathbf{2}$ , and therefore $\llbracket b\rrbracket_{\mathrm{sup}^{1}}=\sup\bar{\alpha}=\mathfrak{s}$ , since $\llbracket-\rrbracket_{\mathrm{sup}^{1}}$ sends $\mathsf{Z}$ to $\mathbf{1}$ rather than to $\mathbf{0}$ . So $\mathfrak{s}$ is totally separated, and Lemmas 6.13 and 6.14 give $\neg\neg\mathrm{WLPO}$ . ∎

6.3. Comparing the four interpretations

Classically, the three alternative interpretations dominate the standard interpretation and are related as in Theorem 6.15 below. Excluded middle is used twice, to make the successor operation of $\mathrm{Ord}$ monotone and to turn an order-preserving map between ordinals into $\mathrel{\leq}$ . A fifth interpretation follows in Section 6.4, related to $\llbracket-\rrbracket_{\Sigma^{1}}$ in a stronger and constructive way (Theorem 6.23).

Theorem 6.15.

Assuming the principle of excluded middle, the following order relations hold for the four interpretations of any Brouwer code $b$ :

So the compact totally separated interpretation gives the largest ordinal among the four.

Proof.

The top row, the left-hand column and the bottom row are proved by induction on $b$ . All three use excluded middle at $\mathsf{S}$ , for monotonicity of the successor operation on ordinals , and the top row and the bottom row use it again at $\mathsf{L}$ , for the fact that a supremum is bounded by the corresponding sum. That fact is in turn the passage from an order-preserving map to $\mathrel{\leq}$ , applied to the map $y\mapsto(x,y)$ of a summand into the sum, which makes the sum an upper bound of the family, so that the supremum, being least among upper bounds (Theorem 5.29(3)), is below it. The right-hand column uses the passage directly.

The top row.At $\mathsf{Z}$ both sides are $\mathbf{0}$ . At $\mathsf{S}$ , apply monotonicity of the successor to the induction hypothesis. At $\mathsf{L}$ , the supremum is monotone in its family, so $\sup_{i}\llbracket b\,i\rrbracket_{\mathrm{sup}}\mathrel{\leq}\sup_{i}\llbracket b\,i\rrbracket_{\Sigma}$ , and a supremum is bounded by the corresponding sum, which $\llbracket\mathsf{L}\,b\rrbracket_{\Sigma}$ takes.

The left-hand column.The same shape, with one extra step at $\mathsf{L}$ , where the family being summed on the right is the extension of the family $n\mapsto\llbracket b\,n\rrbracket_{\mathrm{sup}^{1}}$ along $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ , so we first rewrite its value at $\underline{n}$ as $\llbracket b\,n\rrbracket_{\mathrm{sup}^{1}}$ using the extension property (Lemma 4.31 (1)), compare suprema over $\mathbb{N}$ , and then observe that the supremum over $\mathbb{N}$ of a family restricted along $\iota$ is bounded by the supremum over all of $\mathbb{N}_{\infty}$ . At $\mathsf{Z}$ the inequality is $\mathbf{0}\mathrel{\leq}\mathbf{1}$ , the zero ordinal being least.

The bottom row.Again the same, using at $\mathsf{L}$ that extension along an embedding preserves $\mathrel{\leq}$ fiberwise, the extension being at each point a product indexed by a proposition, so that a simulation between the members gives one between the products, and then that suprema compare and that a supremum is bounded by the corresponding sum. At $\mathsf{S}$ we also need that addition of topped ordinals agrees with addition of plain ordinals on underlying ordinals.

The right-hand column.This one is proved differently. We define a map $\llbracket b\rrbracket_{\Sigma}\to\llbracket b\rrbracket_{\Sigma^{1}}$ by induction on $b$ and show that it is order-preserving, and then excluded middle turns an order-preserving map between ordinals into $\mathrel{\leq}$ . At $\mathsf{Z}$ the source is empty. At $\mathsf{S}$ the two summands go to the two summands. At $\mathsf{L}$ the pair $(i,x)$ goes to $\iota\,i$ paired with the partial element that sends a fiber element $(j,p)$ of $\iota$ over $\iota\,i$ to the recursively defined value at $x$ , transported along the identification $j=i$ supplied by left cancellability of $\iota$ . Order preservation is a routine induction. ∎

Proposition 6.16.

(1)

If the relation $\llbracket b\rrbracket_{\mathrm{sup}}\mathrel{\leq}\llbracket b\rrbracket_{\Sigma}$ holds for every Brouwer code $b$ , then $\mathrm{LPO}$ holds.
(2)

If the relation $\llbracket b\rrbracket_{\mathrm{sup}^{1}}\mathrel{\leq}\llbracket b\rrbracket_{\Sigma^{1}}$ holds for every Brouwer code $b$ , then $\neg\neg\mathrm{WLPO}$ holds.

Proof.

(1) An initial segment of a trichotomous ordinal is trichotomous. Since the trichotomous interpretation is trichotomous (Theorem 6.7(1)), the standard interpretation is trichotomous for every code, and Proposition 6.4 gives $\mathrm{LPO}$ .

(2) An embedding into a totally separated type is totally separated. Since $\llbracket b\rrbracket_{\Sigma^{1}}$ is totally separated (Theorem 6.7(2)), $\llbracket b\rrbracket_{\mathrm{sup}^{1}}$ is totally separated for every code, and Proposition 6.9 gives $\neg\neg\mathrm{WLPO}$ . ∎

Question 6.17.

Do each of the remaining two comparisons, namely the relation $\llbracket b\rrbracket_{\mathrm{sup}}\mathrel{\leq}\llbracket b\rrbracket_{\mathrm{sup}^{1}}$ for every code $b$ , and the relation $\llbracket b\rrbracket_{\Sigma}\mathrel{\leq}\llbracket b\rrbracket_{\Sigma^{1}}$ for every code $b$ , imply a constructive taboo?

6.4. A fifth interpretation

Our fifth interpretation is a modification of the trichotomous interpretation $\llbracket-\rrbracket_{\Sigma}$ of Definition 6.6, mapping $\mathsf{Z}$ to the ordinal $\mathbf{1}$ , rather than $\mathbf{0}$ , and $\mathsf{L}$ to $\Sigma_{1}$ in order to match the compact totally separated interpretation $\llbracket-\rrbracket_{\Sigma^{1}}$ and be able to get Theorem 6.23(2).

Definition 6.18.

We define an interpretation function

\llbracket-\rrbracket_{\Sigma_{1}}:\mathrm{B}\to\mathrm{Ord}^{\top}\qquad\text{(alternative trichotomous interpretation)}

by interpreting the constructors as in the second row of the following table, whose first row repeats the compact totally separated interpretation of Definition 6.6 for comparison:

	$\mathsf{Z}$	$\mathsf{S}$	$\mathsf{L}$
$\llbracket-\rrbracket_{\Sigma^{1}}$	$\mathbf{1}$	$(-)\mathbin{+}\mathbf{1}$	$\Sigma^{1}$
$\llbracket-\rrbracket_{\Sigma_{1}}$	$\mathbf{1}$	$(-)\mathbin{+}\mathbf{1}$	$\Sigma_{1}$

Here $\Sigma^{1}$ and $\Sigma_{1}$ are the extended sum and the successor sum of Definition 5.25.

Theorem 6.19.

For every Brouwer code $b$ ,

(1)

the ordinal $\llbracket b\rrbracket_{\Sigma_{1}}$ is trichotomous,
(2)

the ordinal $\llbracket b\rrbracket_{\Sigma^{1}}$ is compact,
(3)

the underlying type of $\llbracket b\rrbracket_{\Sigma_{1}}$ is a retract of $\mathbb{N}$ , hence discrete,
(4)

the underlying type of $\llbracket b\rrbracket_{\Sigma^{1}}$ is a retract of $\mathbf{2}^{\mathbb{N}}$ , hence totally separated.

Notice that (1) gives an alternative route to the discreteness of $\llbracket b\rrbracket_{\Sigma_{1}}$ (Lemma 5.8), whereas (2) does not follow from (4), the compactness of $\mathbf{2}^{\mathbb{N}}$ being independent of our type theory (Remark 4.12).

Proof.

(1) By induction on $b$ . For $\mathsf{Z}$ the one-point ordinal is trichotomous. For $\mathsf{S}$ , ordinal addition $\tau\mathbin{+}\upsilon$ is not a coproduct here but the ordinal-indexed sum over the ordinal $\mathbf{2}$ of the two-element family, whose index type is $\mathbf{1}+\mathbf{1}$ (Section 5.3), and trichotomy is closed under ordinal-indexed sums, the index $\mathbf{2}$ being trichotomous. For $\mathsf{L}$ , the successor sum must preserve trichotomy. Unfolding $\Sigma_{1}$ as the sum over $\omega\mathbin{+}\mathbf{1}$ of the extension of the family along $\mathbb{N}\hookrightarrow\mathbb{N}+\mathbf{1}$ , the index is trichotomous and it remains to see that each fiber of the extension is. A fiber is a product indexed by the fiber of $\mathbb{N}\hookrightarrow\mathbb{N}+\mathbf{1}$ over the point in question, and such a product is trichotomous as soon as that fiber is decidable: if it holds, the product is equivalent to the fiber at its point, and if it fails, the product is empty and hence $\mathbf{1}$ . The fiber is decidable, being either a singleton or empty according to the two cases of $\mathbb{N}+\mathbf{1}$ . Here the two interpretations differ. For $\Sigma^{1}$ the corresponding fibers are those of $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ , whose decidability is exactly $\mathrm{LPO}$ , so the same argument is unavailable.

(2) This is Theorem 6.7(2), proved there by a direct induction with the same three cases, using Corollary 4.10 for $\mathsf{Z}$ and $\mathsf{S}$ , and Theorem 4.32 for $\mathsf{L}$ .

(3) We show by induction on $b$ that $\llbracket b\rrbracket_{\Sigma_{1}}$ is a retract of $\mathbb{N}$ . For $\mathsf{Z}$ the underlying type is $\mathbf{1}$ , a retract of $\mathbb{N}$ . For $\mathsf{S}$ , use that being a retract of $\mathbb{N}$ is closed under $\Sigma$ , in the sense that if $\tau$ and every $\upsilon\,x$ are retracts of $\mathbb{N}$ , then so is $\Sigma_{x}\upsilon\,x$ , being a retract of $\mathbb{N}\times\mathbb{N}$ , which is a retract of $\mathbb{N}$ by a pairing function ; the index type $\mathbf{1}+\mathbf{1}$ of the addition is a retract of $\mathbb{N}$ by sending $0$ to the left point and every successor to the right one. For $\mathsf{L}$ , the interpretation is a successor sum, whose underlying type is a retract of $\mathbb{N}$ as soon as those of the summands are, by Lemma 5.26(2). Discreteness follows since $\mathbb{N}$ is discrete and discreteness is closed under retracts.

(4) Likewise by induction, we show that $\llbracket b\rrbracket_{\Sigma^{1}}$ is a retract of $\mathbf{2}^{\mathbb{N}}$ . For $\mathsf{Z}$ , the type $\mathbf{1}$ is a retract of any pointed type. For $\mathsf{S}$ , we use that $\mathbf{2}^{\mathbb{N}}+\mathbf{2}^{\mathbb{N}}$ is a retract of $\mathbf{2}^{\mathbb{N}}$ (split on the first digit and pass to the tail), and being a retract of $\mathbf{2}^{\mathbb{N}}$ is closed under $+$ . For $\mathsf{L}$ , the induction hypothesis gives, for each $i:\mathbb{N}$ , a section $s_{i}:\llbracket b\,i\rrbracket_{\Sigma^{1}}\to\mathbf{2}^{\mathbb{N}}$ with retraction $\rho_{i}$ . By Lemma 4.35, the extension along $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ of the family $i\mapsto\llbracket b\,i\rrbracket_{\Sigma^{1}}$ is pointwise a retract of the extension of the constant family at $\mathbf{2}^{\mathbb{N}}$ , and hence the extended sum $\llbracket\mathsf{L}\,b\rrbracket_{\Sigma^{1}}$ is a retract of the constant extended sum. By Lemma 4.36, the constant extended sum, the type of delayed binary sequences, is equivalent to $\mathbf{2}^{\mathbb{N}}$ , and in particular a retract of it. Compositions of retracts are retracts.

Total separatedness now follows without a further induction, because $\mathbf{2}^{\mathbb{N}}$ is totally separated (Examples 3.13(3)) and total separatedness is closed under retracts (Proposition 3.12(1)). ∎

Remark 6.20.

Total separatedness is obtained here through $\mathbf{2}^{\mathbb{N}}$ , but a direct induction also works, and the discreteness of $\llbracket b\rrbracket_{\Sigma_{1}}$ is likewise obtained through $\mathbb{N}$ , but also follows directly by induction on $b$ using Proposition 3.6, without passing through $\mathbb{N}$ . Addition is a sum over the discrete index $\mathbf{1}+\mathbf{1}$ , and total separatedness is closed under $\Sigma$ over a discrete index (Proposition 3.12). The index $\mathbb{N}_{\infty}$ of the extended sum is not discrete, its discreteness being $\mathrm{WLPO}$ (Examples 3.3), but Lemma 3.14 applies, the fiber at $\infty$ being $\mathbf{1}$ . That is the route taken in Theorem 6.7. Closure under $\Sigma$ fails in general (Examples 3.13(1)), and being a retract of $\mathbf{2}^{\mathbb{N}}$ is a stronger property that implies total separatedness and is closed under the constructions used here.

Each of the two interpretations fails constructively to have the property that the other has.

Proposition 6.21.

(1)

The statement that $\llbracket b\rrbracket_{\Sigma_{1}}$ is compact for every Brouwer code $b$ is equivalent to $\mathrm{LPO}$ .
(2)

If $\llbracket b\rrbracket_{\Sigma^{1}}$ is discrete for every Brouwer code $b$ , then $\mathrm{WLPO}$ holds.

Proof.

For the forward implications, apply the hypotheses to $b=\mathsf{L}(\lambda i.\,\mathsf{Z})$ , the code of Example 6.24, whose discrete interpretation is $\omega\mathbin{+}\mathbf{1}$ with underlying type $\mathbb{N}+\mathbf{1}$ and whose compact one is $\mathbb{N}_{\infty}$ with underlying type $\mathbb{N}_{\infty}$ .

Compactness of $\mathbb{N}+\mathbf{1}$ gives compactness of $\mathbb{N}$ , a retract of it (Theorem 4.8(4)), which is $\mathrm{LPO}$ (Examples 4.5(2)), and discreteness of $\mathbb{N}_{\infty}$ is $\mathrm{WLPO}$ (Examples 3.3). Conversely, $\mathrm{LPO}$ makes $\mathbb{N}$ compact, and $\llbracket b\rrbracket_{\Sigma_{1}}$ is a retract of $\mathbb{N}$ for every $b$ (Theorem 6.19(3)). ∎

So the trichotomy of Theorem 6.19(1) has no counterpart for $\llbracket-\rrbracket_{\Sigma^{1}}$ , since trichotomy implies discreteness (Lemma 5.8).

Definition 6.22 (The comparison map).

The map $\iota_{b}:\llbracket b\rrbracket_{\Sigma_{1}}\to\llbracket b\rrbracket_{\Sigma^{1}}$ is defined by induction on $b$ as follows:

\begin{array}[]{l}\iota_{\mathsf{Z}}=\mathrm{id}\\[1.72218pt] \iota_{\mathsf{S}\,b}\,(\mathrm{inl}\,\star,y)=(\mathrm{inl}\,\star,\iota_{b}\,y)\\[1.72218pt] \iota_{\mathsf{S}\,b}\,(\mathrm{inr}\,\star,y)=(\mathrm{inr}\,\star,y)\\[1.72218pt] \iota_{\mathsf{L}\,b}=\mathfrak{c}_{\upsilon}\circ\Sigma_{1}\big(i\mapsto\iota_{b\,i}\big),\end{array}

where $\mathfrak{c}_{\upsilon}$ is the comparison map of Definition 5.27 for the family $\upsilon\,i=\llbracket b\,i\rrbracket_{\Sigma^{1}}$ .

Theorem 6.23.

For every Brouwer code $b$ , the map $\iota_{b}:\llbracket b\rrbracket_{\Sigma_{1}}\to\llbracket b\rrbracket_{\Sigma^{1}}$ is

(1)

an embedding,
(2)

extremely dense,
(3)

order-preserving,
(4)

order-reflecting.

Proof.

The four properties are established by induction on $b$ , with the induction for the embedding property simultaneous with the order-reflection property. At $\mathsf{Z}$ the map is the identity. At $\mathsf{S}$ it is a map of sums, with the identity on the index and with the induction hypothesis and the identity on the two fibers, so that the embedding property and the density come from Lemma 2.29(2, 3) and the two order properties from Lemma 5.14. The embedding hypothesis of Lemma 5.14(2) is what makes the two inductions simultaneous, and the index map is the identity here, so it is met.

At $\mathsf{L}$ , the family of maps $\iota_{b\,i}$ induces a map between the successor sums, namely $\mathrm{inl}\,(i,x)\mapsto\mathrm{inl}\,(i,\iota_{b\,i}\,x)$ and $\mathrm{inr}\,\star\mapsto\mathrm{inr}\,\star$ , which preserves all four properties fiberwise, and the comparison map $\mathfrak{c}_{\upsilon}$ for the family $\upsilon\,i=\llbracket b\,i\rrbracket_{\Sigma^{1}}$ has all four (Lemma 5.28), so the composite does too, being extremely dense and being an embedding both closed under composition. The map $\mathfrak{c}_{\upsilon}$ changes the added top point from an isolated one to a limit point (cf. Definition 7.13). ∎

The first code whose interpretations are both infinite shows the extent of the failure of the comparison embedding to be an equivalence.

Example 6.24.

Take $b=\mathsf{L}(\lambda i.\,\mathsf{Z})$ , the countable sum of the one-point code. By Definition 6.18 the two interpretations are the successor and the extended sum of the constant family at $\mathbf{1}$ ,

\llbracket b\rrbracket_{\Sigma_{1}}=\Sigma_{1}\big(i\mapsto\mathbf{1}\big)\simeq_{o}\big(\omega\mathbin{+}\mathbf{1}\big),\qquad\llbracket b\rrbracket_{\Sigma^{1}}=\Sigma^{1}\big(i\mapsto\mathbf{1}\big)\simeq_{o}\mathbb{N}_{\infty},

the summands being one-point ordinals and a sum of those being its own index, so the discrete side is $\mathbb{N}+\mathbf{1}$ with its added point isolated, because the point of $\mathbf{1}$ is isolated and $\mathrm{inr}$ preserves isolatedness (Proposition 3.6(1)), the compact side is $\mathbb{N}_{\infty}$ with its added point $\infty$ a limit (Section 5.4), and $\iota_{b}$ is the inclusion $\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ that sends the added point to $\infty$ .

The ordinal $\llbracket b\rrbracket_{\Sigma_{1}}$ is discrete and a retract of $\mathbb{N}$ , but it is compact exactly when $\mathrm{LPO}$ holds, since $\mathbb{N}$ is (Examples 4.5). The ordinal $\llbracket b\rrbracket_{\Sigma^{1}}$ is compact and totally separated with no assumption (Theorem 6.19 (2 and 4)), but it is discrete, equivalently its top point is isolated, exactly when $\mathrm{WLPO}$ holds (Examples 3.3). The map between them is an extremely dense order-embedding, by Theorem 6.23. Read as binary sequences, the image of $\iota_{b}$ consists of the sequences $1^{n}0^{\omega}$ and the sequence $1^{\omega}$ . Extreme density of $\iota_{b}$ says that no decreasing binary sequence lies outside this image, which is a theorem, and surjectivity says that every decreasing binary sequence lies in it, which for this code is exactly $\mathrm{LPO}$ .

Proposition 6.25.

The statement that $\iota_{b}$ is an equivalence for every Brouwer code $b$ is equivalent to $\mathrm{LPO}$ .

Proof.

For the forward direction, apply the hypothesis to the code $\mathsf{L}(\lambda i.\,\mathsf{Z})$ , where $\iota_{b}$ is the inclusion $\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ , which is an equivalence exactly when $\mathrm{LPO}$ holds (Example 6.24). Conversely, assume $\mathrm{LPO}$ and induct on $b$ , following the clauses of Definition 6.22. At $\mathsf{Z}$ the map is the identity. At $\mathsf{S}\,b$ it is a map of sums whose index part is the identity and whose two fiber parts are the induction hypothesis and the identity, so it is an equivalence by Lemma 2.29(1). At $\mathsf{L}\,b$ the map between the successor sums induced by the family $\iota_{b\,i}$ is an equivalence by the induction hypothesis, and $\mathfrak{c}_{\upsilon}$ is one because $\mathrm{LPO}$ makes $\iota_{1}$ an equivalence, the maps $e_{z}$ being equivalences anyway (Lemma 5.28). ∎

6.5. The least element property

The compact ordinals $\llbracket b\rrbracket_{\Sigma^{1}}$ are not just compact. Every complemented subset has an infimum, which is a member when the subset is non-empty.

Definition 6.26 (Infima of complemented subsets).

Let $X$ carry a relation $\leq$ . A complemented subset of $X$ is given by its characteristic function $p:X\to\mathbf{2}$ , whose roots are its elements. Say that $X$ has infima of complemented subsets if for every $p$ there is a point $x_{0}:X$ that is

(1)

a conditional root: if $p$ has a root at all then $x_{0}$ is one,
(2)

the infimum of the roots: $x_{0}\leq x$ for every root $x$ , and $l\leq x_{0}$ for every $l$ that is below all roots.

For a topped ordinal $\tau$ this is taken with respect to the weak order $x\leq y:\equiv\neg\,(y\mathrel{<}x)$ .

Remark 6.27.

Having infima of complemented subsets is a strengthening of pointed compactness, since clause (1) alone already gives it. Given $p$ , take the conditional root $x_{0}$ as a universal witness. If $p\,x_{0}=1$ then $p$ has no root, since a root would force $p\,x_{0}=0$ , and a $\mathbf{2}$ -valued function with no root is constantly $1$ .

Lemma 6.28 (Least element property).

Let $X$ have infima of complemented subsets with respect to a relation $\leq$ . Then every non-empty complemented subset of $X$ has a least element, that is, a member below all members.

Proof.

Let $p$ be the characteristic function of the subset and $x_{0}$ the point supplied by Definition 6.26. Having infima gives compactness, so we can decide whether $p$ has a root, and non-emptiness rules out the absence of one. So $p$ has a root, and then $x_{0}$ is a root by clause (1), and it is below every root by clause (2). ∎

The following strengthens the micro-Tychonoff Theorem 4.26 from compactness to infima.

Theorem 6.29.

Let $X$ be a proposition, $Y:X\to\mathcal{U}$ a family, and, for each $x:X$ , let ${\mathrel{<}}$ be an arbitrary relation on $Y\,x$ , with associated relation $y\leq y^{\prime}:\equiv\neg\,(y^{\prime}\mathrel{<}y)$ . Give $\prod_{x}Y\,x$ the pointwise-derived relation

\varphi\leq\gamma\;:\equiv\;\neg\,\Sigma_{x:X}\,\gamma\,x\mathrel{<}\varphi\,x.

If every $Y\,x$ has infima of ${\mathrel{<}}$ -complemented subsets, in the sense of Definition 6.26, then so does $\prod_{x}Y\,x$ .

Proof.

The construction of the witness is the same as in Theorem 4.26. Given a complemented family on $\prod_{x}Y\,x$ , transport it along the evaluation equivalences $f_{x}$ available at each $x:X$ , take the infimum $\varphi_{0}\,x$ within $Y\,x$ , and assemble these pointwise. If $p$ has a root $\gamma$ , then each transported $\gamma\,x$ is a root in $Y\,x$ , so the infimum $\varphi_{0}\,x$ is a root there, and since $f_{x}^{-1}(\varphi_{0}\,x)=\varphi_{0}$ , this gives $p\,\varphi_{0}=0$ , so that $\varphi_{0}$ is a conditional root. It remains to show that $\varphi_{0}$ is the infimum for the pointwise-derived relation.

To see that $\varphi_{0}$ is a lower bound, note that if $\gamma$ is a root, then for each $x$ the transported $\gamma$ is a root in $Y\,x$ , so $\varphi_{0}\,x\leq\gamma\,x$ , and $\varphi_{0}\leq\gamma$ was defined to be $\neg\,\Sigma_{x:X}\,\gamma\,x\mathrel{<}\varphi_{0}\,x$ , which follows.

To see that it is greatest among lower bounds, let $\psi$ be below every root. We must show $\psi\leq\varphi_{0}$ , which by definition rules out $\varphi_{0}\,x\mathrel{<}\psi\,x$ for every $x$ , so suppose that this holds at some $x$ . Every root of the transported family at that $x$ is the value at $x$ of a root of the original family, and $\psi$ is below the latter, so $\psi\,x$ is below the former. Thus $\psi\,x$ is below all roots of the transported family, and $\varphi_{0}\,x$ is their infimum, so $\psi\,x\leq\varphi_{0}\,x$ , contradicting the supposition. ∎

Theorem 6.30.

For every Brouwer code $b$ , the topped ordinal $\llbracket b\rrbracket_{\Sigma^{1}}$ has infima of complemented subsets.

Proof.

By induction on $b$ , with the same three cases and the same shape as Theorem 6.19, but now with closure properties for infima in place of those for compactness.

For $\mathsf{Z}$ , the one-point ordinal has infima, since the unique point is a conditional root and trivially the infimum. For $\mathsf{S}$ , use that having infima of complemented subsets is closed under ordinal-indexed sums, in the sense that if $\tau$ has them and every $\upsilon\,x$ does, then so does $\Sigma_{\tau}\upsilon$ , the infimum being computed lexicographically. That is, first the infimum in the base of those $x$ whose fiber contains a root, then the infimum within that fiber. This needs the lexicographic weak order on the sum to agree with the weak order derived from the sum’s own strict order. The ordinal $\mathbf{2}$ indexing the addition has infima by inspection of its two points.

For $\mathsf{L}$ , unfold $\Sigma^{1}$ as the sum over the ordinal $\mathbb{N}_{\infty}$ of the extension along $\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ and apply the same closure property. Two things are needed. First, the ordinal $\mathbb{N}_{\infty}$ has infima of complemented subsets, which is the property of its selection function recorded in Examples 4.7(3), that the sequence it returns is a conditional root and the infimum of the set of roots. Second, each fiber of the extended family has infima. This is exactly Theorem 6.29, the micro-Tychonoff theorem for infima, applied to the fiber of the embedding over the point in question, which is a proposition. ∎

By Lemma 6.28, we conclude the following.

Corollary 6.31.

For every Brouwer code $b$ , every non-empty complemented subset of the ordinal $\llbracket b\rrbracket_{\Sigma^{1}}$ has a least element.

By Remark 6.27, Theorem 6.30 subsumes the compactness of Theorem 6.19(2).

For the discrete interpretation the least element property fails constructively.

Proposition 6.32.

The statement that every non-empty complemented subset of the discrete interpretation $\llbracket b\rrbracket_{\Sigma_{1}}$ has a least element, for every Brouwer code $b$ , is equivalent to $\mathrm{LPO}$ .

Proof.

For the forward implication, take $b=\mathsf{L}(\lambda i.\,\mathsf{Z})$ , whose discrete interpretation is $\omega\mathbin{+}\mathbf{1}$ with underlying type $\mathbb{N}+\mathbf{1}$ (Example 6.24). Given $\alpha:\mathbb{N}\to\mathbf{2}$ , consider the complemented subset with characteristic function

p\,(\mathrm{inl}\,n)=\alpha\,n,\qquad p\,(\mathrm{inr}\,\star)=0.

It contains the added point, so it is non-empty, and its least element $x_{0}$ is either $\mathrm{inl}\,n$ for some $n$ , in which case $\alpha\,n=0$ , or the added point, in which case no $\mathrm{inl}\,n$ is a member, since membership would give $x_{0}\leq\mathrm{inl}\,n$ , that is, $\neg(\mathrm{inl}\,n\mathrel{<}\mathrm{inr}\,\star)$ . Inspection of $x_{0}$ tells the two cases apart, and they decide whether $\alpha$ has a root, which is compactness of $\mathbb{N}$ , equivalently $\mathrm{LPO}$ (Examples 4.5(2)).

Conversely, $\mathrm{LPO}$ makes $\iota_{b}$ an equivalence (Proposition 6.25), and it is order-preserving and order-reflecting (Theorem 6.23), so $\llbracket b\rrbracket_{\Sigma_{1}}$ and $\llbracket b\rrbracket_{\Sigma^{1}}$ are order equivalent. Every non-empty complemented subset of $\llbracket b\rrbracket_{\Sigma^{1}}$ has a least element, and this property transfers along the isomorphism. ∎

Remark 6.33.

The forward implication needs only the single code $\mathsf{L}(\lambda i.\,\mathsf{Z})$ , as in Proposition 6.25.

7. An inductive-recursive universe of compact ordinals

In the Brouwer codes (Definition 6.1), the branching of the limit constructor $\mathsf{L}$ is always indexed by $\mathbb{N}$ . We now let the branching of a sum be indexed by an ordinal built at an earlier stage, which requires defining the type $\mathrm{E}$ of codes and their standard interpretation $\Delta$ simultaneously by induction-recursion in the sense of [9, 10, 11]. The codes carry a further interpretationd $\mathrm{K}$ , with an extremely dense embedding $\Delta\nu\hookrightarrow\mathrm{K}\nu$ for every code $\nu:\mathrm{E}$ (Theorem 7.5(2)). The Brouwer codes embed into $\mathrm{E}$ , with the inclusion making $\llbracket-\rrbracket_{\Sigma_{1}}$ commute with $\Delta$ , and $\llbracket-\rrbracket_{\Sigma^{1}}$ with $\mathrm{K}$ (Theorem 7.10). The interpretation $\Delta$ gives trichotomous and hence discrete ordinals (Theorem 7.2), and $\mathrm{K}$ gives compact ordinals with infima of complemented subsets (Theorem 7.5). The compact interpretation $\mathrm{K}$ , however, is no longer totally separated in general (Proposition 7.11), and hence the ordinals witnessing this are denoted by no Brouwer code.

7.1. Ordinal expressions and their discrete interpretation

Definition 7.1 ( $\mathrm{E}$ and $\Delta$ ).

We define, by induction-recursion, a type $\mathrm{E}$ of ordinal expressions by the constructors

\ulcorner\mathbf{1}\urcorner,\ulcorner\omega{+}\mathbf{1}\urcorner:\mathrm{E},\qquad\mathbin{\ulcorner{+}\urcorner},\mathbin{\ulcorner{\times}\urcorner}:\mathrm{E}\to\mathrm{E}\to\mathrm{E},

\ulcorner\Sigma\urcorner:\textstyle\prod_{\nu:\mathrm{E}}\,\big((\Delta\nu\to\mathrm{E})\to\mathrm{E}\big),

simultaneously with the standard, discrete interpretation $\Delta:\mathrm{E}\to\mathrm{Ord}^{\top}$ , by

$\displaystyle\Delta\,\ulcorner\mathbf{1}\urcorner$	$\displaystyle=\mathbf{1}$	$\displaystyle\Delta\,\ulcorner\omega{+}\mathbf{1}\urcorner$	$\displaystyle=\omega\mathbin{+}\mathbf{1}$
$\displaystyle\Delta\,(\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1})$	$\displaystyle=\Delta\nu_{0}\mathbin{+}\Delta\nu_{1}$	$\displaystyle\Delta\,(\nu_{0}\mathbin{\ulcorner{\times}\urcorner}\nu_{1})$	$\displaystyle=\Sigma_{\Delta\nu_{0}}(\lambda\_.\,\Delta\nu_{1})$
$\displaystyle\Delta\,(\ulcorner\Sigma\urcorner\,\nu\,A)$	$\displaystyle=\Sigma_{\Delta\nu}(\Delta\circ A).$

Theorem 7.2.

For every $\nu:\mathrm{E}$ , the underlying type of $\Delta\nu$ is a retract of $\mathbb{N}$ , hence discrete, and moreover the ordinal $\Delta\nu$ is trichotomous.

Proof.

By induction on $\nu$ , which for an inductive-recursive definition means induction by the elimination principle of $\mathrm{E}$ , in which the hypothesis for $\ulcorner\Sigma\urcorner\,\nu\,A$ may use the already-available value $\Delta\nu$ in order to speak about the index type $\Delta\nu$ of $A$ .

For $\ulcorner\mathbf{1}\urcorner$ the underlying type is $\mathbf{1}$ . For $\ulcorner\omega{+}\mathbf{1}\urcorner$ it is $\mathbb{N}+\mathbf{1}$ , which is equivalent to $\mathbb{N}$ . The underlying type of an addition is a binary sum (Definition 5.9), that is, a $\Sigma$ over the index type $\mathbf{1}+\mathbf{1}$ , and that of a multiplication is a $\Sigma$ over a constant family (Definition 5.13), so the cases $\mathbin{\ulcorner{+}\urcorner}$ and $\mathbin{\ulcorner{\times}\urcorner}$ are, as in the proof of Theorem 6.19(3), instances of the closure of “being a retract of $\mathbb{N}$ ” under $\Sigma$ , the index type $\mathbf{1}+\mathbf{1}$ being a retract of $\mathbb{N}$ . So is the case $\ulcorner\Sigma\urcorner\,\nu\,A$ , where $\Delta(\ulcorner\Sigma\urcorner\,\nu\,A)$ is the plain ordinal-indexed sum $\Sigma_{\Delta\nu}(\Delta\circ A)$ , with no extension, whose base $\Delta\nu$ and fibers $\Delta(A\,x)$ are retracts of $\mathbb{N}$ by the induction hypothesis. Restricting the branching to a discrete ordinal keeps the sum countable. Discreteness then follows because $\mathbb{N}$ is discrete and discreteness is closed under retracts (Proposition 3.6(2)).

Trichotomy is proved by a separate induction on the same cases, using that $\mathbf{1}$ is trichotomous, that $\omega$ is and hence so is its successor, and that trichotomy is preserved by ordinal-indexed sums of trichotomous families over a trichotomous index, as in the proof of Theorem 6.19(1), which covers addition and multiplication under the above readings of them as sums. Trichotomy gives a second route to the discreteness of $\Delta\nu$ , by Lemma 5.8. ∎

However, compactness and the least element both fail constructively.

Proposition 7.3.

Each of the following two statements is equivalent to $\mathrm{LPO}$ :

(1)

the type $\Delta\nu$ is compact for every code $\nu:\mathrm{E}$ ,
(2)

every non-empty complemented subset of $\Delta\nu$ has a least element, for every code $\nu:\mathrm{E}$ .

Proof.

(1) Under $\mathrm{LPO}$ the type $\mathbb{N}$ is compact (Examples 4.5(2)), and $\Delta\nu$ is a retract of it by Theorem 7.2, so it is compact too, compactness being closed under retracts (Theorem 4.8(4)). Conversely, the single code $\ulcorner\omega{+}\mathbf{1}\urcorner$ suffices, since $\Delta\ulcorner\omega{+}\mathbf{1}\urcorner$ is $\mathbb{N}+\mathbf{1}$ , which has $\mathbb{N}$ as a retract, so the same closure property gives the compactness of $\mathbb{N}$ , which is $\mathrm{LPO}$ .

(2) The proof is that of Proposition 6.32. In the forward implication the single code $\ulcorner\omega{+}\mathbf{1}\urcorner$ takes the place of $\mathsf{L}(\lambda i.\,\mathsf{Z})$ , its discrete interpretation being $\omega\mathbin{+}\mathbf{1}$ . In the converse, $\mathrm{LPO}$ makes $\iota_{\nu}$ an equivalence (Proposition 7.7(1)), and it is order-preserving and order-reflecting (Theorem 7.5(2)), so $\Delta\nu$ and $\mathrm{K}\nu$ are order equivalent, and the least element property transfers along the order equivalence. ∎

7.2. The compact interpretation

Definition 7.4 ( $\mathrm{K}$ and $\iota_{\nu}$ ).

We simultaneously define

\begin{array}[]{lll}\mathrm{K}&:&E\to\mathrm{Ord}^{\top},\\ \iota_{\nu}&:&\Delta\nu\to\mathrm{K}\nu\end{array}

and prove by induction that $\iota_{\nu}$ is an embedding as follows. For a code $\nu:\mathrm{E}$ and $A:\Delta\nu\to\mathrm{E}$ , write $(\mathrm{K}\circ A)\mathbin{/}\iota_{\nu}$ for the extension along $\iota_{\nu}:\Delta\nu\hookrightarrow\mathrm{K}\nu$ of $\mathrm{K}\circ A:\Delta\nu\to\mathrm{Ord}^{\top}$ to a family $\mathrm{K}\nu\to\mathrm{Ord}^{\top}$ , as illustrated in the following diagram :

We define $\mathrm{K}:\mathrm{E}\to\mathrm{Ord}^{\top}$ and $\iota_{\nu}:\Delta\nu\to\mathrm{K}\nu$ by

$\displaystyle\mathrm{K}\,\ulcorner\mathbf{1}\urcorner$	$\displaystyle=\mathbf{1}$	$\displaystyle\mathrm{K}\,\ulcorner\omega{+}\mathbf{1}\urcorner$	$\displaystyle=\mathbb{N}_{\infty}$
$\displaystyle\mathrm{K}\,(\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1})$	$\displaystyle=\mathrm{K}\nu_{0}\mathbin{+}\mathrm{K}\nu_{1}$	$\displaystyle\mathrm{K}\,(\nu_{0}\mathbin{\ulcorner{\times}\urcorner}\nu_{1})$	$\displaystyle=\Sigma_{\mathrm{K}\nu_{0}}(\lambda\_.\,\mathrm{K}\nu_{1})$
$\displaystyle\mathrm{K}\,(\ulcorner\Sigma\urcorner\,\nu\,A)$	$\displaystyle=\Sigma_{\mathrm{K}\nu}\big((\mathrm{K}\circ A)\mathbin{/}\iota_{\nu}\big)$

$\displaystyle\iota_{\ulcorner\mathbf{1}\urcorner}$	$\displaystyle=\mathrm{id}$	$\displaystyle\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}$	$\displaystyle=\iota_{\mathbf{1}}$
$\displaystyle\iota_{\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1}}\,(\mathrm{inl}\,\star,\,y)$	$\displaystyle=(\mathrm{inl}\,\star,\,\iota_{\nu_{0}}\,y)$	$\displaystyle\iota_{\nu_{0}\mathbin{\ulcorner{\times}\urcorner}\nu_{1}}\,(x,\,y)$	$\displaystyle=(\iota_{\nu_{0}}\,x,\,\iota_{\nu_{1}}\,y)$
$\displaystyle\iota_{\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1}}\,(\mathrm{inr}\,\star,\,y)$	$\displaystyle=(\mathrm{inr}\,\star,\,\iota_{\nu_{1}}\,y)$
$\displaystyle\iota_{\ulcorner\Sigma\urcorner\,\nu\,A}\,(x,\,z)$	$\displaystyle=\big(\iota_{\nu}\,x,\;\varphi_{x}^{-1}(\iota_{A\,x}\,z)\big).$

Here $\iota_{\mathbf{1}}$ is the canonical embedding $\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ sending the added point to $\infty$ , and $\varphi_{x}:\big((\mathrm{K}\circ A)\mathbin{/}\iota_{\nu}\big)(\iota_{\nu}\,x)\simeq_{o}\mathrm{K}(A\,x)$ is the extension property of Lemma 5.21 at the point $\iota_{\nu}\,x$ of the image.

That each $\iota_{\nu}$ is an embedding is proved by the same induction. At $\ulcorner\mathbf{1}\urcorner$ the map is the identity and at $\ulcorner\omega{+}\mathbf{1}\urcorner$ it is the canonical embedding $\iota_{\mathbf{1}}$ , an embedding by Examples 3.3(6). The identity is an embedding, a map of sums is an embedding if its index map and all its fiber maps are (Lemma 2.29(2)), embeddings are closed under composition, and an equivalence is an embedding. At $\mathbin{\ulcorner{+}\urcorner}$ , where the addition is a sum over $\mathbf{1}+\mathbf{1}$ (Definition 5.9), the index map is the identity on $\mathbf{1}+\mathbf{1}$ and the fiber maps are $\iota_{\nu_{0}}$ and $\iota_{\nu_{1}}$ , and at $\mathbin{\ulcorner{\times}\urcorner}$ , where the multiplication is a sum over a constant family (Definition 5.13), the index map is $\iota_{\nu_{0}}$ and the fiber map is $\iota_{\nu_{1}}$ , the maps $\iota_{\nu_{0}}$ and $\iota_{\nu_{1}}$ being embeddings by the induction hypothesis. At $\ulcorner\Sigma\urcorner\,\nu\,A$ the map is the map of sums with index map $\iota_{\nu}$ and fiber maps $\varphi_{x}^{-1}\circ\iota_{A\,x}$ , an embedding as the composition of the embedding $\iota_{A\,x}$ with the equivalence $\varphi_{x}^{-1}$ .

The following generalizes Theorems 6.30 and 6.23.

Theorem 7.5.

For every $\nu:\mathrm{E}$ ,

(1)

the ordinal $\mathrm{K}\nu$ has infima of complemented subsets, hence is compact,
(2)

the embedding $\iota_{\nu}:\Delta\nu\to\mathrm{K}\nu$ is extremely dense, order-preserving and order-reflecting.

Proof.

Write $\mathrm{K}_{\nu,A}\;=\;(\mathrm{K}\circ A)\mathbin{/}\iota_{\nu}\;:\;\mathrm{K}\nu\to\mathrm{Ord}^{\top}$ so that $\mathrm{K}(\ulcorner\Sigma\urcorner\,\nu\,A)=\Sigma_{\mathrm{K}\nu}\,\mathrm{K}_{\nu,A}$ , and by Definition 4.30 its value at $y$ is the product of the $\mathrm{K}(A\,x)$ over the fiber of $\iota_{\nu}$ at $y$ . We prove (1) together with ( $\dagger$ ) by induction on $\nu$ , where

( $\dagger$ )

the ordinal $\mathrm{K}_{\nu,A}\,y$ has infima of complemented subsets for every $A:\Delta\nu\to\mathrm{E}$ and every $y:\mathrm{K}\nu$ .

For (1), the ordinal $\mathbf{1}$ has infima by inspection. The ordinal $\mathbb{N}_{\infty}$ has them, which strengthens the compactness of its underlying type by taking the order into account (Examples 4.7(3)). The cases $\mathbin{\ulcorner{+}\urcorner}$ , $\mathbin{\ulcorner{\times}\urcorner}$ and $\ulcorner\Sigma\urcorner$ are all instances of the closure of this property under ordinal-indexed sums , applied in the last case to the family $\mathrm{K}_{\nu,A}$ , which is where the second half of the induction is used.

For ( $\dagger$ ), the ordinal $\mathrm{K}_{\nu,A}\,y$ is a product of the ordinals $\mathrm{K}(A\,x)$ indexed by $\iota_{\nu}^{-1}(y)$ , which is a proposition because $\iota_{\nu}$ is an embedding, and each factor has infima by the first half of the induction. So Theorem 6.29 applies.

Compactness then follows from Remark 6.27.

(2) That $\iota_{\nu}$ is an embedding is part of Definition 7.4. Each of the three remaining properties is then inherited exactly as in Theorem 6.23. All three are preserved by maps of sums (Lemma 2.29(3) and Lemma 5.14, order reflection requiring, as there, that the index map be an embedding), all three are preserved by composition, and equivalences have all three. The only new base case is $\ulcorner\omega{+}\mathbf{1}\urcorner$ , where $\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ is extremely dense (Examples 3.3(6)) and is order-preserving and order-reflecting for the standard order on $\mathbb{N}_{\infty}$ (Lemma 5.28). ∎

Corollary 7.6.

Every non-empty complemented subset of the ordinal $\mathrm{K}\nu$ has a least element for any $\nu:\mathrm{E}$ .

Proof.

As that of Corollary 6.31, with Theorem 7.5(1) in place of Theorem 6.30. ∎

Classically, the embedding $\iota:\Delta\nu\hookrightarrow\mathrm{K}\nu$ is a surjection and hence an equivalence, but this fails constructively, and so does the discreteness, and hence the trichotomy, of $\mathrm{K}\nu$ .

Proposition 7.7.

(1)

The map $\iota_{\nu}$ is an equivalence for every $\nu:\mathrm{E}$ if and only if $\mathrm{LPO}$ holds.
(2)

$\mathrm{LPO}$ makes $\mathrm{K}\nu$ discrete for every $\nu:\mathrm{E}$ .
(3)

If $\mathrm{K}\nu$ is discrete for every $\nu:\mathrm{E}$ , then $\mathrm{WLPO}$ holds.

Proof.

(1) ( $\Rightarrow$ ) Instantiate at $\nu=\ulcorner\omega{+}\mathbf{1}\urcorner$ , where $\iota_{\nu}$ is the canonical map $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ . If it is an equivalence then every conatural number is either the image of a unique $n:\mathbb{N}$ or is $\infty$ , and the inverse image tells us which, and deciding, for an arbitrary $u$ , whether $u$ is finite is $\mathrm{LPO}$ (as in the proof of Proposition 6.4).

( $\Leftarrow$ ) By induction on $\nu$ . At $\ulcorner\mathbf{1}\urcorner$ the map is the identity. At $\ulcorner\omega{+}\mathbf{1}\urcorner$ , the principle $\mathrm{LPO}$ says exactly that finiteness is decidable, which makes $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ split surjective and hence, being an embedding already (Examples 3.3(6)), an equivalence. At $\mathbin{\ulcorner{+}\urcorner}$ , $\mathbin{\ulcorner{\times}\urcorner}$ and $\ulcorner\Sigma\urcorner$ the map is the map of sums of Definition 7.4, which is an equivalence when its index map and all its fiber maps are (Lemma 2.29(1)). At $\ulcorner\Sigma\urcorner$ the fiber map is additionally composed with the equivalence $\varphi_{x}^{-1}$ , which does not affect the conclusion.

(2) Under $\mathrm{LPO}$ the map $\iota_{\nu}$ is an equivalence for every $\nu$ by (1), so $\mathrm{K}\nu$ is discrete, being equivalent to the discrete type $\Delta\nu$ (Theorem 7.2).

(3) Instantiate at $\nu=\ulcorner\omega{+}\mathbf{1}\urcorner$ again, the discreteness of $\mathbb{N}_{\infty}$ being $\mathrm{WLPO}$ , since deciding $u=\infty$ for every $u$ is deciding whether a binary sequence is constantly $1$ . ∎

The embedding $\iota_{\nu}$ is order-preserving and order-reflecting, and it is natural to ask whether it additionally satisfies the initial-segment condition, so that $\Delta\nu\mathrel{\leq}\mathrm{K}\nu$ for all codes $\nu$ . The code $\ulcorner\omega{+}\mathbf{1}\urcorner$ does satisfy this, but the requirement that it holds for every code fails constructively.

Proposition 7.8.

(1)

The canonical embedding $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}:\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ is a simulation, so that $\Delta\ulcorner\omega{+}\mathbf{1}\urcorner\mathrel{\leq}\mathrm{K}\ulcorner\omega{+}\mathbf{1}\urcorner$ .
(2)

The relation $\Delta\nu\mathrel{\leq}\mathrm{K}\nu$ holds for every $\nu:\mathrm{E}$ if and only if $\mathrm{LPO}$ holds.

Proof.

(1) The map is order-preserving (Theorem 7.5(2)). It preserves initial segments because the points of $\mathbb{N}_{\infty}$ below $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}\,z$ are the finite points $\underline{n}$ with $n\mathrel{\sqsubset}\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}\,z$ (Example 5.18), and such a point is the image of $\mathrm{inl}\,n$ , which is below $z$ in $\omega\mathbin{+}\mathbf{1}$ whether $z$ is finite or is the added point.

(2) ( $\Leftarrow$ ) Under $\mathrm{LPO}$ the map $\iota_{\nu}$ is an equivalence (Proposition 7.7(1)), and it is order-preserving and order-reflecting (Theorem 7.5(2)), so it is an order equivalence, and an order equivalence is a simulation.

( $\Rightarrow$ ) The single code $\nu=\ulcorner\omega{+}\mathbf{1}\urcorner\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner$ suffices. Its discrete interpretation is the sum of $\omega\mathbin{+}\mathbf{1}$ and $\mathbf{1}$ , and its compact interpretation is the sum of $\mathbb{N}_{\infty}$ and $\mathbf{1}$ . In both, the right summand contributes the single point $(\mathrm{inr}\,\star,\star)$ , and no point is above it (Definition 5.9), the order of $\mathbf{1}$ being empty.

Let $f$ be a simulation of $\Delta\nu$ into $\mathrm{K}\nu$ . Every point $(\mathrm{inl}\,\star,z)$ of $\Delta\nu$ is below $(\mathrm{inr}\,\star,\star)$ , so its image is below $f\,(\mathrm{inr}\,\star,\star)$ and hence is not $(\mathrm{inr}\,\star,\star)$ , which nothing is above. The image therefore lies in the left summand, giving a map $g:\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ with $f\,(\mathrm{inl}\,\star,z)=(\mathrm{inl}\,\star,\,g\,z)$ .

The map $g$ is a simulation of $\omega\mathbin{+}\mathbf{1}$ into $\mathbb{N}_{\infty}$ . It is order-preserving because $f$ is, and it preserves initial segments because on both sides the points below a point of the left summand are the points of the left summand below it. There is at most one simulation of one ordinal into another (Section 5.1), so $g=\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}$ by (1), and in particular $g$ sends the added point of $\mathbb{N}+\mathbf{1}$ to $\infty$ .

The map $f$ sends $(\mathrm{inr}\,\star,\star)$ to $(\mathrm{inr}\,\star,\star)$ . Otherwise its value there is $(\mathrm{inl}\,\star,w)$ for some $w:\mathbb{N}_{\infty}$ , and, the point $(\mathrm{inl}\,\star,\mathrm{inr}\,\star)$ of $\Delta\nu$ being below $(\mathrm{inr}\,\star,\star)$ , the conatural number $\infty=g\,(\mathrm{inr}\,\star)$ would be below $w$ , whereas $\infty$ is below no conatural number (Example 5.18).

Now let $u:\mathbb{N}_{\infty}$ . The point $(\mathrm{inl}\,\star,u)$ of $\mathrm{K}\nu$ is below $(\mathrm{inr}\,\star,\star)=f\,(\mathrm{inr}\,\star,\star)$ , so initial-segment preservation gives a point of $\Delta\nu$ below $(\mathrm{inr}\,\star,\star)$ whose image it is. That point lies in the left summand, say $(\mathrm{inl}\,\star,z)$ , and then $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}\,z=g\,z=u$ . The assignment $u\mapsto z$ is a section of $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}$ , and deciding whether $z$ is of the form $\mathrm{inl}\,n$ decides whether $u$ is finite, which is $\mathrm{LPO}$ . ∎

7.3. Inclusion of Brouwer codes into inductive-recursive codes

The two notation systems of this paper are related by an inclusion of the first into the second, under which both interpretations are preserved.

Definition 7.9.

The map $\mathfrak{e}:\mathrm{B}\to\mathrm{E}$ is defined by induction, together with the family $A_{b}$ of the limit clause, whose index type $\Delta\ulcorner\omega{+}\mathbf{1}\urcorner$ is $\mathbb{N}+\mathbf{1}$ :

\mathfrak{e}\,\mathsf{Z}=\ulcorner\mathbf{1}\urcorner,\qquad\mathfrak{e}\,(\mathsf{S}\,b)=\mathfrak{e}\,b\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner,\qquad\mathfrak{e}\,(\mathsf{L}\,b)=\ulcorner\Sigma\urcorner\,\ulcorner\omega{+}\mathbf{1}\urcorner\,A_{b},

A_{b}\,(\mathrm{inl}\,n)=\mathfrak{e}\,(b\,n),\qquad A_{b}\,(\mathrm{inr}\,\star)=\ulcorner\mathbf{1}\urcorner.

Theorem 7.10.

The map $\mathfrak{e}$ is an embedding, and for every Brouwer code $b$ ,

(1)

$\llbracket b\rrbracket_{\Sigma_{1}}\simeq_{o}\Delta(\mathfrak{e}\,b)$ ,
(2)

$\llbracket b\rrbracket_{\Sigma^{1}}\simeq_{o}\mathrm{K}(\mathfrak{e}\,b)$ ,

where the interpretations on the left are those of Definition 6.18 and those on the right are those of Definitions 7.1 and 7.4.

Proof.

The map $\mathfrak{e}$ is left cancellable. The constructors of $\mathrm{E}$ have disjoint images and are left cancellable in each argument, so if $\mathfrak{e}\,b=\mathfrak{e}\,b^{\prime}$ then $b$ and $b^{\prime}$ are given by the same constructor of $\mathrm{B}$ , and we argue by induction. At $\mathsf{Z}$ there is nothing to prove. At $\mathsf{S}$ the hypothesis identifies $\mathfrak{e}\,b\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner$ with $\mathfrak{e}\,b^{\prime}\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner$ , hence $\mathfrak{e}\,b$ with $\mathfrak{e}\,b^{\prime}$ , so that $b=b^{\prime}$ by the induction hypothesis. At $\mathsf{L}$ it identifies $\ulcorner\Sigma\urcorner\,\ulcorner\omega{+}\mathbf{1}\urcorner\,A_{b}$ with $\ulcorner\Sigma\urcorner\,\ulcorner\omega{+}\mathbf{1}\urcorner\,A_{b^{\prime}}$ , hence $A_{b}$ with $A_{b^{\prime}}$ , and evaluation at $\mathrm{inl}\,n$ gives $b\,n=b^{\prime}\,n$ for every $n$ , again by the induction hypothesis.

A left-cancellable map into a set is an embedding (Definition 2.10), and $\mathrm{E}$ is a set. For the latter, encode $\mathrm{E}$ into the $\mathrm{W}$ -type with one shape for each of the five constructors, of arities $\mathbf{0}$ , $\mathbf{0}$ , $\mathbf{1}+\mathbf{1}$ , $\mathbf{1}+\mathbf{1}$ and $\mathbf{1}+\mathbb{N}$ . The last of these accommodates $\ulcorner\Sigma\urcorner\,\nu\,A$ , whose branching type $\Delta\nu$ is a retract of $\mathbb{N}$ (Theorem 7.2): the code $\nu$ is recorded at the point of $\mathbf{1}$ and the composite of $A$ with the retraction $\rho:\mathbb{N}\to\Delta\nu$ at the points of $\mathbb{N}$ . This composite determines $A$ , because $\rho\,(\sigma\,x)=x$ for the section $\sigma$ , so that two families with the same composite with $\rho$ take the same value at every point $x$ of $\Delta\nu$ . The encoding is therefore left cancellable, and the $\mathrm{W}$ -type is a set, a $\mathrm{W}$ -type whose type of shapes is a set being one. A type admitting a left-cancellable map into a set is a set, so $\mathrm{E}$ is a set and $\mathfrak{e}$ is an embedding.

The two agreements are proved by induction on $b$ . At $\mathsf{Z}$ both sides are the one-point ordinal. At $\mathsf{S}$ both sides are additions of $\mathbf{1}$ , that is, sums over $\mathbf{1}+\mathbf{1}$ (Definition 5.9) with the same index, so it is enough to compare their two summands, the left ones by the induction hypothesis and the right ones being $\mathbf{1}$ on both sides. Order equivalent families over a common index have order equivalent sums, by Lemma 2.29(1) and Lemma 5.14 with the identity on the index.

At $\mathsf{L}$ both sides are again sums over a common index, so again it is enough to compare the fibers.

In (1) the index is $\omega\mathbin{+}\mathbf{1}$ , whose underlying type is $\mathbb{N}+\mathbf{1}$ . The fibers on the left are the extension of the family $n\mapsto\llbracket b\,n\rrbracket_{\Sigma_{1}}$ along $\mathrm{inl}:\mathbb{N}\hookrightarrow\mathbb{N}+\mathbf{1}$ (Definition 5.25(2)), and those on the right are the values of $\Delta\circ A_{b}$ (Definition 7.1). At $\mathrm{inl}\,n$ the extension gives $\llbracket b\,n\rrbracket_{\Sigma_{1}}$ back (Lemma 5.23), which the induction hypothesis compares with $\Delta(\mathfrak{e}\,(b\,n))$ . At $\mathrm{inr}\,\star$ the fiber of $\mathrm{inl}$ is empty, so the extension is the one-point ordinal (Lemma 4.31(2)), and so is $\Delta\,\ulcorner\mathbf{1}\urcorner$ .

In (2) the index is $\mathbb{N}_{\infty}$ , but the two families are extensions along different embeddings into $\mathbb{N}_{\infty}$ , namely $\iota:\mathbb{N}\hookrightarrow\mathbb{N}_{\infty}$ on the left (Definition 5.25(1)) and $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}:\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ on the right (Definition 7.4). The comparison at a point $u:\mathbb{N}_{\infty}$ is defined on the elements of the two fibers. A point of the fiber on the left is a function $\varphi$ assigning to each $(n,p):\iota^{-1}(u)$ a point of $\llbracket b\,n\rrbracket_{\Sigma^{1}}$ , and it is sent to the function assigning to $(\mathrm{inl}\,n,p):\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}^{-1}(u)$ the image of $\varphi\,(n,p)$ under the induction hypothesis, and to $(\mathrm{inr}\,\star,p)$ the point of the one-point ordinal $\mathrm{K}\,\ulcorner\mathbf{1}\urcorner$ . This is an equivalence, its inverse restricting a function on $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}^{-1}(u)$ along $(n,p)\mapsto(\mathrm{inl}\,n,p)$ and applying the inverse of the induction hypothesis. It is order-preserving and order-reflecting, because a witness of the order relation is given at a point of the fiber, and at $(\mathrm{inr}\,\star,p)$ there is none, the order of the one-point ordinal being empty. ∎

As opposed to the $\llbracket-\rrbracket_{\Sigma_{1}}$ interpretation of Brouwer codes, the $\mathrm{K}$ interpretation of $\mathrm{E}$ codes fails to be totally separated constructively.

Proposition 7.11.

If $\mathrm{K}\nu$ is totally separated for every code $\nu$ , then $\neg\neg\mathrm{WLPO}$ holds.

Proof.

Take $\nu=\ulcorner\Sigma\urcorner\,\ulcorner\omega{+}\mathbf{1}\urcorner\,A$ , where $A$ sends the finite points of $\Delta\ulcorner\omega{+}\mathbf{1}\urcorner$ to $\ulcorner\mathbf{1}\urcorner$ and its added point to $\ulcorner\mathbf{1}\urcorner\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner$ . By Definition 7.4, the ordinal $\mathrm{K}\nu$ is the sum over $\mathbb{N}_{\infty}$ of the extension of $\mathrm{K}\circ A$ along $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}:\mathbb{N}+\mathbf{1}\hookrightarrow\mathbb{N}_{\infty}$ , so a point of its underlying type is a point $u:\mathbb{N}_{\infty}$ together with a function assigning to each element of $\iota_{\ulcorner\omega{+}\mathbf{1}\urcorner}^{-1}(u)$ a point of the corresponding member of the family. The elements with first component $\mathrm{inl}\,n$ contribute the one-point type $\mathrm{K}\,\ulcorner\mathbf{1}\urcorner$ , and the element with first component $\mathrm{inr}\,\star$ , which is available exactly when $u=\infty$ , contributes $\mathrm{K}(\ulcorner\mathbf{1}\urcorner\mathbin{\ulcorner{+}\urcorner}\ulcorner\mathbf{1}\urcorner)$ , which is $\mathbf{1}+\mathbf{1}$ and which we read as $\mathbf{2}$ . Hence

\mathrm{K}\nu\;\simeq\;\textstyle\Sigma_{u:\mathbb{N}_{\infty}}\,\mathbf{2}^{u=\infty},

the type of Examples 3.10(3), whose total separatedness gives $\neg\neg\mathrm{WLPO}$ . Total separatedness is closed under equivalence (Proposition 3.12(1)), so the total separatedness of $\mathrm{K}\nu$ gives $\neg\neg\mathrm{WLPO}$ too. ∎

Remark 7.12.

Since the compact interpretation of a Brouwer code is totally separated (Theorem 6.19(4)) and $\mathrm{K}$ agrees with it along the inclusion of Theorem 7.10, the ordinals witnessing the failure are denoted by no Brouwer code, so that $\mathrm{E}$ denotes strictly more compact ordinals.

7.4. Isolated points and limit points

A point in the image of the embedding $\iota_{\nu}:\Delta\nu\to\mathrm{K}\nu$ can be isolated in $\mathrm{K}\nu$ or a limit point. A boolean valued function on $\Delta\nu$ , defined by induction on the code $\nu$ , determines which of the two holds at each point. Everything in this subsection holds verbatim for the Brouwer codes of Section 6.4, with the same proofs, and we develop it here because the inductive-recursive codes are the more general system.

In classical topology, a limit point is a non-isolated point. Assuming excluded middle in our type theory, every point of any set is isolated, and our ordinals are all sets, so that a point of our ordinals is never non-isolated. In order to overcome this difficulty in the absence of excluded middle but remaining compatible with excluded middle, we define an element to be a limit point when its isolatedness implies $\mathrm{WLPO}$ . We choose this taboo because $\neg\mathrm{WLPO}$ is a weak continuity principle, as discussed in Remark 2.26.

Definition 7.13 (Topological limit point).

A point $x$ of a type is a limit point if its isolatedness implies $\mathrm{WLPO}$ :

\text{$x$ is a limit point}\;:\equiv\;(\text{$x$ is isolated}\to\mathrm{WLPO}).

For example, at the code $\ulcorner\omega{+}\mathbf{1}\urcorner$ , whose compact interpretation is $\mathbb{N}_{\infty}$ , the finite points are isolated while the added point $\infty$ is a limit, its isolatedness being $\mathrm{WLPO}$ (Examples 3.3).

Definition 7.14 (Limit point indicator).

The limit point indicator of a code $\nu$ is the function $\ell_{\nu}:\Delta\nu\to\mathbf{2}$ defined by induction on $\nu$ by

$\displaystyle\ell_{\ulcorner\mathbf{1}\urcorner}(\star)$	$\displaystyle=0$	$\displaystyle\ell_{\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1}}(\mathrm{inl}\,\star,x_{0})$	$\displaystyle=\ell_{\nu_{0}}(x_{0})$
$\displaystyle\ell_{\ulcorner\omega{+}\mathbf{1}\urcorner}(\mathrm{inl}\,n)$	$\displaystyle=0$	$\displaystyle\ell_{\nu_{0}\mathbin{\ulcorner{+}\urcorner}\nu_{1}}(\mathrm{inr}\,\star,x_{1})$	$\displaystyle=\ell_{\nu_{1}}(x_{1})$
$\displaystyle\ell_{\ulcorner\omega{+}\mathbf{1}\urcorner}(\mathrm{inr}\,\star)$	$\displaystyle=1$	$\displaystyle\ell_{\nu_{0}\mathbin{\ulcorner{\times}\urcorner}\nu_{1}}(x_{0},x_{1})$	$\displaystyle=\max(\ell_{\nu_{0}}(x_{0}),\ell_{\nu_{1}}(x_{1}))$
$\displaystyle\ell_{\ulcorner\Sigma\urcorner\,\nu\,A}(x,y)$	$\displaystyle=\max(\ell_{\nu}(x),\ell_{A\,x}(y))$

Theorem 7.15.

For every $\nu:\mathrm{E}$ and $x:\Delta\nu$ ,

(1)

if $\ell_{\nu}(x)=0$ then $\iota_{\nu}\,x$ is isolated in $\mathrm{K}\nu$ ,
(2)

if $\ell_{\nu}(x)=1$ then $\iota_{\nu}\,x$ is a limit point of $\mathrm{K}\nu$ ,
(3)

every point in the image of $\iota_{\nu}$ is either isolated or a limit point,
(4)

if $\neg\mathrm{WLPO}$ holds, isolatedness of $\iota_{\nu}\,x$ is decidable.

Proof.

(1) By induction on $\nu$ , using throughout that a pair is isolated as soon as both of its components are (Proposition 3.6(4)).

At $\ulcorner\mathbf{1}\urcorner$ the unique point is isolated, the type $\mathbf{1}$ being discrete. At $\ulcorner\omega{+}\mathbf{1}\urcorner$ the hypothesis leaves $x=\mathrm{inl}\,n$ , whose image is the finite conatural number $\underline{n}$ , which is isolated (Examples 3.3(4)). At $\mathbin{\ulcorner{+}\urcorner}$ the image is a pair whose index is $\mathrm{inl}\,\star$ or $\mathrm{inr}\,\star$ , isolated in $\mathbf{1}+\mathbf{1}$ (Proposition 3.6(1)), and whose second component is isolated by the induction hypothesis, the value of $\ell$ at the pair being its value at that component. At $\mathbin{\ulcorner{\times}\urcorner}$ and $\ulcorner\Sigma\urcorner$ the hypothesis reads $\max(a,b)=0$ , so that $a=b=0$ and the induction hypothesis applies to both components. This finishes the case $\mathbin{\ulcorner{\times}\urcorner}$ , and in the case $\ulcorner\Sigma\urcorner$ the second component of the image is $\varphi_{x}^{-1}(\iota_{A\,x}\,y)$ (Definition 7.4), which is isolated because $\iota_{A\,x}\,y$ is and equivalences preserve isolatedness (Proposition 3.6(5)).

(2) By induction on $\nu$ , assuming in each case that $\iota_{\nu}\,x$ is isolated and deriving $\mathrm{WLPO}$ .

At $\ulcorner\omega{+}\mathbf{1}\urcorner$ the hypothesis leaves $x=\mathrm{inr}\,\star$ , whose image is $\infty$ , and the isolatedness of $\infty$ is $\mathrm{WLPO}$ (Examples 3.3(5)). The remaining cases pass the assumed isolatedness down to the component that $\ell$ flags, where the induction hypothesis converts it into $\mathrm{WLPO}$ .

At $\mathbin{\ulcorner{+}\urcorner}$ that component is the second one, and isolatedness of a pair gives isolatedness of its second component when the index type is a set (Proposition 3.6(4)), which $\mathbf{1}+\mathbf{1}$ is. At $\mathbin{\ulcorner{\times}\urcorner}$ and $\ulcorner\Sigma\urcorner$ the hypothesis reads $\max(a,b)=1$ , so that $a=1$ or $b=1$ , and the flagged component is the first or the second accordingly. At $\mathbin{\ulcorner{\times}\urcorner}$ the sum is a product, whose components are both isolated with no further hypothesis (same item). At $\ulcorner\Sigma\urcorner$ the first component needs the fibers of the extended family to be compact (Lemma 4.19), which is what the second half of the induction in the proof of Theorem 7.5(1) supplies, and the second component is isolated because $\mathrm{K}\nu$ is a set (Lemma 5.2), which gives the isolatedness of $\varphi_{x}^{-1}(\iota_{A\,x}\,y)$ and hence of $\iota_{A\,x}\,y$ , equivalences reflecting isolatedness (Proposition 3.6(5)).

(3) Decide the value of $\ell_{\nu}(x)$ , which is a point of $\mathbf{2}$ , and apply (1) or (2).

(4) By (3) the point $\iota_{\nu}\,x$ is isolated, in which case isolatedness is decided, or a limit point, in which case its isolatedness implies $\mathrm{WLPO}$ , and contraposing against $\neg\mathrm{WLPO}$ gives that it is not isolated. ∎

Remark 7.16.

A point of an ordinal is an order limit point when it is neither the least element nor a successor. This notion does not agree with the topological notion of limit point (Definition 7.13). The point $(\omega,1)$ of the ordinal $(\omega+1)\times(\omega+1)$ in the lexicographic order is the successor of $(\omega,0)$ , and hence is not an order limit point, but it is a topological limit point, since its isolatedness gives $\mathrm{WLPO}$ , through its first coordinate $\omega$ , a limit point of $\omega+1$ .

8. Discussion

8.1. Summary of results

Table 1. The interpretations of the two notation systems.

Interpretation	Reading of the limit constructor	Holds for every code	Fails constructively
Brouwer codes $b$ (Definition 6.1), limit constructor $\mathsf{L}$
standard $\llbracket b\rrbracket_{\mathrm{sup}}$ in $\mathrm{Ord}$ (Definition 6.2)	supremum	nothing beyond being an ordinal	trichotomy, giving $\mathrm{LPO}$ (Proposition 6.4), and compactness, giving $\mathrm{LPO}$ (Examples 4.5)
$\llbracket b\rrbracket_{\Sigma^{1}}$ in $\mathrm{Ord}^{\top}$ (Definition 6.6)	extended sum	compact and totally separated (Theorem 6.7), a retract of $\mathbf{2}^{\mathbb{N}}$ (Theorem 6.19), and infima of complemented subsets (Theorem 6.30), hence the least element property (Corollary 6.31)	discreteness, giving $\mathrm{WLPO}$ (Proposition 6.21(2)), and hence trichotomy
$\llbracket b\rrbracket_{\mathrm{sup}^{1}}$ in $\mathrm{Ord}$ (Definition 6.6)	supremum of the extension	compact (Theorem 6.7)	total separatedness, giving $\neg\neg\mathrm{WLPO}$ (Proposition 6.9)
$\llbracket b\rrbracket_{\Sigma}$ in $\mathrm{Ord}_{3}$ (Definition 6.6)	sum over $\omega$	trichotomous (Theorem 6.7), hence discrete (Lemma 5.8)	compactness, giving $\mathrm{LPO}$ (Proposition 6.8)
$\llbracket b\rrbracket_{\Sigma_{1}}$ in $\mathrm{Ord}^{\top}$ (Definition 6.18)	successor sum	trichotomous and a retract of $\mathbb{N}$ , hence discrete (Theorem 6.19)	compactness (Proposition 6.21) and the least element property (Proposition 6.32), each equivalent to $\mathrm{LPO}$
Inductive-recursive codes $\nu$ (Definition 7.1), sum constructor $\ulcorner\Sigma\urcorner$
$\Delta\nu$ in $\mathrm{Ord}^{\top}$ (Definition 7.1)	sum over $\Delta\nu$	trichotomous and a retract of $\mathbb{N}$ , hence discrete (Theorem 7.2)	compactness and the least element property, each equivalent to $\mathrm{LPO}$ (Proposition 7.3)
$\mathrm{K}\nu$ in $\mathrm{Ord}^{\top}$ (Definition 7.4)	sum over $\mathrm{K}\nu$ of the extension	compact, with infima of complemented subsets (Theorem 7.5), hence the least element property (Corollary 7.6)	total separatedness, giving $\neg\neg\mathrm{WLPO}$ (Proposition 7.11), and discreteness, giving $\mathrm{WLPO}$ (Proposition 7.7(3))

Table 2. The map

\iota

from the discrete to the compact interpretation, for a Brouwer code

b

and for an

\mathrm{E}

-code

\nu

Property	Status	Reference
Embedding	holds for every code	Theorems 6.23 and 7.4
Extremely dense
Order-preserving
Order-reflecting
Surjective, equivalently an equivalence	fails constructively, and for all codes at once amounts to $\mathrm{LPO}$	Proposition 6.25 and Proposition 7.7(1)

We constructed infinite types that are exhaustively searchable, and called them compact because in many respects they behave like the topological notion of the same name (Section 4). We then noticed that the constructions carry natural well-orders and preserve them, and the ordinals thus obtained measure the logical complexity of the compact types we produced. We gave two notation systems for them, each with several interpretations as ordinals.

The interpretations differ mainly in the reading of the limit constructor, and they are collected in Table 1, which records for each of them what holds and what fails constructively. Total separatedness, one of the properties listed there, is a boolean Leibniz principle corresponding to the topological notion of the same name (Section 3.2). Two of the interpretations are related by an embedding of the discrete one into the compact one (Definitions 6.22 and 6.23), whose properties are collected in Table 2. That embedding needs no assumption, whereas the comparisons among the other interpretations need excluded middle (Theorem 6.15), which for every Brouwer code $b$ gives

\begin{array}[]{ccc}\llbracket b\rrbracket_{\mathrm{sup}}&\mathrel{\leq}&\llbracket b\rrbracket_{\Sigma}\\[4.30554pt] \mathrel{\rotatebox[origin={c}]{-90.0}{$\leqslant$}}&&\mathrel{\rotatebox[origin={c}]{-90.0}{$\leqslant$}}\\[4.30554pt] \llbracket b\rrbracket_{\mathrm{sup}^{1}}&\mathrel{\leq}&\llbracket b\rrbracket_{\Sigma^{1}}\hbox to0.0pt{$.$\hss}\end{array}

The inductive-recursive universe $\mathrm{E}$ carries a discrete and a compact interpretation, $\Delta$ and $\mathrm{K}$ , related by the embedding $\iota$ , as the Brouwer codes do, but its sum constructor is indexed by any previously constructed discrete ordinal rather than by $\mathbb{N}$ (Definitions 7.1 and 7.4). This is possible because the codes and their discrete interpretation are defined simultaneously, so that a code may be indexed by the ordinal denoted by an earlier code. The Brouwer codes are included in it, and the inclusion preserves both interpretations up to order equivalence (Theorem 7.10). Total separatedness of the compact interpretation $\mathrm{K}$ for every code of $\mathrm{E}$ gives $\neg\neg\mathrm{WLPO}$ (Proposition 7.11), whereas the compact interpretation $\llbracket-\rrbracket_{\Sigma^{1}}$ of every Brouwer code is totally separated. The ordinals witnessing the failure are denoted by no Brouwer code.

In the compact ordinals of both systems, every non-empty complemented subset has a least element (Corollarys 6.31 and 7.6). The isolated points and the limit points in the image of the embedding are distinguished by an explicit boolean valued function on the discrete side (Definitions 7.14 and 7.15), and the embedding is an equivalence for every code precisely when $\mathrm{LPO}$ holds (Proposition 6.25 and Proposition 7.7(1)).

Trichotomy of the standard interpretation gives $\mathrm{LPO}$ (Proposition 6.4), the suprema by which it reads the limit constructor not preserving trichotomy, and total separatedness of the interpretation that reads the same constructor by a supremum of an extended family gives $\neg\neg\mathrm{WLPO}$ (Proposition 6.9).

The above constructions rest on the closure properties of compactness (Section 4.3), the micro-Tychonoff theorem for families indexed by a proposition (Theorem 4.26), the extension of a family along an embedding and the sums built from it (Sections 4.7 and 5.4), and suprema of families of ordinals (Section 5.5).

8.2. Reaching large compact ordinals

In [15, §11] we reach compact totally separated ordinals of every rank below $\varepsilon_{0}$ in Gödel’s $T$ , by iterating squashed sums in the Cantor space, and conjecture that this is the best we can do, which Normann proved [36]. If a closed subset of the Baire space has a search functional definable in $T$ , then it is countable and its Cantor–Bendixson rank lies below $\varepsilon_{0}$ . Normann attaches to the functional an evaluation tree, which bounds the rank by the Kleene–Brouwer order type of the tree, and Howard’s estimate of the ordinal complexity of reduction in $T$ puts that order type below $\varepsilon_{0}$ .

Coquand, Hancock and Setzer [6] add the type $\mathrm{B}$ of Definition 6.1 to $T$ as a base type, with its constructors but without its elimination principle, and ask which ordinals are denoted by the closed terms of type $\mathrm{B}$ . They call a point of a type $X$ together with an endomap of $X$ and a map $(\mathbb{N}\to X)\to X$ a limit structure, the generic one being $\mathrm{B}$ itself with $\mathsf{Z}$ , $\mathsf{S}$ and $\mathsf{L}$ . Our interpretations are limit structures in this sense, their main difference being in the third component, which is the supremum for $\llbracket-\rrbracket_{\mathrm{sup}}$ (Definition 6.2), the extended sum for $\llbracket-\rrbracket_{\Sigma^{1}}$ and the successor sum for $\llbracket-\rrbracket_{\Sigma_{1}}$ (Definition 6.18).

In system $T$ they build closed terms denoting $\omega$ , $\omega^{\omega}$ , $\omega^{\omega^{\omega}}$ and so on, so that the ordinal of the system is at least $\varepsilon_{0}$ . They apply a device of Gentzen, which from a predicate $A$ closed under zero, successor and limits of sequences forms $A^{\prime}(x)=\forall y.\,A(y)\to A(y+x)$ and then $A_{1}(x)=A^{\prime}(\omega^{x})$ , again closed under those three operations. Under realizability this transformation turns a limit structure on $X$ into one on $X\to X$ , so that ordinary recursion at higher types replaces transfinite recursion. In the extension of $T$ by one universe of small types, Poincaré’s device of replacing an impredicative intersection by a countable one becomes what they call a lens, a type former $F$ together with a map $FX\to X$ and a way of turning a limit structure on $X$ into one on $FX$ , and every ordinal below $\varphi_{\varepsilon_{0}}0$ is then denoted. This is the easy half of a conjecture of Hancock that one universe reaches exactly those ordinals. In its proof-theoretic form the conjecture reads that $n$ universes have strength $\gamma_{n}$ , where $\gamma_{0}=\varepsilon_{0}$ and $\gamma_{n+1}=\varphi_{\gamma_{n}}0$ , so that $\varphi_{\varepsilon_{0}}0$ is $\gamma_{1}$ . Aczel established this for one universe and Feferman in general, and the limit of the $\gamma_{n}$ is the Feferman–Schütte ordinal $\Gamma_{0}$ (see e.g. [38] for a survey). We can reproduce these constructions in our type theory and evaluate the codes by $\mathrm{K}$ to get compact totally separated ordinals of the same ranks, and so of every rank below $\varphi_{\varepsilon_{0}}0$ .

Our system $\mathrm{E}$ of inductive-recursive codes (Section 7) extends the Brouwer codes, and constructively it denotes strictly more compact ordinals (Remark 7.12).

8.3. Formalization

Every result above was formalized in Agda [35], before this paper was written, in the TypeTopology repository [20], checked with the --safe and --without-K flags, and hence with no postulates, and with the necessary HoTT/UF principles as explicit assumptions of the results that need them. The formalization is spread over the TypeTopology and Ordinals directories in the repository, with auxiliary results in many other directories. For easy reference, we produced a companion Agda file [19] for this paper, which formalizes every definition, lemma, proposition, theorem, example and remark, in the same order and under the same numbering, together with the mathematical claims in running prose outside proofs. Its entries name existing code.

Acknowledgements

Mike Shulman supplied, in personal communication, the counterexample of Remark 5.15, that extensionality of lexicographic sums of ordinals implies excluded middle. Tom de Jong constructed suprema of families of ordinals by set quotients (Section 5.5), and formalized both his construction and ours [7].

References

[1] Michael J. Beeson. Foundations of Constructive Mathematics: Metamathematical Studies. Ergebnisse der Mathematik und ihrer Grenzgebiete, 3. Folge. Springer, Berlin, Heidelberg, 1985.
[2] Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967.
[3] Errett Bishop and Douglas Bridges. Constructive Analysis, volume 279 of Grundlehren der mathematischen Wissenschaften. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.
[4] Douglas Bridges and Luminiţa Simona Vîţă. Techniques of Constructive Analysis. Universitext. Springer, 2006.
[5] Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, Volume 1, Issue 2, 2005.
[6] Thierry Coquand, Peter Hancock, and Anton Setzer. Ordinals in type theory. Invited talk at Computer Science Logic (CSL), Aarhus, 1997. https://www.cse.chalmers.se/~coquand/ordinal.pdf, also archived as https://web.archive.org/web/20251203190938/https://www.cse.chalmers.se/~coquand/ordinal.ps.
[7] Tom de Jong. Domain theory in constructive and predicative univalent foundations. PhD thesis, University of Birmingham, 2023. https://etheses.bham.ac.uk/id/eprint/13401/, also available as arXiv:2301.12405.
[8] Tom de Jong and Martín Hötzel Escardó. Examples and counterexamples of injective types. Annals of Pure and Applied Logic, 178(2), 2027. Available online 8 September 2026.
[9] Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000.
[10] Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications (TLCA 1999), volume 1581 of Lecture Notes in Computer Science, pages 129–146. Springer, 1999.
[11] Peter Dybjer and Anton Setzer. Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66:1–49, 2006.
[12] Martín Hötzel Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21–156, 2004.
[13] Martín Hötzel Escardó. Infinite sets that admit fast exhaustive search. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 443–452. IEEE, 2007.
[14] Martín Hötzel Escardó. Exhaustible sets in higher-type computation. Logical Methods in Computer Science, 4(3):3:3, 37, 2008.
[15] Martín Hötzel Escardó. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, 78(3):764–784, 2013. Revised version: https://martinescardo.github.io/papers/omniscient-journal-revised.pdf.
[16] Martín Hötzel Escardó. Constructive decidability of classical continuity. Mathematical Structures in Computer Science, 25(7):1578–1589, 2015.
[17] Martín Hötzel Escardó. Compact, totally separated and well-ordered types in univalent mathematics. In Types for Proofs and Programs (TYPES 2019), 2019. 4-page abstract, https://martinescardo.github.io/papers/compact-ordinals-Types-2019-abstract.pdf.
[18] Martín Hötzel Escardó. Injective types in univalent mathematics. Mathematical Structures in Computer Science, 2021.
[19] Martín Hötzel Escardó. TypeTopology.CompactTotallySeparatedTypesArticle: an Agda companion to the preprint Compact totally separated types. https://github.com/martinescardo/TypeTopology/blob/0025fb18cda5504f36b74cdbd2a05a8a4e1c1974/source/TypeTopology/CompactTotallySeparatedTypesArticle.lagda, rendered at https://www.cs.bham.ac.uk/~mhe/TypeTopology/TypeTopology.CompactTotallySeparatedTypesArticle.html, 2026. Part of the TypeTopology repository.
[20] Martín Hötzel Escardó et al. TypeTopology: Agda development of univalent mathematics, mainly Type Topology. https://github.com/martinescardo/TypeTopology. Agda repository, continuously developed since 2011.
[21] Martín Hötzel Escardó and Cory M. Knapp. Partial elements and recursion via dominances in univalent type theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 21:1–21:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017.
[22] Martín Hötzel Escardó and Thomas Streicher. The intrinsic topology of Martin-Löf universes. Annals of Pure and Applied Logic, 167(9):794–805, 2016. Fourth Workshop on Formal Topology (4WFTop).
[23] Michael Hedberg. A coherence theorem for Martin-Löf’s type theory. Journal of Functional Programming, 8(4):413–436, 1998.
[24] Martin Hofmann. Extensional concepts in intensional type theory. Technical report ECS-LFCS-95-327, Laboratory for Foundations of Computer Science, University of Edinburgh, 1995. PhD thesis, freely available from https://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/.
[25] Martin Hofmann. Extensional Constructs in Intensional Type Theory. Distinguished Dissertations. Springer, 1997.
[26] J. M. E. Hyland. The effective topos. In A. S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165–216. North-Holland, 1982.
[27] Peter T. Johnstone. On a topological topos. Proceedings of the London Mathematical Society, 38(2):237–271, 1979.
[28] P.T. Johnstone. Stone Spaces. Cambridge University Press, Cambridge, 1982.
[29] Stephen C. Kleene. Countable functionals. Constructivity in Mathematics, pages 81–100, 1959.
[30] Stephen C. Kleene and Richard E. Vesley. The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1965.
[31] Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, and Thorsten Altenkirch. Generalizations of Hedberg’s theorem. In Typed Lambda Calculi and Applications (TLCA 2013), volume 7941 of Lecture Notes in Computer Science, pages 173–188. Springer, 2013.
[32] Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, and Thorsten Altenkirch. Generalizations of Hedberg’s theorem. Logical Methods in Computer Science, 13(1):15:1–15:15, 2017.
[33] Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting constructive notions of ordinals in homotopy type theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), LIPIcs, 2021.
[34] John Longley and Dag Normann. Higher-Order Computability. Theory and Applications of Computability. Springer, 2015.
[35] Ulf Norell, Nils Anders Danielsson, Jesper Cockx, Andreas Abel, et al. Agda.
[36] Dag Normann. On the Cantor–Bendixson rank of a set that is searchable in Gödel’s T. Computability, 5(1):61–74, 2016. Accepted version at https://hdl.handle.net/11250/4673359.
[37] Dag Normann and William Tait. On the computability of the fan functional. In Feferman on Foundations, Outstanding Contributions to Logic. Springer, 2017.
[38] Erik Palmgren. On universes in type theory. In Giovanni Sambin and Jan M. Smith, editors, Twenty-Five Years of Constructive Type Theory, volume 36 of Oxford Logic Guides, pages 191–204. Oxford University Press, 1998.
[39] Andrew M. Pitts. Setoids in intensional type theory. https://arxiv.org/abs/2607.23671, 2026.
[40] Cécilia Pradic and Chad E. Brown. Cantor-Bernstein implies excluded middle, 2019. https://arxiv.org/abs/1904.09193.
[41] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
[42] Egbert Rijke. The join construction, 2017.
[43] Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2025.
[44] Michael Shulman. All $(\infty,1)$ -toposes have strict univalent universes. https://arxiv.org/abs/1904.07004, 2019.
[45] Michael B. Smyth. Power domains and predicate transformers: A topological view. In Josep Díaz, editor, Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18–22, 1983, Proceedings, volume 154 of Lecture Notes in Computer Science, pages 662–675. Springer, 1983.
[46] Michael B. Smyth. Topology. In S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 1: Background: Mathematical Structures, pages 641–761. Oxford University Press, 1992.
[47] A. S. Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer, 1973.
[48] Jaap van Oosten. Realizability: An Introduction to its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 2008.
[49] Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278–1294, 2015.

Full table of contents

Compact totally separated types

Abstract.

0 Contents

1. Introduction

Organization

2. Preliminaries

2.1. Our type theory

Definition 2.1 (Emptiness, negation and decidability).

Definition 2.2 (Logical equivalence).

2.2. Univalent foundations

Definition 2.3 (Singletons).

Definition 2.4 (Homotopy isolated points and sets).

Theorem 2.5 (Hedberg [23]).

Proof.

Definition 2.6 (The type of propositions).

Definition 2.7 (Base and fiber).

Definition 2.8 (Type equivalences).

Definition 2.9 (Surjections and induction along them).

Definition 2.10 (Embeddings).

Definition 2.11 (Complemented families).

Definition 2.12 (Subsets).

Definition 2.13 (Image).

Definition 2.14 (Small and locally small types).

Definition 2.15 (Set replacement).

Definition 2.16 (Set quotients).

2.3. Constructive mathematics

Definition 2.17 (¬¬\neg\neg-separatedness).

Lemma 2.18.

Proof.

Definition 2.19 (Apartness and tightness).

Definition 2.20 (Extreme density).

Proof.

Lemma 2.21.

Proof.

Lemma 2.22.

Proof.

Definition 2.23 (Global choice).

Definition 2.24 (Excluded middle).

Definition 2.25 (Bishop’s principles of omniscience [2]).

Remark 2.26 (Weak topological toposes).

2.4. Retracts and maps of sums

Definition 2.27 (Retracts).

Definition 2.28 (Maps of sums).

Lemma 2.29.

Proof.

3. Totally separated types

Example 3.1.

3.1. Discrete types and isolated points

Definition 3.2 (Isolatedness and discreteness).

Examples 3.3.

Proof.

Lemma 3.4.

Proof.

Remark 3.5.

Proposition 3.6.

Proof.

Lemma 3.7.

Proof.

3.2. Totally separated types

Definition 3.8 (Total separatedness).

Lemma 3.9.

Proof.

Examples 3.10.

Proof of Examples 3.10(2,3).

Proposition 3.11.

Proof.

Proposition 3.12.

Proof.

Examples 3.13.

Proof.

Lemma 3.14.

Proof.

Theorem 3.15.

Proof.

4. Compact types

4.1. Definitions and first examples

Definition 4.1 (Compactness).

Lemma 4.2.

Proof.

Lemma 4.3.

Definition 2.17 ( $\neg\neg$ -separatedness).

4.4. $\exists$ -compactness and $\Pi$ -compactness

Definition 4.30 ( $\Pi$ -extension).