11.5 Compactness of the interval

We already pointed out that our constructions of reals are entirely compatible withclassical logic. Thus, by assuming the law of excluded middle (LABEL:eq:lem) and the axiomof choice (LABEL:eq:ac) we could develop classical analysis, which would essentiallyamount to copying any standard book on analysis.

Nevertheless, anyone interested in computation, for example a numerical analyst, ought tobe curious about developing analysis in a computationally meaningful setting. Thatanalysis in a constructive setting is even possible was demonstrated by [Bishop1967].As a sample of the differences and similarities between classical and constructiveanalysis we shall briefly discuss just one topic—compactness of the closed interval$[0,1]$ and a couple of theorems surrounding the concept.

Compactness is no exception to the common phenomenon in constructive mathematics thatclassically equivalent notions bifurcate. The three most frequently used notions ofcompactness are:

1. metrically compact: “Cauchy complete and totally bounded”,

2. Bolzano–Weierstraß compact: “every sequence has a convergent subsequence”,

3. Heine-Borel compact: “every open cover has a finite subcover”.

These are all equivalent in classical mathematics.Let us see how they fare in homotopy type theory. We can use either the Dedekind or theCauchy reals, so we shall denote the reals just as $ℝ$. We first recall several basicdefinitions.

Definition 11.5.1.

A metric space$\mathrm{(}M\mathrm{,}d\mathrm{)}$ is a set $M$ with a map $d\mathrm{:}M\mathrm{\times }M\mathrm{\to }\mathrm{R}$satisfying, for all $x\mathrm{,}y\mathrm{,}z\mathrm{:}M$,

$d(x,y)$$\ge 0,$$d(x,y)$$=d(y,x),$

$d(x,y)$$=0\iff x=y,$$d(x,z)$$\le d(x,y)+d(y,z).$

Definition 11.5.2.

A Cauchy approximationin $M$ is a sequence $x\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\to }M$ satisfying

The limit of a Cauchy approximation $x\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}\mathrm{\to }M$ is a point $\mathrm{\ell }\mathrm{:}M$satisfying

A complete metric space is one in which every Cauchy approximation has a limit.

Definition 11.5.3.

For a positive rational $ϵ$, an $ϵ$-netin a metric space $\mathrm{(}M\mathrm{,}d\mathrm{)}$ is an element of

In words, this is a finite sequence of points $x_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{x}_n$ such that every pointin $M$ merely is within $ϵ$ of some $x_k$.

A metric space $\mathrm{(}M\mathrm{,}d\mathrm{)}$ is totally boundedwhen it has $ϵ$-nets of allsizes:

Remark 11.5.4.

In the definition of total boundedness we used sloppy notation ${\mathrm{\sum }}_{\mathrm{(}n\mathrm{:}\mathrm{N}\mathrm{)}}{\mathrm{\sum }}_{\mathrm{(}{x}_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{x}_n\mathrm{:}M\mathrm{)}}$. Formally, we should have written ${\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}\mathrm{List}\mathrm{(}M\mathrm{)}\mathrm{)}}$ instead,where $\mathrm{List}\mathit{}\mathrm{(}M\mathrm{)}$ is the inductive type of finite lists from sec:bool-nat.However, that would make the rest of the statement a bit more cumbersome to express.

Note that in the definition of total boundedness we require pure existence of an$ϵ$-net, not mere existence. This way we obtain a function which assigns to each$ϵ:{\mathbb{Q}}_{+}$ a specific $ϵ$-net. Such a function might be called a “modulus oftotal boundedness”. In general, when porting classical metric notions to homotopy typetheory, we should use propositional truncation sparingly, typically so that we avoidasking for a non-constant map from $ℝ$ to $\mathbb{Q}$ or $\mathbb{N}$. For instance, here is the“correct” definition of uniform continuity.

Definition 11.5.5.

A map $f\mathrm{:}M\mathrm{\to }\mathrm{R}$ on a metric space is uniformly continuouswhen

In particular, a uniformly continuous map has a modulus of uniform continuity,which is a function that assigns to each $ϵ$ a corresponding $\delta$.

Let us show that $[0,1]$ is compact in the first sense.

Theorem 11.5.6.

The closed interval $\mathrm{[}\mathrm{0}\mathrm{,}\mathrm{1}\mathrm{]}$ is complete and totally bounded.

Proof.

Given $ϵ:{\mathbb{Q}}_{+}$, there is $n:\mathbb{N}$ such that , so we may take the$ϵ$-net $x_i=i/k$ for $i=0,\mathrm{\dots },k-1$. This is an $ϵ$-net because,for every $y:[0,1]$ there merely exists $i$ such that and , and so .

For completeness of $[0,1]$, consider a Cauchy approximation $x:{\mathbb{Q}}_{+}\to [0,1]$ and let $\mathrm{\ell }$ be its limit in $ℝ$. Since $\max$ and $\min$ are Lipschitz maps,the retraction $r:ℝ\to [0,1]$ defined by $r(x):\equiv \max (0,\min (1,x))$ commuteswith limits of Cauchy approximations, therefore

$$r(\mathrm{\ell })=r(limx)=lim(r\circ x)=r(limx)=\mathrm{\ell },$$

which means that $0\le \mathrm{\ell }\le 1$, as required.∎

We thus have at least one good notion of compactness in homotopy type theory.Unfortunately, it is limited to metric spaces because total boundedness is a metricnotion. We shall consider the other two notions shortly, but first we prove that auniformly continuous map on a totally bounded space has a supremum,i.e. an upper bound which is less than or equal to all other upper bounds.

Theorem 11.5.7.

A uniformly continuous map $f\mathrm{:}M\mathrm{\to }\mathrm{R}$ on a totally bounded metric space$\mathrm{(}M\mathrm{,}d\mathrm{)}$ has a supremum $m\mathrm{:}\mathrm{R}$. For every $ϵ\mathrm{:}{\mathrm{Q}}_{\mathrm{+}}$ there exists $u\mathrm{:}M$ suchthat .

Proof.

Let $h:{\mathbb{Q}}_{+}\to {\mathbb{Q}}_{+}$ be the modulus of uniform continuity of $f$.We define an approximation $x:{\mathbb{Q}}_{+}\to ℝ$ as follows: for any $ϵ:\mathbb{Q}$ totalboundedness of $M$ gives a $h(ϵ)$-net $y_0,\mathrm{\dots },y_n$. Define

$$x_{ϵ}:\equiv \max (f(y_0),\mathrm{\dots },f(y_n)).$$

We claim that $x$ is a Cauchy approximation. Consider any $ϵ,\eta :\mathbb{Q}$, so that

$$x_{ϵ}\equiv \max (f(y_0),\mathrm{\dots },f(y_n))\mathit{\hspace{1em}}\text{and}\mathit{\hspace{1em}}{x}_{\eta }\equiv \max (f(z_0),\mathrm{\dots },f(z_m))$$

for some $h(ϵ)$-net $y_0,\mathrm{\dots },y_n$ and $h(\eta )$-net $z_0,\mathrm{\dots },z_m$.Every $z_i$ is merely $h(ϵ)$-close to some $y_j$, therefore , from which we may conclude that

therefore . Symmetrically we obtain , therefore .

We claim that $m:\equiv limx$ is the supremum of $f$. To prove that $f(x)\le m$ forall $x:M$ it suffices to show . So suppose to the contrary that . There is $ϵ:{\mathbb{Q}}_{+}$ such that . But now merely forsome $y_i$ participating in the definition of $x_{ϵ}$ we get , therefore , a contradiction.

We finish the proof by showing that $m$ satisfies the second part of the theorem, becauseit is then automatically a least upper bound. Given any $ϵ:{\mathbb{Q}}_{+}$, on one hand, and on the other merely for some $y_i$ participating in the definition of $x_{ϵ/2}$,therefore by taking $u:\equiv y_i$ we obtain by triangleinequality.∎

Now, if in ctb-uniformly-continuous-sup we also knew that $M$ were complete, wecould hope to weaken the assumption of uniform continuity to continuity, and strengthenthe conclusion to existence of a point at which the supremum is attained. The usual proofsof these improvements rely on the facts that in a complete totally bounded space

1. continuity implies uniform continuity, and

2. every sequence has a convergent subsequence.

The first statement follows easily from Heine-Borel compactness, and the second is justBolzano–Weierstraß compactness.Unfortunately, these are both somewhat problematic. Letus first show that Bolzano–Weierstraß compactness implies an instance of excluded middleknown as the limited principle of omniscience:for every $\alpha :\mathbb{N}\to \mathrm{𝟐}$,

$$(\sum _{n:\mathbb{N}}\alpha (n)=1_{\mathrm{𝟐}})+(\prod _{n:\mathbb{N}}\alpha (n)=0_{\mathrm{𝟐}}).$$(11.5.8)

Computationally speaking, we would not expect this principle to hold, because it asks us to decidewhether infinitely many values of a function are $0_{\mathrm{𝟐}}$.

Theorem 11.5.9.

Bolzano–Weierstraß compactness of $\mathrm{[}\mathrm{0}\mathrm{,}\mathrm{1}\mathrm{]}$ implies the limited principle of omniscience.

Proof.

Given any $\alpha :\mathbb{N}\to \mathrm{𝟐}$, define the sequence $x:\mathbb{N}\to [0,1]$ by

If the Bolzano–Weierstraß property holds, there exists a strictly increasing $f:\mathbb{N}\to \mathbb{N}$ such that $x\circ f$ is a Cauchy sequence. For a sufficiently large $n:\mathbb{N}$ the $n$-th term $x_{f(n)}$ is within $1/6$ of its limit. Either or$x_{f(n)}>1/3$. If then $x_n$ converges to $0$ and so ${\prod }_{(n:\mathbb{N})}\alpha (n)=0_{\mathrm{𝟐}}$. If $x_{f(n)}>1/3$ then $x_{f(n)}=1$, therefore ${\sum }_{(n:\mathbb{N})}\alpha (n)=1_{\mathrm{𝟐}}$.∎

While we might not mourn Bolzano–Weierstraß compactness too much, it seems harder to livewithout Heine–Borel compactness, as attested by the fact that both classical mathematicsand Brouwer’s Intuitionism accepted it. As we do not want to wade too deeply into generaltopology, we shall work with basic open sets. In the case of $ℝ$ these are the openintervals with rational endpoints. A family of such intervals, indexed by a type $I$,would be a map

with the idea that a pair of rationals $(q,r)$ with determines the type . It is slightly more convenient to allow degenerate intervals as well, so we take afamily of basic intervalsto be a map

$$ℱ:I\to \mathbb{Q}\times \mathbb{Q}.$$

To be quite precise, a family is a dependent pair $(I,ℱ)$, not just$ℱ$. A finite family of basic intervals is one indexed by for some $n:\mathbb{N}$. We usually present it by a finite list $[(q_0,r_0),\mathrm{\dots },(q_{n-1},r_{n-1})]$. Finally, a finite subfamily of $(I,ℱ)$ is givenby a list of indices $[i_1,\mathrm{\dots },i_n]$ which then determine the finite family$[ℱ(i_1),\mathrm{\dots },ℱ(i_n)]$.

As long as we are aware of the distinction between a pair $(q,r)$ and the correspondinginterval , we may safely use the same notation $(q,r)$ forboth. Intersections and inclusions of intervals are expressible in terms of theirendpoints:

$(q,r)\cap (s,t)$$\mathrm{ }:\equiv (\max (q,s),\min (r,t)),$

$(q,r)\subseteq (s,t)$

We say that $(I,\lambda i.(q_i,r_i))$ (pointwise) covers $\mathrm{[}a\mathrm{,}b\mathrm{]}$when

(11.5.10)

The Heine-Borel compactness for $\mathrm{[}\mathrm{0}\mathrm{,}\mathrm{1}\mathrm{]}$states that every covering family of $[0,1]$merely has a finite subfamily which still covers $[0,1]$.

Theorem 11.5.11.

If excluded middle holds then $\mathrm{[}\mathrm{0}\mathrm{,}\mathrm{1}\mathrm{]}$ is Heine-Borel compact.

Proof.

Assume for the purpose of reaching a contradiction that a family $(I,\lambda i.(a_i,b_i))$ covers $[0,1]$ but no finite subfamily does. We construct a sequence of closedintervals $[q_n,r_n]$ which are nested, their sizes shrink to $0$, and none of them is coveredby a finite subfamily of $(I,\lambda i.(a_i,b_i))$.

We set $[q_0,r_0]:\equiv [0,1]$. Assuming $[q_n,r_n]$ has been constructed, let $s:\equiv (2q_n+r_n)/3$ and $t:\equiv (q_n+2r_n)/3$. Both $[q_n,t]$ and $[s,r_n]$are covered by $(I,\lambda i.(a_i,b_i))$, but they cannot both have a finite subcover,or else so would $[q_n,r_n]$. Either $[q_n,t]$ has a finite subcover or it does not.If it does we set $[q_{n+1},r_{n+1}]:\equiv [s,r_n]$, otherwise we set $[q_{n+1},r_{n+1}]:\equiv [q_n,t]$.

The sequences $q_0,q_1,\mathrm{\dots }$ and $r_0,r_1,\mathrm{\dots }$ are both Cauchy and theyconverge to a point $x:[0,1]$ which is contained in every $[q_n,r_n]$.There merely exists $i:I$ such that . Because the sizes of theintervals $[q_n,r_n]$ shrink to zero, there is $n:\mathbb{N}$ such that , but this means that $[q_n,r_n]$ is covered by a single interval $(a_i,b_i)$, while at the same time it has no finite subcover. A contradiction.∎

Without excluded middle, or a pinch of Brouwerian Intuitionism, we seem to be stuck.Nevertheless, Heine-Borel compactness of $[0,1]$ can be recovered in a constructivesetting, in a fashion that is still compatible with classical mathematics! For this to bedone, we need to revisit the notion of cover. The trouble with(11.5.10) is that the truncated existential allows a space tobe covered in any haphazard way, and so computationally speaking, we stand no chance ofmerely extracting a finite subcover. By removing the truncation we get

(11.5.12)

which might help, were it not too demanding of covers. With this definition wecould not even show that $(0,3)$ and $(2,5)$ cover $[1,4]$ because that would amountto exhibiting a non-constant map $[1,4]\to \mathrm{𝟐}$, seeex:reals-non-constant-into-Z. Here we can take a lesson from “pointfree topology”(i.e. locale theory):the notion of cover ought to be expressed in terms of open sets, withoutreference to points. Such a “holistic” view of space will then allow us to analyze thenotion of cover, and we shall be able to recover Heine-Borel compactness. Localetheory uses power sets,which we could obtain by assuming propositional resizing;but instead we can steal ideas from the predicative cousin of locale theory,which is called “formal topology”.

Suppose that we have a family $(I,ℱ)$ and an interval $(a,b)$. How mightwe express the fact that $(a,b)$ is covered by the family, without referring to points?Here is one: if $(a,b)$ equals some $ℱ(i)$ then it is covered by the family.And another one: if $(a,b)$ is covered by some other family $(J,𝒢)$, and inturn each $𝒢(j)$ is covered by $(I,ℱ)$, then $(a,b)$ is covered$(I,ℱ)$. Notice that we are listing rules which can be used todeduce that $(I,ℱ)$ covers $(a,b)$. We should find sufficientlygood rules and turn them into an inductive definition.

Definition 11.5.13.

The inductive cover $\mathrm{◁}$is a mere relation

$$◁:(\mathbb{Q}\times \mathbb{Q})\to \left(\sum _{I:𝒰}(I\to \mathbb{Q}\times \mathbb{Q})\right)\to \mathrm{𝖯𝗋𝗈𝗉}$$

defined inductively by the following rules, where $q\mathrm{,}r\mathrm{,}s\mathrm{,}t$ are rational numbers and$\mathrm{(}I\mathrm{,}\mathrm{F}\mathrm{)}$, $\mathrm{(}J\mathrm{,}\mathrm{G}\mathrm{)}$ are families of basic intervals:

1. reflexivity:$ℱ(i)◁(I,ℱ)$ for all $i:I$,

2. transitivity:if $(q,r)◁(J,𝒢)$ and $\forall (j:J).𝒢(j)◁(I,ℱ)$then $(q,r)◁(I,ℱ)$,

3. monotonicity:if $(q,r)\subseteq (s,t)$ and $(s,t)◁(I,ℱ)$ then $(q,r)◁(I,ℱ)$,

4. localization:if $(q,r)◁(I,ℱ)$ then $(q,r)\cap (s,t)◁(I,\lambda i.(ℱ(i)\cap (s,t)))$.

5. if then $(q,r)◁[(q,t),(r,s)]$,

6. .

The definition should be read as a higher-inductive type in which the listed rules arepoint constructors, and the type is $(-1)$-truncated. The first four clauses are of ageneral nature and should be intuitively clear. The last two clauses are specific to thereal line: one says that an interval may be covered by two intervals if they overlap,while the other one says that an interval may be covered from within. Incidentally, if $r\le q$ then $(q,r)$ is covered by the empty family by the last clause.

Inductive covers enjoy the Heine-Borel property, the proof of which requires a lemma.

Lemma 11.5.14.

Suppose and $\mathrm{(}q\mathrm{,}r\mathrm{)}\mathrm{◁}\mathrm{(}I\mathrm{,}\mathrm{F}\mathrm{)}$. Then there merelyexists a finite subfamily of $\mathrm{(}I\mathrm{,}\mathrm{F}\mathrm{)}$ which inductively covers $\mathrm{(}s\mathrm{,}t\mathrm{)}$.

Proof.

We prove the statement by induction on $(q,r)◁(I,ℱ)$. There aresix cases:

1. Reflexivity: if $(q,r)=ℱ(i)$ then by monotonicity $(s,t)$ is coveredby the finite subfamily $[ℱ(i)]$.

2. Transitivity:suppose $(q,r)◁(J,𝒢)$ and $\forall (j:J).𝒢(j)◁(I,ℱ)$. By the inductive hypothesis there merely exists$[𝒢(j_1),\mathrm{\dots },𝒢(j_n)]$ which covers $(s,t)$.Again by the inductive hypothesis, each of $𝒢(j_k)$ is covered by a finitesubfamily of $(I,ℱ)$, and we can collect these into a finitesubfamily which covers $(s,t)$.

3. Monotonicity:if $(q,r)\subseteq (u,v)$ and $(u,v)◁(I,ℱ)$ then we mayapply the inductive hypothesis to $(u,v)◁(I,ℱ)$ because .

4. Localization:suppose $(q^{\prime },r^{\prime })◁(I,ℱ)$ and $(q,r)=(q^{\prime },r^{\prime })\cap (a,b)$.Because , by the inductive hypothesis there is a finite subcover$[ℱ(i_1),\mathrm{\dots },ℱ(i_n)]$ of $(s,t)$. We also know that , therefore $(s,t)=(s,t)\cap (a,b)$ is covered by$[ℱ(i_1)\cap (a,b),\mathrm{\dots },ℱ(i_n)\cap (a,b)]$, which is afinite subfamily of $(I,\lambda i.(ℱ(i)\cap (a,b)))$.

5. If $(q,r)◁[(q,v),(u,r)]$ for some then by monotonicity$(s,t)◁[(q,v),(u,r)]$.

6. Finally, byreflexivity. ∎

Say that $(I,ℱ)$ inductively covers$\mathrm{[}a\mathrm{,}b\mathrm{]}$ when there merely exists $ϵ:{\mathbb{Q}}_{+}$ such that $(a-ϵ,b+ϵ)◁(I,ℱ)$.

Corollary 11.5.15.

A closed interval is Heine-Borel compact for inductive covers.

Proof.

Suppose $[a,b]$ is inductively covered by $(I,ℱ)$, so there merely is$ϵ:{\mathbb{Q}}_{+}$ such that $(a-ϵ,b+ϵ)◁(I,ℱ)$.By reals-formal-topology-locally-compact there is a finite subcover of$(a-ϵ/2,b+ϵ/2)$, which is therefore a finite subcover of $[a,b]$.∎

Experience from formal topology shows that the rules for inductive covers are sufficientfor a constructive development of pointfree topology. But we can also provide our ownevidence that they are a reasonable notion.

Theorem 11.5.16.

1. An inductive cover is also a pointwise cover.

2. Assuming excluded middle, a pointwise cover is also an inductive cover.

Proof.

1. Consider a family of basic intervals $(I,ℱ)$, where we write $(q_i,r_i):\equiv ℱ(i)$, an interval $(a,b)$ inductively covered by $(I,ℱ)$, and $x$ such that .We prove by induction on $(a,b)◁(I,ℱ)$ that there merelyexists $i:I$ such that . Most cases are pretty obvious, so we showjust two. If $(a,b)◁(I,ℱ)$ by reflexivity, then there merelyis some $i:I$ such that $(a,b)=(q_i,r_i)$ and so . If $(a,b)◁(I,ℱ)$ by transitivity via $(J,\lambda j.(s_j,t_j))$ then bythe inductive hypothesis there merely is $j:J$ such that , and then since$(s_j,t_j)◁(I,ℱ)$ again by the inductive hypothesis there merelyexists $i:I$ such that . Other cases are just as exciting.

2. Suppose $(I,\lambda i.(q_i,r_i))$ pointwise covers $(a,b)$. Bydefn:inductive-cover-interval-2 of defn:inductive-cover itsuffices to show that $(I,\lambda i.(q_i,r_i))$ inductively covers $(c,d)$ whenever, so consider such $c$ and $d$. By classical-Heine-Borelthere is a finite subfamily $[i_1,\mathrm{\dots },i_n]$ which already pointwise covers $[c,d]$, and hence $(c,d)$. Let $ϵ:{\mathbb{Q}}_{+}$ be a Lebesgue numberfor $(q_{i_1},r_{i_1}),\mathrm{\dots },(q_{i_n},r_{i_n})$ as inex:finite-cover-lebesgue-number. There is a positive $k:\mathbb{N}$ such that . For $0\le i\le k$ let

   $$c_k:\equiv ((k-i)c+id)/k.$$

   The intervals $(c_0,c_2)$, $(c_1,c_3)$, …, $(c_{k-2},c_k)$ inductively cover$(c,d)$ by repeated use of transitivity and defn:inductive-cover-interval-1in defn:inductive-cover. Because their widths are below $ϵ$ each ofthem is contained in some $(q_i,r_i)$, and we may use transitivity and monotonicity toconclude that $(I,\lambda i.(q_i,r_i))$ inductively cover $(c,d)$. ∎

The upshot of the previous theorem is that, as far as classical mathematics is concerned,there is no difference between a pointwise and an inductive cover. In particular, since itis consistent to assume excluded middle in homotopy type theory, we cannot exhibit aninductive cover which fails to be a pointwise cover. Or to put it in a different way, thedifference between pointwise and inductive covers is not what they cover but in theproofs that they cover.

We could write another book by going on like this, but let us stop here and hope that wehave provided ample justification for the claim that analysis can be developed in homotopytype theory. The curious reader should consult ex:mean-value-theorem forconstructive versions of the mean value theorem.