classicality axioms suffice to ensure that the usual $\mathbb{R}_{C}$ is
already Cauchy complete, hence coincides with that of [53]:

######  Corollary {AC,C1} .

$\mathbb{R}_{C}$ is Cauchy-complete.

###### Sketch of proof..

Since $\mathbb{R}_{C}$ is discrete by Theorem 8.4 and the quotient map
$\mathcal{C}\to\mathbb{R}_{C}$ is surjective, by Theorem 6.15 there exists a
section of it. Thus, for any Cauchy sequence in $\mathbb{R}_{C}$ there exists
a sequence of sequences of rational numbers, and “diagonalizing” this in the
usual way we obtain a limit in $\mathbb{R}_{C}$. ∎

Finally, we can also nail down the exact relationship between the topology on
the two types of real numbers.

######  Corollary {ACN or LEM, C1} .

$\mathbb{R}_{C}\simeq\flat\mathbb{R}$.

###### Proof.

By section 6.4, $\flat\mathbb{R}_{C}\simeq\flat\mathbb{R}$. But
$\mathbb{R}_{C}$ is discrete, so $\flat\mathbb{R}_{C}\simeq\mathbb{R}_{C}$. ∎

We will return to the question of what the topology on $\mathbb{R}$ itself is
in section 11.

###  8.3. Omniscience principles

We have seen that the ordinary LEM and AC are inconsistent with spatial
interpretations, motivating the introduction of $\sharp$ and $\flat$ in order
to state our modified Axiom LEM and Axiom AC. However, there are weaker
“classicality” principles whose ordinary versions _are_ true in our motivating
model, and some of them can even be proven from our current axioms, such as
the following.

######  Theorem {LEM,C1} 8.5.

The limited principle of omniscience (LPO) holds: for any
$f:\mathbb{N}\to\mathbf{2}$, either there exists an $n:\mathbb{N}$ such that
$f(n)={1_{\mathbf{2}}}$, or $f(n)={0_{\mathbf{2}}}$ for all $n$.

###### Proof.

Since $\mathbb{N}\to\mathbf{2}$ is discrete by section 8.1, we may assume
$f::\mathbb{N}\to\mathbf{2}$ is crisp. Then “$\exists
n.f(n)={1_{\mathbf{2}}}$” is a crisp proposition, so by Axiom LEM we have
either $\exists n.f(n)={1_{\mathbf{2}}}$ or $\neg(\exists
n.f(n)={1_{\mathbf{2}}})$. But $\neg(\exists n.f(n)={1_{\mathbf{2}}})$ is the
same as $(\forall n.f(n)={0_{\mathbf{2}}})$, so we are done. ∎

In particular, this implies that if we define $\mathbb{N}_{\infty}$ as in [13]
to be the type of non-increasing binary sequences $\mathbb{N}\to\mathbf{2}$,
then the canonical map $\mathbb{N}+\mathbf{1}\to\mathbb{N}_{\infty}$ is an
equivalence. In particular, _every_ type in our theory is “indiscrete” in the
sense of [13]. Thus, the “topology” of the types in cohesive type theory is
very different from the “topology” studied by [13].

It is well-known in constructive mathematics that LPO implies the following
weaker classicality principles.

######  Corollary {LEM,C1} .

The lesser limited principle of omniscience (LLPO) holds: for any
$f,g:\mathbb{N}\to\mathbf{2}$, if it is not the case that both $\exists
n.f(n)={1_{\mathbf{2}}}$ and $\exists n.g(n)={1_{\mathbf{2}}}$, then either
$\forall n.f(n)={0_{\mathbf{2}}}$ or $\forall n.g(n)={0_{\mathbf{2}}}$.∎

######  Corollary {LEM,C1} .

Markov’s principle (MP) holds: if $f:\mathbb{N}\to\mathbf{2}$ and $\neg\forall
n.f(n)={0_{\mathbf{2}}}$, then $\exists n.f(n)={1_{\mathbf{2}}}$.∎

It is also well-known that LPO, LLPO, and MP are equivalent to statements
about the order and equality of _Cauchy_ real numbers. Specifically:

  1. (1)

LPO is equivalent to saying that $\mathbb{R}_{C}$ has decidable equality.
(Thus, Theorems 8.5 and 8.2 give an alternative proof of Theorem 8.4.)

  2. (2)

LLPO is equivalent to $\forall x:\mathbb{R}_{C}.(x\leq 0\vee x\geq 0)$, hence
that $\leq$ is a total order on $\mathbb{R}_{C}$.

  3. (3)

MP is equivalent to $\forall x:\mathbb{R}_{C}.(\neg(x\leq 0)\to x>0)$.

Traditionally in constructive mathematics, two real numbers $x,y$ are said to
be apart, written $x\mathbin{\\#}y$, if $|x-y|>0$. We have
$\neg(x\mathbin{\\#}y)\leftrightarrow(x=y)$, but in general, $x\mathbin{\\#}y$
is stronger than $\neg(x=y)$. However, since $x=y$ is equivalent to $|x-y|\leq
0$, Markov’s Principle implies that $x\mathbin{\\#}y$ and $\neg(x=y)$ coincide
for _Cauchy_ reals.

Of course, we are generally more interested in the Dedekind reals $\mathbb{R}$
than the Cauchy ones $\mathbb{R}_{C}$. Toby Bartels has suggested the
following terminology:

  1. (1)

The analytic LPO claims that $\mathbb{R}$ has decidable equality.

  2. (2)

The analytic LLPO claims that $\forall x:\mathbb{R}.(x\leq 0\vee x\geq 0)$.

  3. (3)

The analytic MP claims that $\forall x:\mathbb{R}.(\neg(x\leq 0)\to x>0)$.

Since (assuming Axiom R$\flat$) $\mathbb{R}$ is not discrete (its identity map
is not constant), the analytic LPO is false. Somewhat more surprisingly, we
will prove in Theorem 11.6 that the analytic LLPO is also false. The analytic
Markov’s principle, however, is actually _true_ in our motivating model! I
conjecture that it can even be proven from Axiom LEM and Axiom R$\flat$, but I
have not managed to show this yet. Thus, we assume it as an additional axiom.
Actually, I prefer the following axiom, which is equivalent in the presence of
Axiom LEM.

######  Axiom T.

For any $x:\mathbb{R}$, the proposition $x>0$ is codiscrete.

######  Theorem {LEM,C1,T} 8.6 (Analytic Markov’s Principle).

If $x,y:\mathbb{R}$ satisfy $\neg(x=y)$, then $x\mathbin{\\#}y$. In
particular, if $\neg(x\leq 0)$, then $x>0$.

###### Proof.

By Axiom T, $x\mathbin{\\#}y$ is codiscrete, so by section 8.2 it is
$\neg\neg$-stable. Thus, we can prove it by contradiction. However,
$\neg(x\mathbin{\\#}y)$ means $x=y$, which contradicts the assumption of
$\neg(x=y)$. ∎

Axiom T is arguably the most mysterious part of the theory. Topologically, it
says that the open subset $(0,\infty)$ of $\mathbb{R}$ is a sub _space_ , i.e.
has the induced topology. In other words, it relates the intrinsic “topology”
of $\mathbb{R}$, arising from its definition as a type, to the internal
_ordering_ relation defined on it. Another way to look at it is that it
ensures that the intrinsic “topology” of $\mathbb{R}$ makes it into a
_topological field_ , i.e. that the reciprocal is continuous on the _subspace_
of invertible elements.

Some considerations of models may also help to understand Axiom T.

######  Example .

Axiom T holds in our motivating model of sheaves on the category $\mathcal{C}$
of cartesian spaces $\mathbb{R}^{n}$.

###### Sketch of proof..

This requires recalling a bit about the standard proof that $\mathbb{R}$
inherits the correct topology in this model, which goes as follows
[see][§VI.9]mm:shv-gllin:shtop. For any space $X\in\mathcal{C}$, we have
$\mathrm{Sh}(\mathcal{C})/X\simeq\mathrm{Sh}(\mathcal{C}/X)$, which admits a
local geometric morphism to $\mathrm{Sh}(X)$. Since local geometric morphisms
are orthogonal to grouplike morphisms [19, C3.6.10], and the space of real
numbers is a grouplike locale, to give a real number in
$\mathrm{Sh}(\mathcal{C})/X$ is equivalent to giving a real number in
$\mathrm{Sh}(X)$, or equivalently a map $X\to\mathbb{R}$. Thus, the sections
of the Dedekind real number object over $X$ are the continuous maps
$X\to\mathbb{R}$.

Repeating this argument with $\mathbb{R}$ replaced by the space of _positive_
real numbers, which is also grouplike, we find that the object of positive
reals in $\mathrm{Sh}(\mathcal{C})$ is the sheaf of positive real-valued
functions. To say that this is a codiscrete subobject of the Dedekind reals is
to say that a continuous real-valued function factors through the space of
positive real numbers just when it is positive at every point, which is
obviously true. ∎

The preceding argument depends crucially on the classicality of the base
topos, and in particular the fact that the locale of formal real numbers
(which classifies internal Dedekind real numbers) is spatial. Indeed, we have:

######  Example .

If we start from an arbitrary base topos, and construct a similar topos of
sheaves on the category of cartesian _locales_ $R_{f}^{n}$ (where $R_{f}$
denotes the locale of formal reals), then Axiom T can fail.

###### Sketch of proof..

I am indebted to Bas Spitters for this argument. There exist toposes
(particularly, recursive ones such as the effective topos) in which there are
uniformly continuous functions $f:\mathbb{R}\to\mathbb{R}$ such that $f(x)>0$
for all $x$ but $f$ does not have uniform lower bounds on all finite
intervals. Now since the metric space $\mathbb{R}$ is “locally compact” in the
sense of Bishop, by [38], $f$ extends to a locale morphism $\bar{f}:R_{f}\to
R_{f}$, and since $\mathbb{R}$ is the space of points of $R_{f}$, we still
have $\bar{f}(x)>0$ for all $x$. However, $\bar{f}$ does not factor through
the locale of formal positive reals, since by [39] if it did then it would
have local uniform lower bounds. Thus, we can repeat the proof of section 8.3
until the last sentence, at which point we find that the “obvious” fact is now
false. ∎

Note that the topos of section 8.3 is local over its base and satisfies Axiom
R$\flat$, by the same argument as before. Thus, (modulo section 7) Axiom T
does not follow from Axiom R$\flat$ alone; but I do not know a countermodel to
it that satisfies both Axiom R$\flat$ and Axiom LEM.

##  9\. Shape

Codiscrete types are defined by the fact that functions _into_ them need not
be continuous; while discrete types are defined by the fact that functions
_out_ of them need not be continuous. In a sense, this means that all the
_non-tautological_ information about codiscrete types is carried by the maps
_out_ of them, and likewise the non-trivial information about discrete types
is carried by the maps _into_ them. Let us leave the first for another
day131313But see Theorems 10.2 and 10.3. and concentrate on maps $A\to B$,
where $B$ is discrete.

In the world of classical topological spaces, if $B$ is discrete, then (at
least when $A$ is well-behaved, which at the moment means “locally connected”)
continuous maps $A\to B$ are the same as functions $\pi_{0}(A)\to B$, where
$\pi_{0}(A)$ is the set of connected components of $A$. In other words,
$\pi_{0}$ is a _reflection_ into the subcategory of discrete spaces. Since
$\pi_{0}(A)$ is also the “first layer” of the homotopy type, or fundamental
$\infty$-groupoid, of $A$, this suggests that mapping into discrete spaces can
carry information about the latter construction.

In fact, it turns out that the single generalization from sets to
$\infty$-groupoids ensures that mapping into discrete types carries _all_ the
information about the fundamental $\infty$-groupoid. At least in good
situations, such as our $\infty$-topos of sheaves on the category of cartesian
spaces $\mathbb{R}^{n}$, the fundamental $\infty$-groupoid can be _defined_ as
a left adjoint to the inclusion of discrete spaces [see][Proposition
4.3.32]schreiber:dcct[§3]carchedi:hotyorb. With Axiom R$\flat$ in our theory,
we can get an inkling of how this works internally by considering the
topological circle $\mathbb{S}^{1}$.

######  Definition .

The topological circle $\mathbb{S}^{1}$ is the (homotopy) coequalizer of the
pair of maps

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.68056pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathbb{R}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
12.76389pt\raise 8.27582pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{\mathsf{id}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.68056pt\raise
2.84526pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
11.20833pt\raise-8.39247pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.9639pt\hbox{$\scriptstyle{+1}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
30.68056pt\raise-2.84526pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.68056pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathbb{R}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

We might write this as $\mathbb{S}^{1}\vcentcolon\equiv\mathbb{R}/\mathbb{Z}$.
In Theorem 9.8 we will compare this definition to some other possible
definitions of the topological circle. For now let us simply observe that it
is at least _one_ reasonable definition — with one caveat, namely that
$\mathbb{S}^{1}$ ought to be a set (i.e. have no higher identifications), and
with this definition it is not obvious that this is so. We could, of course,
0-truncate it, but that would defeat the purpose of what we are about to do,
and fortunately it turns out to be unnecessary:

######  Theorem {UA} 9.1.

Suppose $R$ is a set and $f:R\simeq R$ an equivalence such that for all $r:R$
and $m,n:\mathbb{Z}$, if $f^{n}(r)=f^{m}(r)$, then $m=n$. (In other words, the
induced action of $\mathbb{Z}$ on $R$ is free.) Then the homotopy coequalizer
of
$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{id}}$$\scriptstyle{f}$$\textstyle{R}$
is also a set.

###### Proof.

Recall that $S^{1}$ denotes the _homotopical_ circle, a HIT with two
constructors $\mathsf{base}:S^{1}$ and
$\mathsf{loop}:\mathsf{base}=\mathsf{base}$. We define
$P:S^{1}\to\mathsf{Type}$ by $P(\mathsf{base})\vcentcolon\equiv R$ and
$P(\mathsf{loop})=f$ (modulo univalence). Note that $S^{1}$ is the homotopy
coequalizer of $\mathbf{1}\rightrightarrows\mathbf{1}$. Thus, by the
flattening lemma [53, §6.12], the desired homotopy coequalizer of
$\mathsf{id}_{R}$ and $f$ is equivalent to
$\mathchoice{\sum_{x:S^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:S^{1})}}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}}{\mathchoice{{\textstyle\sum_{(x:S^{1})}}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}}{\mathchoice{{\textstyle\sum_{(x:S^{1})}}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}{\sum_{(x:S^{1})}}}P(x)$;
so it will suffice to prove that the latter is a set.

Let $x,y:S^{1}$ and $u:P(x)$, $v:P(y)$; we must prove that $(x,u)=(y,v)$ is a
proposition. Now $(x,u)=(y,v)$ is equivalent to
$\mathchoice{\sum_{p:x=y}\,}{\mathchoice{{\textstyle\sum_{(p:x=y)}}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}}{\mathchoice{{\textstyle\sum_{(p:x=y)}}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}}{\mathchoice{{\textstyle\sum_{(p:x=y)}}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}{\sum_{(p:x=y)}}}(p_{*}u=v)$.
Thus, suppose $p,q:x=y$ and $r:p_{*}u=v$ and $s:q_{*}u=v$; we must show
$(p,r)=(q,s)$. Since $r$ and $s$ are equalities in a set, it suffices to show
$p=q$. But this is also an equality in a set (since $S^{1}$ is a 1-type),
hence a proposition; thus, since $S^{1}$ is connected, we may assume
$x=\mathsf{base}$ and $y=\mathsf{base}$.

Now under the isomorphism $(\mathsf{base}=\mathsf{base})\simeq\mathbb{Z}$, our
$p$ and $q$ get identified with $n,m:\mathbb{Z}$ respectively. Moreover, by
definition of $P$, transporting along $p$ or $q$ gets identified with
application of $f^{n}$ or $f^{m}$ respectively. Thus, from $r$ and $s$ we
obtain $p_{*}u=q_{*}u$ and hence $f^{n}(u)=f^{m}(u)$, with $u:R$, and so the
freeness assumption gives $n=m$ as needed. ∎

######  Remark .

It should be possible to prove Theorem 9.1 using univalence only for
propositions [[, e.g. with]Theorem 7.2.2]hottbook. But the preceding proof is
easier.

######  Corollary {UA} .

The topological circle $\mathbb{S}^{1}$ is a set.

###### Proof.

Since $\mathbb{R}$ is an abelian group, $(+1):\mathbb{R}\to\mathbb{R}$ is an
equivalence. The freeness condition in Theorem 9.1 is equivalent to saying
that the unique ring homomorphism $\mathbb{Z}\to\mathbb{R}$ is injective,
which just says that $\mathbb{R}$ has characteristic 0. ∎

The following proof contains the crucial idea involved in the adjoint
characterization of fundamental $\infty$-groupoids.

######  Theorem {R$\flat$} 9.2.

For any discrete type $X$, we have $(\mathbb{S}^{1}\to X)\simeq(S^{1}\to X)$.

###### Proof.

The universal property of $S^{1}$ means that $(S^{1}\to X)$ is equivalent to

(9.1)
$\mathchoice{\sum_{x:X}\,}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}(x=x).$

But by the universal property of a coequalizer, $(\mathbb{S}^{1}\to X)$ is
equivalent to

(9.2) $\mathchoice{\sum_{g:\mathbb{R}\to
X}\,}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to
X)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to
X)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to X)}}}(g\circ(+1)=g).$

Now $g\circ(+1)=g$ is an equality in the type $\mathbb{R}\to X$, which is
equivalent to $X$ since $X$ is discrete. The equivalence can be implemented by
evaluating at any $r:\mathbb{R}$, such as $0$; thus (9.2) is equivalent to

(9.3) $\mathchoice{\sum_{g:\mathbb{R}\to
X}\,}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to
X)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to
X)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbb{R}\to
X)}}}{\sum_{(g:\mathbb{R}\to X)}}{\sum_{(g:\mathbb{R}\to
X)}}{\sum_{(g:\mathbb{R}\to X)}}}(g(1)=g(0)).$

But since $(\mathbb{R}\to X)\simeq X$, we may assume $g$ is constant at some
$x:X$, giving (9.1). ∎

In particular, the identity map of $S^{1}$ corresponds to a nontrivial map
$\mathbb{S}^{1}\to S^{1}$, which may be said informally to “wrap the
topological circle around the homotopical one”. Since Theorem 9.2 is easily
shown to be natural, this map exhibits $S^{1}$ as a _reflection_ of
$\mathbb{S}^{1}$ into the discrete types. (Recall from Theorem 6.11 that
$S^{1}$ is _topologically_ discrete.)

Since $S^{1}$ is, or should be, the fundamental $\infty$-groupoid of
$\mathbb{S}^{1}$, this leads us to ask: does every type have a reflection into
the discrete types? The answer is yes, and it requires only the much weaker
Axiom C0.

######  Definition {C0} .

For any type $A$, its shape $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is
the higher inductive type with the following five constructors.

  1. (1)

$\sigma_{A}:A\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$

  2. (2)

$\kappa_{A}:\mathchoice{\prod_{i:I}\,}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}(R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$

  3. (3)

For all $i:I$ and $g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ and
$x:R_{i}$, an equality $g(x)=\kappa_{A}(i,g)$.

  4. (4)

$\kappa^{\prime}_{A}:\mathchoice{\prod_{i:I}\,}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}(R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$

  5. (5)

For all $i:I$ and $x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$, an equality
$x=\kappa^{\prime}_{A}(i,\mathsf{const}_{x})$.

######  Remark .

We use the word “shape” not only because it is nine syllables shorter than
“fundamental $\infty$-groupoid”, but because the latter has various
connotations that we want to be free of. In particular, the shape is a purely
internal construction in our “real-cohesive type theory”, although it
generally _behaves like_ the fundamental $\infty$-groupoid. Moreover, the
fundamental $\infty$-groupoid is usually notated $\Pi_{\infty}$, but since
$\Pi$ is rather overworked in type theory already, a different symbol is
preferable. The word “shape” comes from _shape theory_ , which also studies
generalizations of the fundamental $\infty$-groupoid that make sense for less
well-behaved spaces. The symbol $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$
is not an integral sign ($\int$) but an “esh”, the IPA sign for a voiceless
postalveolar fricative (English sh).

The definition of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is cooked up
precisely to admit a map from $A$ and to be discrete:

######  Lemma {C0} .

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is discrete.

###### Proof.

The last four constructors say exactly that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to(R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)$
has both a left and a right inverse. ∎

It is unsurprising, therefore, that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ has the desired universal
property. We express this first as a
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction principle.

######  Theorem {C0} 9.3.

If $P:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to\mathsf{Type}$ is a family
of discrete types, and we have
$d:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(\sigma(x))$,
then we have
$f:\mathchoice{\prod_{y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A}\,}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}P(y)$
such that $f(\sigma(x))=d(x)$ for all $x:A$.

###### Proof.

The “basic” induction principle of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ arising from its higher
inductive definition says that given
$Q:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to\mathsf{Type}$ together with

  1. (1)

$d_{\sigma}:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}Q(\sigma(x))$

  2. (2)

$d_{\kappa}:\mathchoice{\prod_{(i:I)}\,}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}\mathchoice{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}\,}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}\mathchoice{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}\,}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}Q(\kappa(i,g))$

  3. (3)

$d_{=}:\mathchoice{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}\,}{\mathchoice{{\textstyle\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:\mathbb{R}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}\mathchoice{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}\,}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}Q(g(x)))}}}\mathchoice{\prod_{(x:\mathbb{R})}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{R})}}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}{\prod_{(x:\mathbb{R})}}}(h(x)=_{\xi}d_{\kappa}(i,g,h))$,
where $\xi$ is the third constructor of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$,

  4. (4)

$d_{\kappa^{\prime}}:\mathchoice{\prod_{(i:I)}\,}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}\mathchoice{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}\,}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}\mathchoice{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}\,}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\mathchoice{{\textstyle\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}{\prod_{(h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x)))}}}Q(\kappa^{\prime}(i,g))$

  5. (5)

$d_{=^{\prime}}:\mathchoice{\prod_{(i:I)}\,}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}{\mathchoice{{\textstyle\prod_{(i:I)}}}{\prod_{(i:I)}}{\prod_{(i:I)}}{\prod_{(i:I)}}}\mathchoice{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}\,}{\mathchoice{{\textstyle\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}\mathchoice{\prod_{(y:Q(x))}\,}{\mathchoice{{\textstyle\prod_{(y:Q(x))}}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}}{\mathchoice{{\textstyle\prod_{(y:Q(x))}}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}}{\mathchoice{{\textstyle\prod_{(y:Q(x))}}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}{\prod_{(y:Q(x))}}}(y=_{\zeta}d_{\kappa^{\prime}}(i,\mathsf{const}_{x},\mathsf{const}_{y}))$,
where $\zeta$ is the last constructor of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$,

we have
$f:\mathchoice{\prod_{y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A}\,}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}P(y)$
such that $f(\sigma(x))\equiv d_{\sigma}(x)$ (plus four other equalities).
Thus, given our current hypotheses, it remains to construct $d_{\kappa}$,
$d_{=}$, $d_{\kappa^{\prime}}$, and $d_{=^{\prime}}$.

First suppose ${g:R_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A}$ and
${h:\mathchoice{\prod_{x:R_{i}}\,}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}{\mathchoice{{\textstyle\prod_{(x:R_{i})}}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}{\prod_{(x:R_{i})}}}Q(g(x))}$,
for some $i$. By the third constructor of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$, we have $g(x)=\kappa(i,g)$ for
all $x:R_{i}$. Thus, transporting $h(x)$ along these equalities, we get
$h^{\prime}:R_{i}\to Q(\kappa(i,g))$. Thus, since $Q(\kappa(i,g))$ is
discrete, there is a $d_{\kappa}(i,g,h):Q(\kappa(i,))$ such that
$d_{=}(i,g,h,x):h^{\prime}(x)=d_{\kappa}(i,g,h)$ for all $x:\mathbb{R}$, as
desired.

Now suppose $x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ and $y:Q(x)$. By
the last constructor of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$, we have
$x=\kappa(i,\mathsf{const}_{x})$. Thus, transporting $y$ along this equality,
we obtain $y^{\prime}:Q(\kappa(i,\mathsf{const}_{x}))$. Since
$Q(\kappa(i,\mathsf{const}_{x}))$ is discrete, we have
$d_{=^{\prime}}(i,x,y):y^{\prime}=d_{\kappa^{\prime}}(i,\mathsf{const}_{x},\mathsf{const}_{y})$
as desired. ∎

######  Corollary {C0} .

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}R_{i}$ is contractible for any
$i:I$.

###### Proof.

It is inhabited by $\kappa_{R_{i}}(i,\sigma_{R_{i}})$, so it remains to show
$x=\kappa_{R_{i}}(i,\sigma_{R_{i}})$ for all
$x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}R$. Since
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}R_{i}$ is discrete, so is this
equality type; so by $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction,
it suffices to prove $\sigma_{R_{i}}(x)=\kappa_{R_{i}}(i,\sigma_{R_{i}})$ for
all $x:R_{i}$. But this follows from the third constructor of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}R_{i}$. ∎

######  Corollary {R$\flat$} .

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}$ is contractible.∎

######  Corollary {C1} .

For any $A$, the map $\sigma:A\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$
is surjective. In particular, if
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\right\|\mathclose{}$
then $\mathopen{}\left\|A\right\|\mathclose{}$.

###### Proof.

Given $y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$, define
$P(y)\vcentcolon\equiv\mathopen{}\left\|\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}\sigma(x)=y\right\|\mathclose{}$.
By section 8.2, each $P(y)$ is discrete. Thus, by Theorem 9.3, to prove
$\mathchoice{\prod_{y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A}\,}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\mathchoice{{\textstyle\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}{\prod_{(y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)}}}P(y)$
(i.e. that $\sigma$ is surjective), it suffices to prove
$\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(\sigma(x))$;
but this is obvious. ∎

######  Remark .

Recall from section 4 that many positive type formers have a “crisp” variant
of their induction principle, so that we can do case analysis on a $u::A+B$ or
induction on a $u::\mathbb{N}$. This is _not_ the case for
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$, however. If it were, then we
could do $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction on
$u::\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$, so that if $B$ were discrete
then any $M:B$ depending on $u::A$ would factor through
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$. Specializing to
$A\vcentcolon\equiv\mathbb{R}$ and $B\vcentcolon\equiv\mathbf{2}$, any
$M:\mathbf{2}$ depending on $u::\mathbb{R}$ would be constant. However, since
$u$ is crisp, by using the crisp LEM we can define $M:\mathbf{2}$ to be
${0_{\mathbf{2}}}$ if $u<0$ and ${1_{\mathbf{2}}}$ otherwise, which is not at
all constant.

Now we have the reflection property:

######  Theorem {C0} 9.4.

For any $A:\mathsf{Type}$ and any discrete $B:\mathsf{Type}$, composition with
$\sigma:A\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ induces an
equivalence

$(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to B)\simeq(A\to B).$

###### Proof.

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction into the constant
family ${\lambda}x.\,B$ yields a section of $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\circ\sigma)$. Thus, it suffices to show that given
$h,k:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to B$, if
$h\circ\sigma=k\circ\sigma$, then $h=k$. This follows from another
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction with
$P(x)\vcentcolon\equiv(h(x)=k(x))$, which is discrete by section 8.1. ∎

Moreover, analogously to how $\flat\dashv\sharp$ crisply (section 6.3), we
have $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\dashv\flat$ crisply.

######  Theorem {C0} 9.5.

For any $A,B::\mathsf{Type}$, there is a natural equivalence

$\flat(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to B)\simeq\flat(A\to\flat
B).$

###### Proof.

Since $\flat B$ is discrete, by Theorem 9.4 we have a natural equivalence

$(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to\flat B)\simeq(A\to\flat B)$

and this equivalence is preserved by $\flat$. On the other hand, since
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is discrete, by section 6.2 we
have a natural equivalence

$\flat(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to\flat
B)\simeq\flat(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to B).$

Composing these two equivalences yields the conclusion. ∎

Theorem 9.4 makes $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ into a monadic
modality, like $\sharp$, and its construction as a localization makes it an
_accessible_ one [[, see]]rss:modalities. Unlike $\sharp$, however,
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is not left exact. To show this,
we introduce our final weakening of Axiom R$\flat$.

######  Axiom C2.

Axiom C1 holds, and moreover there exist $i_{0}:I$ and $r_{0},r_{1}:R_{i_{0}}$
such that $R_{i_{0}}$ is a set and $r_{0}\neq r_{1}$.

Note that Axiom R$\flat$ implies Axiom C2, since $0\neq 1$ in $\mathbb{R}$.

######  Theorem {C2} 9.6.

There exists a pullback that is not preserved by
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$.

###### Proof.

The pullback of the inclusions $r_{0},r_{1}:\mathbf{1}\to R_{i_{0}}$ is
$\emptyset$. But $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbf{1}$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}R_{i_{0}}$ are both contractible,
whereas $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\emptyset=\emptyset$ since
it is already discrete. ∎

(However, like any monadic modality,
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ does preserve products.)

Viewing $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ as a reflection gives
another, more category-theoretic, way to phrase and prove Theorem 9.2.

######  Theorem {R$\flat$} 9.7.

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$.

###### Proof.

By Theorem 9.4, $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is a left adjoint
to the inclusion of discrete types in all types. Thus, it preserves all
colimits, which is to say it takes colimits in the category of all types to
colimits in the category of discrete types. Thus, since $\mathbb{S}^{1}$ is
the (homotopy) coequalizer of $\mathbb{R}\rightrightarrows\mathbb{R}$, it
follows that $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}$ is the
coequalizer _in the category of discrete types_ of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}\rightrightarrows\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}$,
and hence by section 9 of $\mathbf{1}\rightrightarrows\mathbf{1}$. Now $S^{1}$
is the coequalizer of $\mathbf{1}\rightrightarrows\mathbf{1}$ in the category
of _all_ types; but by Theorem 6.11 it lies in the subcategory of discrete
types and hence is also the coequalizer there. ∎

Similar methods may be used in many other examples. That is, given a “cell
complex” presentation of a classical topological space, if we can convert it
into both a specification for a HIT and a colimit decomposition of that space
that is sufficiently “cofibrant”, then
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ will preserve that colimit and
take the space to the HIT. We do have to be careful to avoid the sort of cell
complex used in classical algebraic topology where discs are glued along their
_boundaries_ , because such gluing in a constructive world tends to produce
inhomogeneous “cusps”. For instance, identifying the two endpoints of the
topological interval $[0,1]=\\{x:\mathbb{R}\mid 0\leq x\leq 1\\}$ would
not141414Although, amusingly, its shape would still be $S^{1}$: it would be
the coequalizer of $1\rightrightarrows[0,1]$, while
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}[0,1]$ is also contractible since
$[0,1]$ is a retract of $\mathbb{R}$. produce a space equivalent to
$\mathbb{S}^{1}$. This is also a known “defect” (if one regards it so) of the
topos model we have in mind; see also the remarks after Theorem 11.6. (It is
“fixed” in the topological topos of [18, §6], but in that model no left
adjoint $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ can exist due to a lack
of local connectedness.)

However, in many cases it should be possible to remedy this by gluing along
_open overlaps_ instead. What makes this work is the fact that although
$\mathbb{R}$ fails to satisfy the trichotomy principle constructively, we do
have $(x<z)\to(x<y)\lor(y<z)$ for all $x,y,z:\mathbb{R}$. Combined with the
following observation, this tells us that gluing along open overlaps produces
no cusps.

######  Lemma .

If $f:A\to C$ and $g:B\to C$ are embeddings, then their union as sub-types of
$C$ is their pushout under their intersection: $A\cup B\simeq A\sqcup^{A\cap
B}B$.

###### Proof.

By definition, $f\cup g:A\cup B\to C$ is the smallest embedding through which
both $f$ and $g$ factor, while $A\cap B$ is the pullback $A\times_{C}B$. If
$h:D\to C$ is an embedding through which both $f$ and $g$ factor, then the
square

$\textstyle{A\cap
B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{D}$

commutes since $h$ is an embedding, so there is an induced map $A\sqcup^{A\cap
B}B\to D$. It remains to note that $A\sqcup^{A\cap B}B\to C$ is an embedding
by [44, Lemma 2.4]. ∎

As an example, we give two other definitions of $\mathbb{S}^{1}$.

######  Theorem 9.8.

The following types are equivalent.

  1. (1)

$\mathbb{S}^{1}$ as defined in section 9, i.e. the coequalizer of the identity
and $+1:\mathbb{R}\to\mathbb{R}$.

  2. (2)

The subset $\\{(x,y)\mid x^{2}+y^{2}=1\\}$ of $\mathbb{R}\times\mathbb{R}$
(the boundary of the topological disc $\mathbb{D}^{2}$).

  3. (3)

The coequalizer of the inclusion of open intervals $(0,\varepsilon)\to(0,1)$
and the translated inclusion
$({\lambda}x.\,1-\varepsilon+x):(0,\varepsilon)\to(0,1)$, for any
$0<\varepsilon<\frac{1}{2}$.

###### Proof.

We can define the functions $\sin$ and $\cos$ on the Dedekind reals
constructively, and prove that $\sin^{2}x+\cos^{2}x=1$. Thus,
${\lambda}x.\,(\cos(2\pi x),\sin(2\pi x))$ defines a map from $\mathbb{R}$ to
$\\{(x,y)\mid x^{2}+y^{2}=1\\}$, which by the periodicity of $\sin$ and $\cos$
descends to $\mathbb{S}^{1}$. It is then straightforward to verify that this
map is both surjective and injective, hence an equivalence since both types
are sets. Thus (1) and (2) are equivalent.

Now let $0<\varepsilon<\frac{1}{2}$. Every real number is either
$<\varepsilon$ or $>-\varepsilon$, so the set $\\{(x,y)\mid x^{2}+y^{2}=1\\}$
in (2) is the union of its subsets $U$ and $V$ consisting of the points where
$y<\varepsilon$ and where $y>-\varepsilon$. Thus, by section 9 it is the
pushout of $U$ and $V$, each of which is isomorphic to an open interval, under
their intersection, which is isomorphic to the disjoint union of two open
intervals, included into $U$ and $V$ at their ends. Since (again by section 9)
the pushout of two open intervals under their intersection is their union, we
can rearrange this pushout to become (3). ∎

Similarly, we can obtain the topological sphere $\mathbb{S}^{2}$ by gluing two
topological discs $\mathbb{D}^{2}$ (isomorphic to $\mathbb{R}^{2}$, hence with
contractible shape) along a strip $\mathbb{S}^{1}\times\mathbb{R}$ (with shape
$S^{1}$). Thus $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{2}$ is
the homotopical suspension of $S^{1}$, i.e. the homotopical sphere $S^{2}$. We
can proceed inductively for higher spheres, and so on. In this way it may be
possible to access homotopy types that would be quite difficult to present as
HITs (due, for example, to their having infinitely many constructors), by
first constructing their topological versions as sets using the Dedekind reals
and then applying $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$.

######  Remark .

The overall conclusions drawn from Axiom C0 in this section and section 8 can
be summarized as “$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is a reflector
into the same subcategory that $\flat$ coreflects into, and it preserves
finite products”. As with the analogous conclusions about $\sharp$ and $\flat$
noted in sections 3 and 6.3, in [47] we assumed this axiomatically, while here
we have deduced it from Axiom C0 and a higher inductive definition of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$. This difference from [47] is
roughly orthogonal to our introduction of $\flat$ and $\sharp$ using crisp
variables; it is not necessitated by anything, but it is a convenient starting
point for expressing the stronger Axiom C1, Axiom C2, and Axiom R$\flat$.
These axioms were not considered in [47]; but in section 10 we will relate the
first two to corresponding categorical properties studied by [25, 20, 26].

######  Remark .

The crisp adjointness $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\dashv\flat$
from Theorem 9.5 finally allows us to justify the choice of the notations
$\flat$ and $\sharp$ (the notation and justification are both due to [46]).
Suppose $G$ is a group, meaning a set (0-type) with a group structure (but,
like all types in spatial type theory, also possessing intrinsic topology). We
can construct a delooping $\mathbf{B}G$ (a.k.a. $K(G,1)$) by the methods of
[27].

Now if $X$ is any space, a _principal $G$-bundle over $X$ with a flat
connection_ assigns to every (topological) path in $X$ an element of $G$
(“transport” along that path), such that concatenating paths corresponds to
multiplication in $G$, and so forth. Since paths in $X$ and elements of $G$
are the 1-morphisms in the fundamental $\infty$-groupoid of $X$ and in
$\mathbf{B}G$, respectively, such a bundle with flat connection can be
described categorically as a map
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}X\to\mathbf{B}G$. But by Theorem
9.5, this is equivalent to a map $X\to\flat\mathbf{B}G$. Thus,
$\flat\mathbf{B}G$ is the _moduli space of flat $G$-connections_, justifying
the notation $\flat$. The notation $\sharp$ is chosen simply as dual to flat;
although one can argue that if $Z$ classifies bundles of some sort then
$\sharp Z$ classifies analogous bundles that are “sharp” in that their fibers
can vary discontinuously. (Unfortunately, as noted in section 7, in [2] and
[3] the symbols $\flat$ and $\sharp$ were used for the propositional
restriction of the same operations, but with reversed meanings.)

##  10\. Axioms of cohesion

The axioms introduced in sections 8 and 9 form a linear string of
implications:

R$\flat$ $\Rightarrow$ C2 $\Rightarrow$ C1 $\Rightarrow$ C0.

Our main goal (the Brouwer fixed point theorem) requires Axiom R$\flat$ (or at
least its consequence section 9). However, the weaker versions are much more
general assumptions, which are not very specific to the “topological”
situation and are satisfied in many other models, so it is interesting that
they suffice for most of the general theory. In this somewhat digressive
section, we investigate some of their further consequences and their topos-
theoretic meaning.

###  10.1. Axiom C0 means stable local connectedness

Combining sections 6.3 and 9.5, we see that Axiom C0 gives us a crisp “adjoint
triple” $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\dashv\flat\dashv\sharp$,
in which $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ preserves finite
products. In topos-theoretic language, the category of types is “local and
locally connected” over the category of discrete (or, equivalently,
codiscrete) types, and in addition the left adjoint preserves binary products.
[20] called this additional condition _stable local connectedness_.

Conversely, if a topos is local and stably locally connected, then by
combining [19, C3.6.3(d)] with [20, Proposition 1.3], it has a site of
definition that is local and locally connected and closed under finite
products. We should therefore be able to show that Axiom C0 holds in its
internal spatial type theory by taking $I$ to be the discrete set of objects
of the site and $R_{i}$ the corresponding representable. The condition that
$A\to(R_{i}\to A)$ be an equivalence then says, in terms of sheaves, that
$A(U)\to A(R_{i}\times U)$ is an isomorphism (or, in the higher-topos case, an
equivalence) for any object $U$ of the site (here we use the fact that the
site has finite products). The special case $U=1$ tells us that $A$ is a
constant (pre)sheaf, and the rest of the conditions follow automatically. (We
could also take $I$ to be a set of objects that generate the site under finite
products, as $\mathbb{R}$ does for our site of cartesian spaces
$\mathbb{R}^{n}$.)

Thus, Axiom C0 is exactly a type-theoretic incarnation of stable local
connectedness (as an additional property added to a local topos). [46] calls a
local and stably locally connected $\infty$-topos _cohesive_ (although for
[25] the word “cohesive” also includes the categorical version of Axiom C1,
below, and an additional axiom called “continuity” that we do not consider
here).

In addition to our motivating example (sheaves on cartesian spaces), several
other similar examples of local and stably locally connected toposes and
$\infty$-toposes can be found in [46]. Here are a few more:

  * •

By [20, Lemma 1.1] and [19, C3.6.3(a) and C3.6.17(a)], the topos
$\mathrm{Sh}(X)$ of sheaves on a space (or locale) is local and stably locally
connected if and only if $X$ has both a focal point and a dense point. For
example, in the Sierpinski space, the closed point is focal and the open point
is dense.

  * •

The local $\infty$-topos of parametrized spectra mentioned in section 7 is
stably locally connected, with
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}=\sharp$. In fact, it is also
punctually locally connected (see below).

  * •

[43] shows that “global equivariant homotopy theory” forms a local and stably
locally connected $\infty$-topos.

###  10.2. Axiom C1 means punctual local connectedness

If we additionally assume Axiom C1, then by section 8.2 the discrete objects
are closed under subobjects. [20] shows that this is equivalent to the
following condition, there called _punctual local connectedness_ ([25] calls
it the _Nullstellensatz_ ; and [46] calls it _pieces have points_).

######  Theorem {C1} 10.1 ([20, Lemma 2.3]).

For any $A::\mathsf{Type}$, the composite $\flat A\to
A\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is surjective.

###### Proof.

As in [53, Theorem 8.8.1], it suffices to show that $\mathopen{}\left\|\flat
A\right\|_{0}\mathclose{}\to\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\right\|_{0}\mathclose{}$
is surjective. Thus, since epimorphisms of sets are surjections [53, Lemma
10.1.4], it suffices to show (invoking the universal property of
$\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|_{0}\mathclose{}$) that
$(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to C)\to(\flat A\to C)$ is
injective for any set $C$. Moreover, since in the proof of Lemma 10.1.4 from
[53] we only need to instantiate this property with one particular set $C$, in
fact it suffices to show that

(10.1) $\flat(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to C)\to\flat(\flat
A\to C)$

is injective for any _crisp_ set $C$. And by section 6.2, we may as well
assume $C$ is also discrete (otherwise we could apply $\flat$ to it).

Now we can essentially copy the proof of Lemma 2.3 from [20]. Firstly, note
that (10.1) is equal to the composite

$\flat(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\to
C)\xrightarrow{\simeq}\flat(A\to C)\xrightarrow{\;\flat\;}\flat(\flat
A\to\flat C)\xrightarrow{\simeq}\flat(\flat A\to C)$

where the first equivalence is Theorem 9.4 and the last is because $C$ is
discrete. Thus, it will suffice to show that the middle map is injective. But
this map is equal to the composite

$\flat(A\to C)\longrightarrow\flat(A\to\sharp
C)\xrightarrow{\simeq}\flat(\flat A\to C)\xrightarrow{\simeq}\flat(\flat
A\to\flat C)$

where the middle equivalence is section 6.3 and the last is because $C$ is
discrete. But $C\to\sharp C$ is injective by section 8.2. ∎

Thus, Axiom C1 implies punctual local connectedness. Conversely, by [20,
Proposition 1.4], any punctually locally connected topos has a site of
definition that is local and locally connected and in which every object has a
global point. Clearly in this case if we take $I$ and $R_{i}$ as described
above, then Axiom C1 will hold; thus it is exactly a type-theoretic
incarnation of punctual local connectedness.

In the different terminology of [26], Theorem 10.1 (along with our previous
results) means that the category of types is “pre-cohesive” over that of
(co)discrete types. In fact, it is “stably pre-cohesive”, because all of our
theorems admit an arbitrary crisp context.

###  10.3. Axiom C2 means contractible codiscreteness

Following [26] further, we investigate the shapes of codiscrete types, for
which purpose we bring back Axiom C2 (page Axiom C2).

######  Theorem {LEM,C2} 10.2.

If $A$ is codiscrete, then $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is a
proposition.

###### Proof.

Let $x,y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$; we must show $x=y$. By
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$-induction, we may assume that
$x=\eta(u)$ and $y=\eta(v)$ for $u,v:A$. Let $i_{0}$ and
$r_{0},r_{1}:R_{i_{0}}$ be as in Axiom C2. Since they are axioms, they are
crisp, and so we have $r_{0}{}^{\flat}:\flat R_{i_{0}}$ and
$r_{1}{}^{\flat}:\flat R_{i_{0}}$. By Theorem 6.1,
$(r_{0}{}^{\flat}=r_{1}{}^{\flat})$ is equivalent to $\flat(r_{0}=r_{1})$,
i.e. to $\flat\emptyset$ and hence to $\emptyset$. In other words, we have
$(r_{0}{}^{\flat}\neq r_{1}{}^{\flat})$.

Now since $\flat R_{i_{0}}$ is a crisp discrete set, by the flat LEM it has
decidable equality. Thus, there is a map $f:\flat R_{i_{0}}\to A$ with
$f(r_{0}^{\flat})=u$ and $f(r_{1}{}^{\flat})=v$. But the inclusion $\flat
R_{i_{0}}\to R_{i_{0}}$ is inverted by $\flat$ and hence also by $\sharp$, so
since $A$ is codiscrete our $f$ extends to a map $g:R_{i_{0}}\to A$ with
$g(r_{0})=u$ and $g(r_{1})=v$. Now the composite
$g\circ\eta:R_{i_{0}}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ has
$g(r_{0})=x$ and $g(r_{1})=y$; but as
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A$ is discrete, $g$ is constant, so
$x=y$. ∎

######  Corollary {LEM,C2} .

For any crisp $B$ we have $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp
B=\mathopen{}\left\|B\right\|\mathclose{}$.

###### Proof.

For any $B$ we have $B\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp B$,
hence a map
$\mathopen{}\left\|B\right\|\mathclose{}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp
B$. But $\flat B\simeq\flat\sharp
B\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp B$ is surjective by
Theorem 10.1, and factors through $\mathopen{}\left\|B\right\|\mathclose{}$.
Hence our map
$\mathopen{}\left\|B\right\|\mathclose{}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp
B$ is also surjective, thus an equivalence. ∎

[26] call the conclusion of Theorem 10.2 _connected codiscreteness_ , and
section 10.3 (proven there as Lemma 7.3) _explicit connected codiscreteness_.
In a homotopical context, however, it seems better to say _contractible_
codiscreteness. As before, since we can work in an arbitrary crisp context, we
automatically have “stable contractible codiscreteness”.

######  Remark .

Unfortunately, the phrase “$X$ is contractible” is used by [26] to mean
“$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(Y\to
X)\right\|_{0}\mathclose{}\simeq\mathbf{1}$ for all $Y$”, which conflicts with
its standard usage in homotopy type theory to mean “$X\simeq\mathbf{1}$”.
(They don’t mention the 0-truncation since they are working with 1-toposes.)
The intution behind their definition is that the sets
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(Y\to
X)\right\|_{0}\mathclose{}$ are the hom-sets of a “strong homotopy category”
of types, analogous to the strong homotopy category of topological spaces
obtained by identifying homotopic maps, so this definition says that $X$ is
terminal in that category. Since $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$
is a functor from this strong homotopy category to the category of discrete
spaces and their 0-truncated hom-sets, and it preserves the terminal object,
if $X$ is contractible in the sense of ibid. then
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}X\simeq\mathbf{1}$, i.e.
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}X$ is contractible in the sense of
homotopy type theory. Thus, if we want to keep “$X$ is contractible” to mean
$X\simeq\mathbf{1}$, we could use a phrase like _strongly spatially
contractible_ for the “contractibility” of [26].

Conversely, if a punctually locally connected topos satisfies Theorem 10.2,
then we have an object, namely $\sharp\mathbf{2}$, for which
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\sharp\mathbf{2}$ is contractible,
but which has two unequal elements ${0_{\mathbf{2}}}^{\sharp}$ and
${1_{\mathbf{2}}}^{\sharp}$. (By Theorem 3.5 we have
$({0_{\mathbf{2}}}^{\sharp}={1_{\mathbf{2}}}^{\sharp})\simeq\sharp({0_{\mathbf{2}}}={1_{\mathbf{2}}})\simeq\sharp\emptyset$,
which is empty by Theorem 8.1.) Thus, we can make Axiom C2 hold by adding
$\sharp\mathbf{2}$ to the collection of $R_{i}$’s; so Axiom C2 is exactly a
type-theoretic incarnation of (punctual local connectedness and) contractible
codiscreteness.

We could now copy the proof of [26, Corollary 6.5] to show that every type $A$
embeds into a type $B$ such that $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}B$
is contractible, there called _sufficient cohesion_. I conjecture that Axiom
R$\flat$ and Axiom AC should together also imply the property called
_continuity_ in [25, 37] — that the canonical map
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(A^{S})\to(\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A)^{S}$
is an equivalence for any crisp set $A$ and any crisp discrete set $S$ — but I
have not managed to prove this yet.

Axiom R$\flat$ does not seem to have been studied yet in a topos-theoretic
context. Of course, it is much more restrictive even than Axiom C2; rather
than defining a general class of toposes for investigation, it singles out an
important characteristic of a single topos (or a small group of toposes) that
we are already interested in.

##  11\. Synthetic topology

As a warm-up for Brouwer’s fixed-point theorem, in this section we develop
some aspects of synthetic topology that stay in the world of sets (0-types).
Here we can already see the power of Axiom R$\flat$, even before any homotopy
theory enters: it forces $\mathbb{R}$ to be _connected_ in several senses. One
such sense is the following.

######  Theorem {R$\flat$} 11.1.

If $P:\mathbb{R}\to\mathsf{Prop}$ is a “detachable subset” (i.e. for all
$x:\mathbb{R}$ we have $P(x)\vee\neg P(x)$), then either $\forall x,\,P(x)$ or
$\forall x,\,\neg P(x)$.

###### Proof.

A detachable $P:\mathbb{R}\to\mathsf{Prop}$ yields a function
$f:\mathbb{R}\to\mathbf{2}$, where $f(x)={1_{\mathbf{2}}}$ if $P(x)$ and
$f(x)={0_{\mathbf{2}}}$ if $\neg P(x)$. But $\mathbf{2}$ is discrete, so by
Axiom R$\flat$ $f$ is constant. ∎

Put differently, if $U$ and $V$ are subsets of $\mathbb{R}$ such that $U\cup
V=\mathbb{R}$ and $U\cap V=\emptyset$, then either $U=\mathbb{R}$ or
$V=\mathbb{R}$. In other words, $\mathbb{R}$ cannot be “broken into two
pieces” nontrivially. [51] calls this property _compact connectedness_.
Combining this with Axiom LEM, and also Axiom T from section 8.3, we can prove
a version of the Intermediate Value Theorem (which is a sort of one-
dimensional analogue of Brouwer’s fixed-point theorem).

######  Theorem {LEM,R$\flat$,T} 11.2 (Discontinuous IVT).

Let $f::\mathbb{R}\to\mathbb{R}$ be a crisp function and $c::\mathbb{R}$ a
crisp real number. If there exist $a,b:\mathbb{R}$ such that $f(a)<c<f(b)$,
then there exists an $x:\mathbb{R}$ such that $f(x)=c$.

###### Proof.

Since the hypothesis of $a$ and $b$ is a crisp proposition, it is discrete.
Thus all our hypotheses may as well be crisp, so we may prove
$\sharp\mathopen{}\left\|\mathchoice{\sum_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}f(x)=c\right\|\mathclose{}$
instead, which by section 8.2 is equivalent to
$\neg\neg{\mathchoice{\sum_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}f(x)=c}$.
Thus, suppose for contradiction
$\neg{\mathchoice{\sum_{x:\mathbb{R}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{R})}}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}{\sum_{(x:\mathbb{R})}}}f(x)=c}$,
i.e. for all $x:\mathbb{R}$ we have $f(x)\neq c$. By Theorem 8.6, for all $x$
we have $f(x)\mathbin{\\#}c$, hence either $f(x)<c$ or $f(x)>c$. Let
$U=\\{x\mid f(x)<c\\}$ and $V=\\{x\mid f(x)>c\\}$; then $U\cup V=\mathbb{R}$
and $U\cap V=\emptyset$. By Theorem 11.1, then, either $U=\mathbb{R}$ or
$V=\mathbb{R}$, which is a contradiction since $a\in U$ and $b\in V$. ∎

The crispness of the hypotheses $f$ and $c$ means that the point $x$ does not
vary continuously with them. It is well-known that a continuous choice of $x$
is impossible, and that this is what prevents the classical version of IVT
from holding constructively [[, see, for instance,]]taylor:lamcra. Our
technology of spatial type theory enables us to state a “discontinuous” IVT,
even in a world where all types are spaces, and our axioms of classicality and
real-cohesion allow us to prove it.

A more common way to constructivize the IVT is to strengthen the hypothesis
(e.g. that $f$ “doesn’t hover” or is “locally non-constant”) or weaken the
conclusion (e.g. we only find an approximate solution). We can also use Axiom
R$\flat$ to prove such a form of IVT, without the need for Axiom LEM or Axiom
T.

First we show that $\mathbb{R}$ is connected in a different sense. The
following proof also introduces an idea that we will use repeatedly. Since
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is a left adjoint, it takes
colimits of types to colimits in the subcategory of discrete types. Moreover,
since _crisp_ discrete types are also coreflective, they are closed under
colimits, so $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ preserves crisp
colimits of types. Similarly, using section 8.2, crisp discrete sets are also
closed under set-colimits (i.e. 0-truncations of homotopy colimits). Thus, if
we write $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}A$ for
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}A\right\|_{0}\mathclose{}$,
then the functor $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}$ reflects
sets into discrete sets, so it preserves crisp set-colimits. We can then use
facts about (set-)colimits of the shapes of types to conclude things about the
types themselves.

######  Theorem {R$\flat$} 11.3.

Let $U,V::\mathbb{R}\to\mathsf{Prop}$ be crisp subsets of $\mathbb{R}$ with
$U\cup V=\mathbb{R}$. If $\mathopen{}\left\|U\right\|\mathclose{}$ and
$\mathopen{}\left\|V\right\|\mathclose{}$, then also $\mathopen{}\left\|U\cap
V\right\|\mathclose{}$.

###### Proof.

By section 9, the assumption ensures that $\mathbb{R}$ is the pushout of $U$
and $V$ over $U\cap V$. Thus, the contractible type
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}$ is the pushout of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}V$ under
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(U\cap V)$, and hence the
contractible $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}\mathbb{R}$ is the
set-pushout of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V$ under
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U\cap V)$. But
$\mathopen{}\left\|U\right\|\mathclose{}$ and
$\mathopen{}\left\|V\right\|\mathclose{}$, hence also
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U\right\|\mathclose{}$
and
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V\right\|\mathclose{}$.

Now if $x:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$ and
$y:\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V$, their images in the
contractible type $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}\mathbb{R}$
must be equal. Using the explicit construction of this set-pushout as the set-
quotient of an equivalence relation of zigzags on
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U+\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V$,
we see that we must in particular have
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U\cap
V)\right\|\mathclose{}$. Finally, since
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(U\cap
V)\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U\cap V)$ is 0-connected
and hence surjective, while $(U\cap
V)\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(U\cap V)$ is surjective by
section 9, we also have $\mathopen{}\left\|U\cap V\right\|\mathclose{}$. ∎

[51] calls the above property _overt connectedness_. Note that we have only
proven it for crisp subsets.

The 0-truncations in the above proof could be omitted, but if we left them
out, then instead of the set-based construction of set-pushouts we would need
to use the van Kampen theorem [53, §8.7]. The former needs only the fact that
the sets form a $\Pi W$-pretopos [53, Theorem 10.1.11], which requires only
function extensionality and propositional extensionality; whereas the latter
in general requires full univalence. Similar remarks apply to the proof of
Theorem 11.5 below, but in Theorem 12.2 we will need to resort to univalence
and van Kampen. (Actually, based on intuition from classical topology, it is
natural to conjecture that $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$ is
automatically a set for any subset $U\subseteq\mathbb{R}$, but I do not know
how to prove this.)

######  Theorem {R$\flat$} 11.4 (Approximate IVT).

Let $f::\mathbb{R}\to\mathbb{R}$ be a crisp function and $c::\mathbb{R}$ a
crisp real number. Then for any $\varepsilon>0$, if there exist
$a,b:\mathbb{R}$ such that $f(a)<c<f(b)$, then there exists an $x:\mathbb{R}$
such that $|f(x)-c|<\varepsilon$.

###### Proof.

It suffices to consider the case when $\varepsilon:\mathbb{Q}^{+}$ is a
positive rational number. Then since $\mathbb{Q}^{+}$ is discrete, we may
assume $\varepsilon$ is also crisp. Therefore the sets
$U\vcentcolon\equiv\\{x:\mathbb{R}\mid f(x)<c+\varepsilon\\}$ and
$V\vcentcolon\equiv\\{x:\mathbb{R}\mid f(x)>c-\varepsilon\\}$ are also crisp.
We have $U\cup V=\mathbb{R}$ by locatedness of Dedekind reals, while by
assumption $a\in U$ and $b\in V$. Thus, Theorem 11.3 supplies the desired $x$.
∎

Note that although Theorem 11.4 eliminates classicality axioms, we still have
only crisp dependence on $f$ and $a$. In fact, the approximate IVT (for
continuous functions) is contructively provable without any additional
assumptions; the most common proofs use countable choice or uniform continuity
of $f$, but [14] has recently given a proof avoiding both of these. So there
is no topological reason for this crispness restriction, but I do not know
whether it can be removed using our current methods.

On the other hand, Theorems 11.2 and 11.4 are statements about _all_ functions
$\mathbb{R}\to\mathbb{R}$. No explicit continuity hypothesis is required,
because in our synthetic world “all functions are continuous”. In fact, with a
little more work we can actually prove explicitly that all functions are
continuous, thereby showing that the axioms of real-cohesion really do nail
down precisely the “topology” of $\mathbb{R}$ to be the intended one.

######  Theorem {R$\flat$,T} 11.5.

Every crisp function $f::\mathbb{R}\to\mathbb{R}$ is $\varepsilon$-$\delta$
continuous at every crisp real number $a::\mathbb{R}$.

###### Proof.

We will need to assume given crisp $b_{1}<a$ and $b_{2}>a$ such that
$f(b_{1})\mathbin{\\#}f(a)$ and $f(b_{2})\mathbin{\\#}f(a)$. This can always
be ensured by modifying $f$ without changing it near $a$. For instance,
$f(a+2)-f(a)$ is either $>\frac{1}{2}$ or $<1$ (and this is crisp since it is
a proposition); if the former we can take $b_{2}=a+2$, while if the latter we
can subtract $\max(0,x-a-1)$ from $f$ before taking $b_{2}=a+2$.

As before, we may assume $\varepsilon::\mathbb{Q}^{+}$ is a crisp positive
rational number. We may also assume $\varepsilon$ is less than both
$|f(b_{1})-f(a)|$ and $|f(b_{2})-f(a)|$. Define

$\displaystyle U$
$\displaystyle=\\{x:\mathbb{R}\mid|f(x)-f(a)|<\varepsilon/2\\}$ $\displaystyle
V$ $\displaystyle=\\{x:\mathbb{R}\mid|f(x)-f(a)|>\varepsilon/4\\}$

Then $U\cup V=\mathbb{R}$, so that $\mathbb{R}$ is the pushout of $U$ and $V$
under $U\cap V$. Let $R_{1}=(-\infty,a]$ and $R_{2}=[a,\infty)$, and
$U_{i}=U\cap R_{i}$, $V_{i}=V\cap R_{i}$ for $i=1,2$, so that $R_{i}=U_{i}\cup
V_{i}$ and $R_{i}$ is the pushout of $U_{i}$ and $V_{i}$ under $U_{i}\cap
V_{i}$. Note that $a\in U_{i}$ and $b_{i}\in V_{i}$ for $i=1,2$.

Consider the fibers of the map
$U\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$; these are the
“spatially connected components” of $U$. Let $w$ be the image of $a$ in
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$, and $W$ the preimage of $w$
in $U$; thus $W$ is the “component of $U$ containing $a$”. Similarly, define
$w_{i}$ and $W_{i}$ for $i=1,2$ to represent the component of $U_{i}$
containing $a$. Then the function
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U_{i}\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$
maps $w_{i}$ to $w$, so that $W_{i}$ is a subset of $W$. Similarly, let
$Z_{i}$ be the component of $V_{i}$ containing $b_{i}$, with image $z_{i}$ in
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V_{i}$, for $i=1,2$.

Now as remarked above, $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}$
prerves crisp set-colimits. Thus, the contractible
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}R$ is the set-pushout of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V$ under
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U\cap V)$, and similarly for
$i=1,2$. In particular, $w_{i}$ and $z_{i}$ are identified in the set-pushout
of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U_{i}$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}V_{i}$ under
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U_{i}\cap V_{i})$, and so
$w_{i}$ must be equal to the image of some element of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}(U_{i}\cap V_{i})$. Since
$X\to\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}X$ is surjective by section
9, $W_{i}$ must contain an element of $U_{i}\cap V_{i}$. Let $y_{i}$ be such
an element. Since $y_{i}\in V_{i}$, we have in particular $f(y_{i})\neq f(a)$,
and hence $y_{i}\neq a$. By Theorem 8.6, $y_{i}\mathbin{\\#}a$; so since
$y_{i}\in R_{i}$ we have $y_{1}<a<y_{2}$. Finally, since $y_{i}\in U_{i}$,
also $y_{i}\in U$.

Let $\delta=\min(y_{2}-a,a-y_{1})$; I claim this is the $\delta$ to our
$\varepsilon$. Thus, suppose $x:\mathbb{R}$ and $|x-a|<\delta$, hence
$x\in(y_{1},y_{2})$. (Note that $x$ is _not_ crisp.) Either
$|f(x)-f(a)|<\varepsilon$ or $|f(x)-f(a)|>\varepsilon/2$; the first is what we
want, so it suffices to show that the second leads to a contradiction.

Thus, suppose $|f(x)-f(a)|>\varepsilon/2$. Then since any $p\in U$ satisfies
$|f(p)-f(a)|<\varepsilon/2$ by definition of $U$, we have $f(p)\neq f(x)$,
hence $p\neq x$. By Theorem 8.6, therefore, $p\mathbin{\\#}x$, and thus either
$p<x$ or $x<p$. In other words,
$\mathchoice{\prod_{p:U}\,}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}(p<x)\vee(x<p)$,
which is equivalent to
$\mathchoice{\prod_{p:U}\,}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}{\mathchoice{{\textstyle\prod_{(p:U)}}}{\prod_{(p:U)}}{\prod_{(p:U)}}{\prod_{(p:U)}}}(p<x)+(x<p)$
since $y$ cannot be both greater and less than $x$. It follows that we can
define a map $q:U\to\mathbf{2}$ by $q(p)={0_{\mathbf{2}}}$ if $p<x$ and
$q(p)={1_{\mathbf{2}}}$ if $x<p$. In particular, since $y_{1}<x$ and
$x<y_{2}$, we have $q(y_{1})={0_{\mathbf{2}}}$ and
$q(y_{2})={1_{\mathbf{2}}}$. But $y_{1}$ and $y_{2}$ are also both in $W$,
i.e. they are identified in $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$.
Since $\mathbf{2}$ is a discrete set, $q:U\to\mathbf{2}$ must factor through
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}U$, and so $q(y_{1})=q(y_{2})$,
a contradiction. So it must be that the other case holds:
$|f(x)-f(a)|<\varepsilon$, as desired. ∎

The statement that all functions $\mathbb{R}\to\mathbb{R}$ are
$\varepsilon$-$\delta$ continuous is sometimes called “Brouwer’s theorem”,
because Brouwer proved it in his “intuitionistic mathematics” using choice
sequences. Here we have proved a version of it using instead our Axiom
R$\flat$ and Axiom T. (Both uses of Axiom T could also be replaced by the
assumption that $f$ is “strongly extensional”, i.e. $f(x)\mathbin{\\#}f(y)$
implies $x\mathbin{\\#}y$.)

Theorem 11.5 provides an almost complete answer to the question of “what is
the topology of $\mathbb{R}$”, with “topology” interpreted in the sense
relevant to our intended model, namely “functions out of $\mathbb{R}$”.

######  Corollary {LEM,R$\flat$,T} .

The canonical function
$\flat(\mathbb{R}\to\mathbb{R})\to(\flat\mathbb{R}\to\flat\mathbb{R})$ is an
injection, and coincides with the inclusion of the $\varepsilon$-$\delta$
continuous functions.

###### Proof.

To show it is an injection, suppose given $f,g::\mathbb{R}\to\mathbb{R}$ such
that $\flat f=\flat g$ as functions $\flat\mathbb{R}\to\flat\mathbb{R}$, or
equivalently $\sharp f=\sharp g$ as functions
$\sharp\mathbb{R}\to\sharp\mathbb{R}$. We must show that for any
$x:\mathbb{R}$ we have $f(x)=g(x)$; but since $\mathbb{R}$ is concrete by
Theorem 8.2, it suffices to show $f(x)^{\sharp}=g(x)^{\sharp}$, which follows
from $\sharp f=\sharp g$.

Now Theorem 11.5 implies that this injection lands inside the
$\varepsilon$-$\delta$ continuous functions. Conversely, suppose
$f:\flat\mathbb{R}\to\flat\mathbb{R}$ is $\varepsilon$-$\delta$ continuous. By
Axiom LEM applied in the universe of discrete types, $f$ is locally uniformly
continuous therein (meaning that it is uniformly continuous on all finite
intervals). Since it suffices to consider intervals with rational endpoints,
while $\mathbb{Q}$ is discrete and discrete types are closed under all logical
operations, $f$ is also locally uniformly continuous in the world of all
types. Therefore, so is the composite
$\mathbb{Q}\to\flat\mathbb{R}\xrightarrow{f}\flat\mathbb{R}\to\mathbb{R}$. But
it can be proved constructively that any locally uniformly continuous function
$\mathbb{Q}\to\mathbb{R}$ extends uniquely to $\mathbb{R}$; see [52, Theorem
5.6.2]. And such an extension restricts to $f$ on $\flat\mathbb{R}$, since the
two agree on $\mathbb{Q}$ and both are continuous. ∎

It would be even better to characterize the “topology” of
$\mathbb{R}\to\mathbb{R}$ itself and so on, or equivalently the functions
$\mathbb{R}^{n}\to\mathbb{R}$ for all $n:\mathbb{N}$, but I don’t know how to
do this without additional axioms. However, the general method of proof of
Theorem 11.5 does have various further applications. Here we mention only one
more: the promised falsity of the analytic LLPO from section 8.3.

######  Theorem {LEM,R$\flat$} 11.6.

It is not the case that for all $x:\mathbb{R}$ we have $x\leq 0\vee x\geq 0$.

###### Proof.

By section 8.2, it suffices to show $\neg\flat(\forall x:\mathbb{R}.(x\leq
0\vee x\geq 0))$. For contradiction, suppose $\flat(\forall
x:\mathbb{R}.(x\leq 0\vee x\geq 0))$, hence $\forall x:\mathbb{R}.(x\leq 0\vee
x\geq 0)$ crisply.

Let $f:\mathbb{R}\to\mathbb{R}$ be such that $f(0)=0$ and
$f(x)=x\sin(\frac{\pi}{x})$ for any $x\mathbin{\\#}0$. Such a function can be
defined constructively without too much trouble, and since it needs no
hypotheses it is crisp. Let $U=\\{x:\mathbb{R}\mid x\geq 0\wedge f(x)\geq
0\\}$ and $V=\\{x:\mathbb{R}\mid x\geq 0\wedge f(x)\leq 0\\}$; then $U$ and
$V$ are also crisp. Our assumption implies that $U\cup V=[0,\infty)$.

Classically, $U$ would be the disjoint union of $\\{0\\}$ with the intervals
$[\frac{1}{n+1},\frac{1}{n}]$ for even $n$, and $V$ the similar union for odd
$n$. (Here and subsequently, we adopt the convention that when $n=0$, the
interval $[\frac{1}{n+1},\frac{1}{n}]$ means $[1,\infty)$.) In fact, Axiom LEM
and Axiom C1 suffice to make this true, by the following argument.

Let $\mathbb{N}_{\infty}$ be the type of functions $\mathbb{N}\to\mathbf{2}$
that take the value ${1_{\mathbf{2}}}$ at most once (this is equivalent to the
type of non-increasing sequences). Now, for any even $n$ and any $x\in U$, we
have $(x<\frac{1}{n-1})\vee(x>\frac{1}{n})$; but since
$x\notin(\frac{1}{n},\frac{1}{n-1})$, it follows that
$(x\leq\frac{1}{n})\vee(x>\frac{1}{n})$. Similarly,
$(x\geq\frac{1}{n+1})\vee(x<\frac{1}{n+1})$, and so the proposition
$x\in[\frac{1}{n+1},\frac{1}{n}]$ is decidable (given that $x\in U$). Thus, we
can define $p:U\to\mathbb{N}_{\infty}$ by

$p(x)_{n}=\begin{cases}{1_{\mathbf{2}}}&\quad
x\in[\frac{1}{2n+1},\frac{1}{2n}]\\\ {0_{\mathbf{2}}}&\quad
x\notin[\frac{1}{2n+1},\frac{1}{2n}].\end{cases}$

If we write $\underline{n}:\mathbb{N}_{\infty}$ for the characteristic
sequence of $n:\mathbb{N}$, and $\infty:\mathbb{N}_{\infty}$ for the
constantly-${0_{\mathbf{2}}}$ sequence, then
$p^{-1}(\underline{n})=[\frac{1}{2n+1},\frac{1}{2n}]$ and
$p^{-1}(\infty)=\\{0\\}$. On the other hand, as for any function,
$U\simeq\mathchoice{\sum_{n:\mathbb{N}_{\infty}}\,}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N}_{\infty})}}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N}_{\infty})}}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}}{\mathchoice{{\textstyle\sum_{(n:\mathbb{N}_{\infty})}}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}{\sum_{(n:\mathbb{N}_{\infty})}}}p^{-1}(n)$.
But by LPO (Theorem 8.5), $\mathbb{N}_{\infty}=\mathbb{N}+\mathbf{1}$, so we
have

$\displaystyle U$
$\displaystyle\simeq\\{0\\}+\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}\textstyle[\frac{1}{2n+1},\frac{1}{2n}]$
and similarly $\displaystyle V$
$\displaystyle\simeq\\{0\\}+\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}\textstyle[\frac{1}{2n+2},\frac{1}{2n+1}].$

Now as remarked above, $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ preserves
coproducts of crisp types (such as the summands of $U$ and $V$). Similarly,
for any $P:\mathbb{N}\to\mathsf{Type}$, by the generalization of [53, Theorem
7.3.9] to monadic modalities we have

$\displaystyle\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\bigl{(}\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}P(n)\bigr{)}$
$\displaystyle\simeq\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\bigl{(}\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}P(n)\bigr{)}$
$\displaystyle\simeq\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}P(n)$
(since this is already discrete, as $\mathbb{N}$ is).

Thus,
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U\simeq\mathbf{1}+\mathchoice{{\textstyle\sum_{(n:\mathbb{N})}}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}{\sum_{(n:\mathbb{N})}}\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}[\frac{1}{2n+1},\frac{1}{2n}]$
and similarly for $V$. But any closed interval $[a,b]$ is a retract of
$\mathbb{R}$, hence $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}[a,b]$ is a
retract of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}$ and thus
contractible. Therefore,
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U\simeq\mathbf{1}+\mathbb{N}$ and
also $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}V\simeq\mathbf{1}+\mathbb{N}$.

Recalling that $[0,\infty)=U\cup V$, it follows that $[0,\infty)$ is the
pushout of $U$ and $V$ under their intersection. However, this intersection is
just $\\{0\\}\cup\\{\frac{1}{n}\mid n:\mathbb{N}\\}$, which is another copy of
$\mathbf{1}+\mathbb{N}$. Since $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$
preserves this pushout, the contractible type
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}[0,\infty)$ is the pushout of
$\mathbf{1}+\mathbb{N}$ and $\mathbf{1}+\mathbb{N}$ under
$\mathbf{1}+\mathbb{N}$. Moreover, the two maps
$\mathbf{1}+\mathbb{N}\rightrightarrows\mathbf{1}+\mathbb{N}$ in this pushout
can be identified with the identity and with “$+1$” acting on $\mathbb{N}$,
respectively (arising from the inclusions of $\frac{1}{n}$ as the left
endpoint of one interval and the right endpoint of another). But the pushout
of these two maps is $\mathbf{2}$ rather than $\mathbf{1}$, since there is
nothing to identify the elements of $\mathbf{1}$ (which correspond to
$\\{0\\}$ in $[0,\infty)$) with anything else. This is a contradiction, so our
assumption $\flat(\forall x:\mathbb{R}.(x\leq 0\vee x\geq 0))$ is false. ∎

Theorem 11.6 explains why classical “closed” cell complexes must be avoided in
real-cohesion, as mentioned in section 9. Namely, the analytic LLPO claims
that the evident map $(-\infty,0]+[0,\infty)\to\mathbb{R}$ is surjective,
which would be exactly what we need in order to be able to glue (say) the
endpoints of a closed interval together seamlessly; its failure means that
such a gluing will not give the desired answer. (Conversely, therefore, if one
wants a “topological topos” in which classical cell complexes _do_ work, one
has to give up on local connectedness, as done by [18].)

##  12\. The Brouwer fixed-point theorem

Finally we are ready to attack Brouwer’s fixed-point theorem. We confine
ourselves to the simplest version, which is about self-maps of the disc:

$\mathbb{D}^{2}\vcentcolon\equiv\\{(x,y):\mathbb{R}\times\mathbb{R}\mid
x^{2}+y^{2}\leq 1\\}.$

Recall from Theorem 9.8 that the boundary of the disc

$\partial\mathbb{D}^{2}\vcentcolon\equiv\\{(x,y):\mathbb{R}\times\mathbb{R}\mid
x^{2}+y^{2}=1\\}$

is an equivalent definition of the topological circle $\mathbb{S}^{1}$; it is
the only one we will use in this section. Recall also from Theorem 9.7 that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}\simeq S^{1}$. We
also have:

######  Lemma {R$\flat$} .

$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{D}^{2}$ is contractible.

###### Proof.

Since $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{R}$ is contractible
and $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ preserves finite products,
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(\mathbb{R}\times\mathbb{R})$ is
also contractible. But $\mathbb{D}^{2}$ is a retract of
$\mathbb{R}\times\mathbb{R}$, by the function

$(x,y)\mapsto\left(\frac{x}{\max(1,\sqrt{x^{2}+y^{2}})},\frac{y}{\max(1,\sqrt{x^{2}+y^{2}})}\right).$

Hence $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{D}^{2}$ is a retract
of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(\mathbb{R}\times\mathbb{R})$,
and thus also contractible. ∎

In particular, therefore, we have:

######  Lemma {UA,R$\flat$} .

$\mathbb{S}^{1}$ is not a retract of $\mathbb{D}^{2}$.

###### Proof.

If it were, $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}$ would
be a retract of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{D}^{2}$ and
hence contractible. But
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$, which is not
contractible since its loop space is $\mathbb{Z}$ [29]. ∎

So much for the homotopy-theoretic part of the proof; we proceed to the
topological part. This might be done in many ways, but we choose to be
explicit and calculational to make it obvious that the argument is
constructive. Here is also where the mysterious Axiom T from section 8.3
reappears.

######  Lemma {LEM,C1,T} .

If there is a map $f:\mathbb{D}^{2}\to\mathbb{D}^{2}$ with no fixed point,
then $\mathbb{S}^{1}$ is a retract of $\mathbb{D}^{2}$.

###### Proof.

Our assumption is that for all $z:\mathbb{D}^{2}$ we have $f(z)\neq z$. Write
$z=(x,y)$ and $f(z)=(u,v)$; then $f(z)\neq z$ means $(x-u)^{2}+(y-v)^{2}\neq
0$, hence by Theorem 8.6 (using Axiom T) $(x-u)^{2}+(y-v)^{2}>0$.

Now the line through $f(z)$ and $z$ can be parametrized as

(12.1) $(tx+(1-t)u,ty+(1-t)v)$

with $t=0$ being $f(z)$ and $t=1$ being $z$. We are interested in the
intersections of this line with $\mathbb{S}^{1}$, which are given by solving a
quadratic equation:

$\displaystyle(tx+(1-t)u)^{2}+(ty+(1-t)v)^{2}$ $\displaystyle=1\quad\iff$
$\displaystyle((x-u)t+u)^{2}+((y-v)t+v)^{2}$ $\displaystyle=1\quad\iff$
$\displaystyle((x-u)^{2}+(y-v)^{2})t^{2}+2((x-u)u+(y-v)v)t+(u^{2}+v^{2}-1)$
$\displaystyle=0$

The standard quadratic formula yields the solutions

$\displaystyle t$ $\displaystyle=\frac{-B\pm\sqrt{D}}{A}$

where

$\displaystyle B$ $\displaystyle=((x-u)u+(y-v)v)$ $\displaystyle D$
$\displaystyle={((x-u)u+(y-v)v)^{2}-((x-u)^{2}+(y-v)^{2})(u^{2}+v^{2}-1)}$
$\displaystyle A$ $\displaystyle={(x-u)^{2}+(y-v)^{2}}.$

To ensure that this yields real solutions constructively, we need to know that
$A\mathbin{\\#}0$ and $D\geq 0$. As we saw above, the former follows from our
assumption that $f(z)\neq z$. For the latter, we can compute

$D=(x-u)^{2}+(y-v)^{2}-(vx-uy)^{2}.$

Now $(x-u)^{2}+(y-v)^{2}$ is the squared length of one diagonal of the
parallelogram spanned by $z$ and $f(z)$ regarded as vectors originating at the
origin, while $(vx-uy)^{2}$ is the squared area of that parallelogram. The
area of a parallelogram is at most half the product of the lengths of its
diagonals; thus $D\geq 0$ as long as the other diagonal of the parallelogram
in question is $\leq 2$. But this other diagonal is the vector sum $z+f(z)$,
which has magnitude $\leq 2$ since both $z$ and $f(z)$ lie in
$\mathbb{D}^{2}$.

Thus we constructively have two real solutions to our quadratic equation for
$t$. We choose the one in which the $\pm$ sign is $+$. Substituting this value
of $t$ into the equation (12.1) of our line, we obtain a formula for a point
in $\mathbb{R}^{2}$ that is a function of $(x,y)$ and $(u,v)$, hence
(recalling that $(u,v)=f(x,y)$) of $z=(x,y):\mathbb{D}^{2}$ only. Moreover, by
construction, this point always lies in $\mathbb{S}^{1}$. Let us denote it
$r(z)$; thus we have $r:\mathbb{D}^{2}\to\mathbb{S}^{1}$.

It remains to show that $r$ is a retraction of the obvious inclusion, i.e.
that if $z=(x,y)$ lies in $\mathbb{S}^{1}$, then $r(z)=z$. For this, it
suffices to show that if $x^{2}+y^{2}=1$, then our chosen value of $t$ becomes
equal to $1$. This is equivalent to asking that $A+B=\sqrt{D}$, and this in
turn is equivalent to asking that $A+B\geq 0$ and that $(A+B)^{2}-D=0$. For
the first, we compute

$\displaystyle A+B$ $\displaystyle=x^{2}+y^{2}-ux-vy$
$\displaystyle=1-(ux+vy)$

But $ux+vy$ is the dot product of $z$ and $f(z)$, which is $\leq 1$ since both
have magnitude $\leq 1$. Finally, for the second we compute

$(A+B)^{2}-D=((x-u)^{2}+(y-v)^{2})(x^{2}+y^{2}-1)$

which clearly vanishes if $x^{2}+y^{2}=1$. ∎

Combining sections 12 and 12, we see that an arbitrary
$f:\mathbb{D}^{2}\to\mathbb{D}^{2}$ cannot fail to have a fixed point. To
deduce a positive statement from this, we invoke Axiom LEM.

######  Theorem {UA,LEM,R$\flat$,T} 12.1 (Sharp Brouwer Fixed-Point Theorem).

For any function $f:\mathbb{D}^{2}\to\mathbb{D}^{2}$, we have
$\sharp\mathopen{}\left\|\mathchoice{\sum_{x:\mathbb{D}^{2}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}f(x)=x\right\|\mathclose{}$.
That is, any self-map of $\mathbb{D}^{2}$ sharply has a fixed point.

###### Proof.

By section 8.2, the claim is equivalent to
$\neg\neg\mathchoice{\sum_{x:\mathbb{D}^{2}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{D}^{2})}}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}{\sum_{(x:\mathbb{D}^{2})}}}f(x)=x$.
But this is what we have just proven. ∎

Equivalently, we can say:

######  Corollary {UA,LEM,R$\flat$,T} (Crisp Brouwer Fixed-Point Theorem).

For any crisp function $f::\mathbb{D}^{2}\to\mathbb{D}^{2}$, there exists
$x:\mathbb{D}^{2}$ such that $f(x)=x$.

###### Proof.

If $f$ is crisp, then so is the fixed point asserted by Theorem 12.1, so we
can strip the $\sharp$ from it. ∎

Topologically, these formulations both say the same thing: every continuous
self-map of $\mathbb{D}^{2}$ has a fixed point, but such a fixed point cannot
be selected continuously. Since the existential in both theorems is
propositionally truncated, even if the $\sharp$ or crispness could be omitted
we would not be asserting the existence of a single continuous _function_
selecting fixed points. However, according to section 7, we would be asserting
that such a function exists _locally_ , i.e. that any given function has a
neighborhood of functions on which fixed points can be selected continuously;
and this is just as impossible. Thus, the versions of the theorem that we have
proven really are the strongest we can expect.

On the other hand, just as we did with the Intermediate Value Theorem in
section 11, we can eliminate Axiom LEM and Axiom T by constructing an
_approximate_ fixed point. Our proof of this will also involve more synthetic
homotopy theory: in addition to $\pi_{1}(S^{1})=\mathbb{Z}$, we will use the
van Kampen theorem for pushouts.

######  Theorem {UA,R$\flat$} 12.2 (Approximate Brouwer Fixed-Point Theorem).

For any crisp function $f::\mathbb{D}^{2}\to\mathbb{D}^{2}$ and
$\varepsilon>0$, there exists an $x:\mathbb{D}^{2}$ such that
$|f(x)-x|<\varepsilon$.

###### Proof.

As before, we may assume that $\varepsilon$ is rational, and hence that it is
crisp. We may also assume $\varepsilon<1$. Define

$g(x)=\begin{cases}f(x)\cdot\frac{\min(|f(x)|,1-\varepsilon/2)}{|f(x)|}&\qquad\text{if}\;|f(x)|>1-\varepsilon\\\
f(x)&\qquad\text{if}\;|f(x)|<1-\varepsilon/2\end{cases}$

The case division is constructively valid by section 9, since one of the two
cases must be true, and if both are true then the two definitions agree. And
since $\varepsilon<1$, if $|f(x)|>1-\varepsilon$ then $|f(x)|>0$, so that
$\frac{\min(|f(x)|,1-\varepsilon/2)}{|f(x)|}$ makes sense.

Now this definition ensures that $|f(x)-g(x)|<\varepsilon/2$, so it suffices
to find an $x:\mathbb{D}^{2}$ such that $|g(x)-x|<\varepsilon/2$. Moreover, we
have $|g(x)-x|>\varepsilon/4$ for all $x:\mathbb{S}^{1}$.

Let $U=\\{x:\mathbb{D}^{2}\mid|g(x)-x|>\varepsilon/4\\}$ and
$V=\\{x:\mathbb{D}^{2}\mid|g(x)-x|<\varepsilon/2\\}$. Then $U\cup
V=\mathbb{D}^{2}$, exhibiting $\mathbb{D}^{2}$ as a crisp pushout of $U$ and
$V$ under their intersection. Therefore the contractible type
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{D}^{2}$ is also the pushout
of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}V$ under
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(U\cap V)$.

However, $\mathbb{S}^{1}$ is contained in $U$ by the construction of $g$, and
the construction of the retraction $r$ in section 12 works for all $x:U$.
Thus, $\mathbb{S}^{1}$ is a retract of $U$, and so
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}$ is a retract of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$. But since
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$, it contains
a nonidentity identification, and hence so does
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$. On the other hand, this
identification must be mapped to the identity in the contractible type
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{D}^{2}$.

Now recall that the van Kampen theorem [53, §8.7] identifies the 0-truncated
equality types of a (homotopy) pushout as a certain set-quotient. Inspecting
this construction we see that the only way two identifications in
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U$ can become equal in
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}U\sqcup^{\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}(U\cap
V)}\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}V$ is if we have
$\mathopen{}\left\|\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}V\right\|\mathclose{}$.
Hence, by section 9, we also have $\mathopen{}\left\|V\right\|\mathclose{}$. ∎

As in Theorem 11.4, there seems no topological reason for the crispness of
$f$, but I do not know how to remove it. Note that although the technique is
similar to that in Theorems 11.3 and 11.5, here we need to use
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ rather than
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}_{0}$, and likewise we need the van
Kampen theorem for pushouts that are not sets (whose proof also involves the
full univalence axiom).

## References

  * [1] Steve Awodey and Michael A. Warren  “Homotopy theoretic models of identity types”  In _Math. Proc. Camb. Phil. Soc._ 146.45, 2009, pp. 45–55  eprint: arXiv:0709.0248
  * [2] Steven Awodey and Lars Birkedal  “Elementary axioms for local maps of toposes”  In _Journal of Pure and Applied Algebra_ 177.3, 2003, pp. 215–230
  * [3] Steven Awodey, Lars Birkedal and Dana S. Scott  “Local Realizability Toposes and a Modal Logic for Computability: (Extended Abstract)”  In _Electronic Notes in Theoretical Computer Science_ 23.1, 1999, pp. 13–26
  * [4] John C. Baez and Alexander E. Hoffnung  “Convenient categories of smooth spaces”  In _Trans. Amer. Math. Soc._ 363.11, 2011, pp. 5789–5825
  * [5] Andrej Bauer and Davorin Lešnik  “Metric spaces in synthetic topology”  In _Ann. Pure Appl. Logic_ 163.2, 2012, pp. 87–100
  * [6] David Carchedi  “On The Homotopy Type of Higher Orbifolds and Haefliger Classifying Spaces” arXiv:1504.02394, 2015
  * [7] Eduardo J. Dubuc and Luis Español  “Quasitopoi over a base category” arXiv:math/0612727, 2006
  * [8] Eduardo J. Dubuc and Jacques Penon  “Objets Compacts Dans les Topos”  In _J. Austral. Math. Soc. (Series A)_ 40, 1986, pp. 203–217
  * [9] E.J. Dubuc  “Concrete quasitopoi”  In _Applications of sheaves (Proceedings, Durham 1977)_ 753, Lecture Notes in Math  Springer-Verlag, 1979, pp. 239–254
  * [10] Daniel Dugger  “Universal Homotopy Theories”  In _Advances in Mathematics_ 164, 2001, pp. 144–176
  * [11] Martín Escardó  “Synthetic topology of data types and classical spaces” http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf In _Electron. Notes Theor. Comput. Sci_ Elsevier, 2004, pp. 2004
  * [12] Martín Escardó  “Topology via higher-order intuitionistic logic” Unfinished draft, available at http://www.cs.bham.ac.uk/~mhe/papers/index.html, 2004
  * [13] M.H. Escardo and T. Streicher  “The intrinsic topology of Martin-Löf universes” http://www.cs.bham.ac.uk/~mhe/papers/universe-indiscrete.pdf. To appear in Annals of Pure and Applied Logic., 2016
  * [14] Matthew Frank  “Interpolating Between Choices for the Approximate Intermediate Value Theorem” arXiv:1701.02227, 2017
  * [15] David Gepner and Joachim Kock  “Univalence in locally cartesian closed $\infty$-categories” arXiv:1208.1749, 2012
  * [16] Thomas G. Goodwillie  “Calculus. III. Taylor series”  In _Geom. Topol._ 7, 2003, pp. 645–711 (electronic)
  * [17] HoTT Project  “The Homotopy Type Theory Coq library”, http://github.com/HoTT/HoTT/, 2015
  * [18] Peter T. Johnstone  “On a topological topos”  In _Proc. London Math. Soc. (3)_ 38.2, 1979, pp. 237–271
  * [19] Peter T. Johnstone  “Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2”, Oxford Logic Guides 43  Oxford Science Publications, 2002
  * [20] Peter T. Johnstone  “Remarks on punctual local connectedness”  In _Theory Appl. Categ._ 25.3, 2011, pp. 51–63
  * [21] Andre Joyal  “Notes on logoi” http://www.math.uchicago.edu/~may/IMA/JOYAL/Joyal.pdf, 2008
  * [22] Chris Kapulkin and Peter LeFanu Lumsdaine  “The Simplicial Model of Univalent Foundations (after Voevodsky)” arXiv:1211.2851, 2012
  * [23] Nicolai Kraus  “Constructions with Non-Recursive Higher Inductive Types”  In _LICS’16_ , 2016
  * [24] F. William Lawvere  “Equality in hyperdoctrines and comprehension schema as an adjoint functor”  In _Applications of Categorical Algebra (Proc. Sympos. Pure Math., Vol. XVII, New York, 1968)_ Providence, R.I.: Amer. Math. Soc., 1970, pp. 1–14
  * [25] F. William Lawvere  “Axiomatic cohesion”  In _Theory and Applications of Categories_ 19.3, 2007, pp. 41–49
  * [26] F. William Lawvere and M. Menni  “Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness”  In _Theory Appl. Categ._ 30.26, 2015, pp. 909–932
  * [27] Dan Licata and Eric Finster  “Eilenberg–MacLane Spaces in Homotopy Type Theory” http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf In _LICS_ , 2014
  * [28] Daniel Licata and Michael Shulman  “Adjoint Logic with a 2-Category of Modes” LFCS ’16. Available at http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf, 2016
  * [29] Daniel R. Licata and Michael Shulman  “Calculating the Fundamental Group of the Circle in Homotopy Type Theory”  In _LICS’13_ , 2013  eprint: arXiv:1301.3443
  * [30] Daniel R. Licata, Michael Shulman and Mitchell Riley  “A Fibrational Framework for Substructural and Modal Logics” Submitted, 2017
  * [31] Zhen Lin  “Answer to MathOverflow question “The real numbers object in Sh(Top)””, http://mathoverflow.net/a/186165/49, 2014
  * [32] Peter LeFanu Lumsdaine and Michael Shulman  “Semantics of higher inductive types” In preparation, 2016
  * [33] Peter Lefanu Lumsdaine and Michael A. Warren  “The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories” arXiv:1411.1736  In _ACM Trans. Comput. Logic_ 16.3 ACM, 2015, pp. 23:1–23:31
  * [34] Jacob Lurie  “Higher topos theory”, Annals of Mathematics Studies 170  Princeton University Press, 2009  eprint: arXiv:math.CT/0608040
  * [35] Jacob Lurie  “Higher Algebra” Available at http://www.math.harvard.edu/~lurie/, 2014
  * [36] Saunders Mac Lane and Ieke Moerdijk  “Sheaves in geometry and logic: a first introduction to topos theory” Corrected reprint of the 1992 edition, Universitext  New York: Springer-Verlag, 1994
  * [37] Matías Menni  “Continuous cohesion over sets”  In _Theory Appl. Categ._ 29.20, 2014, pp. 542–568
  * [38] Erik Palmgren  “A constructive and functorial embedding of locally compact metric spaces into locales”  In _Topology and its Applications_ 154.9, 2007, pp. 1854 –1880
  * [39] Erik Palmgren  “Resolution of the uniform lower bound problem in constructive analysis”, 2007
  * [40] Jacques Penon  “De l’infinitésimal au local (Thèse de Doctorat d’État)” http://www.numdam.org/item?id=DIA_1985__S13__1_0 In _Diagrammes_ S13, 1985, pp. 1–191
  * [41] Frank Pfenning and Rowan Davies  “A Judgmental Reconstruction of Modal Logic”  In _Mathematical Structures in Comp. Sci._ 11.4 New York, NY, USA: Cambridge University Press, 2001, pp. 511–540
  * [42] Jason Reed  “A Judgmental Deconstruction of Modal Logic” http://www.cs.cmu.edu/~jcreed/papers/jdml.pdf, 2009
  * [43] Charles Rezk  “Global homotopy theory and cohesion” http://www.math.uiuc.edu/~rezk/global-cohesion.pdf, 2014
  * [44] Egbert Rijke  “The join construction” arXiv:1701.07538, 2017
  * [45] Egbert Rijke, Michael Shulman and Bas Spitters  “Modalities in homotopy type theory” In preparation, 2016
  * [46] Urs Schreiber  “Differential cohomology in a cohesive $\infty$-topos” http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos; arXiv:1310.7930, 2013
  * [47] Urs Schreiber and Michael Shulman  “Quantum gauge field theory in cohesive homotopy type theory” http://ncatlab.org/schreiber/files/QFTinCohesiveHoTT.pdf In _QPL’12_ , 2012
  * [48] Michael Shulman  “Internalizing the External, or The Joys of Codiscreteness”, https://golem.ph.utexas.edu/category/2011/11/internalizing_the_external_or.html, 2011
  * [49] Michael Shulman  “Reflective Subfibrations, Factorization Systems, and Stable Units”, https://golem.ph.utexas.edu/category/2011/12/reflective_subfibrations_facto.html, 2011
  * [50] Thomas Streicher  “Semantics of type theory: correctness, completeness, and independence results”, Progress in Theoretical Computer Science  Birkhäuser, 1991
  * [51] Paul Taylor  “A lambda calculus for real analysis”  In _Journal of Logic & Analysis_ 2.5, 2010, pp. 1–115
  * [52] A. S. Troelstra and D. Dalen  “Constructivism in mathematics. Vol. I” An introduction 121, Studies in Logic and the Foundations of Mathematics  Amsterdam: North-Holland Publishing Co., 1988, pp. xx+342+XIV
  * [53] Univalent Foundations Program  “Homotopy Type Theory: Univalent Foundations of Mathematics”  http://homotopytypetheory.org/book/, 2013
  * [54] Floris van Doorn  “Constructing the Propositional Truncation using Non-recursive HITs” arXiv:1512.02274  In _Certified Programs and Proofs ’16_ , 2016
  * [55] Oswald Wyler  “Lecture notes on topoi and quasitopoi”  World Scientific, 1991