lemthm lem corthm cor rmkthm rmk defnthm defn egthm eg footnote

# Brouwer’s fixed-point theorem in real-cohesive homotopy type theory

Michael Shulman  University of San Diego, San Diego, CA, 92110, USA

###### Abstract.

We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter
internally with a version of “adjoint logic” in which the discretization and
codiscretization modalities are characterized using a judgmental formalism of
“crisp variables”. This yields type theories that we call “spatial” and
“cohesive”, in which the types can be viewed as having independent topological
and homotopical structure. These type theories can then be used to study
formally the process by which topology gives rise to homotopy theory (the
“fundamental $\infty$-groupoid” or “shape”), disentangling the
“identifications” of Homotopy Type Theory from the “continuous paths” of
topology. In a further refinement called “real-cohesion”, the shape is
determined by continuous maps from the real numbers, as in classical algebraic
topology. This enables us to reproduce formally some of the classical
applications of homotopy theory to topology. As an example, we prove Brouwer’s
fixed-point theorem.

This material is based on research sponsored by The United States Air Force
Research Laboratory under agreement number FA9550-15-1-0053. The U.S.
Government is authorized to reproduce and distribute reprints for Governmental
purposes notwithstanding any copyright notation thereon. The views and
conclusions contained herein are those of the author and should not be
interpreted as necessarily representing the official policies or endorsements,
either expressed or implied, of the United States Air Force Research
Laboratory, the U.S. Government, or Carnegie Mellon University.

##  1\. Introduction

### On spaces, types, and $\infty$-groupoids

Homotopy type theory [53] is an emerging field that connects homotopy theory
and higher category theory with constructive type theory. The homotopy-
theoretic semantics for type theory [1, 22] enables us to view the types in
type theory as homotopical objects. This motivates new rules and axioms for
type theory, such as Voevodsky’s univalence axiom and higher inductive types,
which allow us to do _synthetic homotopy theory_. That is, we can construct
homotopical objects in type theory and prove theorems about them there, such
as calculating homotopy groups of spheres [53, Chapter 8]. The homotopy-
theoretic semantics imply that such formal theorems automatically yield proofs
of corresponding classical results.

However, it is important to understand that at least on the surface, a theorem
in synthetic homotopy theory is a different statement about different objects
than a theorem of the same name in classical homotopy theory. For instance, in
the synthetic theorem that $\pi_{1}(S^{1})=\mathbb{Z}$ [29]:

  * •

$S^{1}$ is a _higher inductive type_ , freely generated by a basepoint and a
loop.

  * •

$\pi_{1}(X)$ is the 0-truncation of the loop space $\Omega(X)$, where the
0-truncation is a higher inductive type that “kills all information above
dimension 0”.

  * •

The loop space $\Omega(X)$ involves “paths” that are an essentially undefined
primitive notion, like “point” and “line” in axiomatic geometry. They are
given meaning by the rules governing them (namely, those of Martin-Löf’s
intensional identity type).

This should be contrasted with the meanings of the same words in the theorem
of classical homotopy theory that is denoted
$\pi_{1}(\mathbb{S}^{1})=\mathbb{Z}$:

  * •

$\mathbb{S}^{1}$ is the topological space
$\\{(x,y)\in\mathbb{R}\times\mathbb{R}\mid x^{2}+y^{2}=1\\}$.

  * •

$\pi_{1}(X)$ is the set of path-components of the loop space $\Omega(X)$.

  * •

The loop space $\Omega(X)$ (and the notion of path-component) involves paths
that are _defined_ as continuous functions $[0,1]\to X$ out of the topological
unit interval.

######  Remark .

In contrast to [53], I will use $\mathbb{S}^{1}$ for the topological circle
$\\{(x,y)\in\mathbb{R}\times\mathbb{R}\mid x^{2}+y^{2}=1\\}$, hoping that the
font will serve as a mnemonic for its relationship to the real numbers
$\mathbb{R}$. This leaves $S^{1}$ for the higher inductive one.

The connection between these worlds that justifies using the same terminology
in both cases can be described as follows.

  1. (1)

In homotopy theory we study objects that may be called _homotopy spaces_ or
_$\infty$ -groupoids_, which have objects, identifications between those
objects, higher identifications between identifications, and so on.

  2. (2)

A topological space $X$ gives rise to an $\infty$-groupoid, traditionally
called its _fundamental $\infty$-groupoid_, whose objects are the points of
$X$, whose identifications are continuous paths in $X$, whose higher
identifications are continuous homotopies in $X$, and so on.

  3. (3)

Type theory admits semantics in $\infty$-groupoids.

  4. (4)

Finally, the fundamental $\infty$-groupoid of the topological circle
$\mathbb{S}^{1}$ is the same $\infty$-groupoid that furnishes semantics for
the higher inductive circle $S^{1}$ in type theory (and similarly for paths,
truncations, and so on).

A classical algebraic topologist would not bring up $\infty$-groupoids, of
course, but just talk about topological spaces directly. However, I find it
clarifying to do so, because it enables us to distinguish ways in which
topological spaces and $\infty$-groupoids behave differently. Specifically, a
topological space can be defined up to homeomorphism, whereas an
$\infty$-groupoid is (at least the way I use the word) only ever defined up to
homotopy equivalence. For instance, as topological spaces, a cylinder is
distinct from a Möbius strip (e.g. one is orientable and one is not); but they
have the same fundamental $\infty$-groupoid (which is, in fact, also the same
as that of $\mathbb{S}^{1}$).

This is important because the homotopy-theoretic semantics of type theory
lands in $\infty$-groupoids, and _not_ in topological spaces.111To be
completely precise, at least with current technology [22] it lands in
simplicial sets, which are a different model for $\infty$-groupoids. Like a
topological space and unlike an $\infty$-groupoid, a simplicial set can be
defined up to isomorphism rather than equivalence; but the notion of
isomorphism for simplicial sets is totally different from the notion of
isomorphism for topological spaces. Moreover, at most a very small amount of
this extra strictness of simplicial sets beyond $\infty$-groupoids is visible
to type theory, and conjecturally none at all. Thus, inside of type theory we
should think of types as $\infty$-groupoids and not as topological spaces. In
particular, although it is common in homotopy type theory to use terminology
borrowed from topology such as “path” and “circle”, these words have a priori
nothing to do with their topological versions _which can also be defined
inside of type theory_. That is, since type theory is rich enough to encode
all of mathematics, we can define in it the real numbers $\mathbb{R}$ and thus
also the topological circle
$\mathbb{S}^{1}=\\{(x,y):\mathbb{R}\times\mathbb{R}\mid x^{2}+y^{2}=1\\}$; but
this type is quite different from the higher inductive circle $S^{1}$. For
instance, the former is a set (0-truncated) with infinitely many distinct
points, while the latter is not a set and has “only one point” (technically,
it is 0-connected).

This frequently causes confusion among newcomers to homotopy type theory, who
struggle to understand the meaning of “path” because it both is, and is not,
like the topological concept after which it is named. For this reason among
others, in this paper I will say _identification_ or _equality_ rather than
“path” when speaking of the synthetic notion (i.e. elements of identity
types).

More importantly, however, this means there is something missing from homotopy
type theory, because there is more to algebraic topology than the study of
$\infty$-groupoids in their own right. The process by which they arise from
topological spaces (the fundamental $\infty$-groupoid) is also important. This
often becomes clear when we are concerned with _applications_ of algebraic
topology to fields such as geometry and physics, which have no _intrinsic_
interest in homotopy theory. As a simple example, consider the standard
homotopy-theoretic proof of Brouwer’s fixed-point theorem:

######  Theorem 1.1.

Let $\mathbb{D}^{2}$ denote the topological disc
$\\{(x,y)\in\mathbb{R}^{2}\mid x^{2}+y^{2}\leq 1\\}$. Then any continuous map
$f:\mathbb{D}^{2}\to\mathbb{D}^{2}$ has a fixed point.

###### Proof.

Suppose $f:\mathbb{D}^{2}\to\mathbb{D}^{2}$ is continuous with no fixed point.
For any point $z\in\mathbb{D}^{2}$, draw the ray from $f(z)$ to $z$ (which is
well-defined since they are distinct) and keep going until you hit the
boundary of $\mathbb{D}^{2}$ (see fig. 1).

$f(z)$$r(z)$$z$ Figure 1. A retraction from a self-map

Call that point of intersection $r(z)$; then $r$ defines a continuous map from
$\mathbb{D}^{2}$ to its boundary, which is the topological circle
$\mathbb{S}^{1}$. Moreover, if $z\in\mathbb{S}^{1}$ to begin with, then there
is no need to keep going once we get from $f(z)$ to $z$, so that $r(z)=z$ in
this case. Thus, $\mathbb{S}^{1}$ would be a retract of $\mathbb{D}^{2}$. It
follows that $\pi_{1}(\mathbb{S}^{1})$ would be a retract of
$\pi_{1}(\mathbb{D}^{2})$; but the latter is trivial while the former is not.
∎

Note how crucial it is that $\mathbb{S}^{1}$ is a topological space, with
points that can be specified exactly and not just up to homotopy. Indeed, the
statement of the theorem makes no reference to homotopy theory.

With present technology, this theorem is completely inaccessible to homotopy
type theory. Of course, the use of proof by contradiction requires the law of
excluded middle, but this can be assumed, as discussed by [53, Chapter 3]. The
real problem is that inside of type theory, we have no way to relate
$\mathbb{S}^{1}$ to $S^{1}$, so that we cannot make the jump into homotopy
theory in the last step. (We could, of course, repeat the _classical_
definition of $\pi_{1}$ as a quotient of a set of continuous paths, and
likewise the classical proof that $\pi_{1}(\mathbb{S}^{1})\cong\mathbb{Z}$,
but then we would have gained nothing from homotopy type theory.)

What we need is some way to define the fundamental $\infty$-groupoid inside of
type theory. The most natural way to interpret this is that given a
topological space $X$ in type theory, we want a _type_ whose _synthetic_ paths
(i.e. elements of its identity type) are the _topological_ paths in $X$ (i.e.
continuous maps $[0,1]\to X$), and so on. It is natural to try to construct
such a thing as a higher inductive type, but there are at least two problems
with this. Firstly, it seems that we would need infinitely many constructors
to handle paths of all dimension, which at present we do not know how to do in
the finitary syntax of type theory. And secondly, if we succeed in doing it,
it is not immediately clear how we would show that this construction takes
$\mathbb{S}^{1}$ to $S^{1}$ without essentially copying again the classical
proof, thereby negating any benefit from synthetic homotopy theory.

### Combining synthetic topology and synthetic homotopy theory

In this paper we will take a different approach: _we make the topology
synthetic, as well as the homotopy theory_. That is, in addition to carrying a
structure of synthetic $\infty$-groupoid, with identifications and higher
identifications, every type also carries a structure of _synthetic topological
space_ , with some sort of “cohesion” attaching nearby elements together. (I
am being deliberately vague here; I don’t want to demand that a synthetic
topology is necessarily specified in terms of open sets the way a classical
topology usually is.)

It is well known that type theory admits topological semantics, in which types
are interpreted by topological spaces or other similar objects. Indeed, this
has been known for much longer than the homotopical interpretations. Moreover,
just as type theory can be enhanced with homotopically motivated axioms such
as univalence, it can be enhanced with topologically motivated axioms such as
Browerian continuity principles or an axiomatic “Sierpinski space”, leading to
_synthetic topology_ [11, 12, 51, 5].

What we will do is to _combine_ these two kinds of interpretation, so that
each type will have _both_ an $\infty$-groupoid structure _and_ a topological
structure. In contrast to the situation in classical algebraic topology, where
the same structure is viewed at different times either as topological or
homotopical, in our world the topological and homotopical structures will be
unrelated. The objects of our motivating model will be _topological
$\infty$-groupoids_, which can be thought of as $\infty$-groupoids together
with topologies on their points, identifications, higher identifications, and
so on, making all of the operations continuous. Here are some examples to get
the reader’s intuition up to speed.

  * •

An ordinary topological space yields a topological $\infty$-groupoid with no
nontrivial identifications, in the same way that a set yields an ordinary
$\infty$-groupoid.

  * •

An ordinary $\infty$-groupoid can be given the discrete topology (in all
dimensions, i.e. on points, identifications, and so on).

  * •

An ordinary $\infty$-groupoid can also be given the _indiscrete_ topology.

  * •

Recall that an ordinary group $G$ can be “delooped” to an $\infty$-groupoid
$K(G,1)$, with one point $b$ and $G$ forming the identifications from $b$ to
itself. If $G$ is a _topological_ group, then we have an analogous $K(G,1)$
that is a _topological_ $\infty$-groupoid, but remembering the topology on $G$
as the space of identifications.222This is different from what a classical
algebraic topologist means by “$BG$” for a topological group $G$. The latter
is the _ordinary_ $\infty$-groupoid with one object whose identifications are
points of $G$, whose 2-identifications are paths in $G$, etc.—i.e. the
delooping of the fundamental $\infty$-groupoid of $G$.

Note that here it starts to matter even more that we distinguish between paths
and equalities: a topological $\infty$-groupoid has both paths _and_
equalities; and it can also have equalities between paths, and paths between
equalities.333Modulo dealing correctly with endpoints, equalities between
paths and paths between equalities are actually the same, but are different
from paths between paths and from equalities between equalities.

At this point we are presented with several problems.

  1. (1)

How should we define precisely what we mean by a “topological
$\infty$-groupoid” (in set-theoretic foundations, to serve as semantics for
type theory)?

  2. (2)

What new rules or axioms can we bring into type theory, motivated by such a
model, that will enable us to relate $\mathbb{S}^{1}$ to $S^{1}$? Continuity
principles and the Sierpinski space are not well-adapted to saying interesting
things about types that are not 0-truncated.

  3. (3)

The classical proof of Brouwer’s fixed-point theorem uses the law of excluded
middle. But unlike homotopical interpretations, topological interpretations
are generally incompatible with excluded middle; how can we resolve this
apparent contradiction?

Fortunately, all three have the same solution. Let us start with (3). The
problem with excluded middle in topological models is that it may not hold
_continuously_ : e.g. a subspace $U\subseteq X$ and its complement $X\setminus
U$ will together contain all the points of $X$, but the map from their
coproduct $U+(X\setminus U)$ to $X$ does not have a _continuous_ section
because the topology on the domain is different. Thus, we cannot expect to
have the full law of excluded middle in a topological model.

However, we can recover a form of excluded middle if we enhance our model and
our type theory with the ability to talk about _discontinuous_ functions in
addition to continuous ones. Then it will be consistent to say something like
“discontinuously, for all $P$ we have $P\vee\neg P$”. There are at least three
ways to add discontinuous functions to a world where everything is continuous:
we could add a new basic notion of “discontinuous map”, we could add an
operation that retopologizes a space discretely (since every function out of a
discrete space is continuous), or we could dually add an operation that
retopologizes a space indiscretely (since every function into an indiscrete
space is continuous). In fact, we will do all three; we will denote the two
retopologization operations by $\flat$ and $\sharp$, respectively.
Categorically, $\flat$ is a coreflection and $\sharp$ is a reflection; in type
theory we call them _modalities_.

Now let us move on to question (2). Here our answer comes from [25] [[, see
also]]lm:ac-cohesive, who has proposed an axiomatization of “categories of
cohesive spaces” based entirely on adjoint functors and their properties. This
is convenient because it is easy to generalize to homotopy theory (regarded as
$(\infty,1)$-category theory), since we have well-behaved notions of adjoint
$\infty$-functors. Lawvere has considered many axioms, but the basic setup is
a string of four adjoint functors:

setscohesive spaces$p_{*}$$p^{!}$$p^{*}$$p_{!}$$\dashv$$\dashv$$\dashv$

in which $p^{*}$ (hence also $p^{!}$) is fully faithful. The idea is that
$p_{*}$ finds the underlying set of a space, $p^{*}$ equips a set with the
discrete topology, and $p^{!}$ equips it with the indiscrete topology. (We
will return to the meaning of $p_{!}$ below.) It follows that $p^{*}p_{*}$ is
a coreflection into the subcategory of discrete spaces while $p^{!}p_{*}$ is a
reflection into the subcategory of indiscrete spaces; thus they coincide with
the modalities $\flat$ and $\sharp$ mentioned above. We can $\infty$-ize this
whole setup by simply replacing categories with $(\infty,1)$-categories,
“sets” with “$\infty$-groupoids”, and adjoint functors with adjoint
$\infty$-functors; this has been studied extensively by [46].

Finally, there is a topos-theoretic side to Lawvere’s work which informs our
answer to question (1). If the category of cohesive spaces is to be a topos,
then the existence of this adjoint string says that it must be a _local and
locally connected_ topos. And we know how to construct local and locally
connected toposes, by taking categories of sheaves on Grothendieck sites with
special properties [[, see e.g]C3.3.10 and C3.6.3(d)]ptj:elephant. Thus, it
stands to reason that by taking $\infty$-sheaves on similar sorts of sites, we
should be able to construct _cohesive $(\infty,1)$-toposes_, and this is in
fact the case, as shown by [46]. The objects of the particular cohesive
$(\infty,1)$-topos we are interested in are known as _topological
$\infty$-groupoids_ or _topological stacks_.

### Real-cohesive homotopy type theory

At this point we may appear to have wandered rather far from our original
motivating problem, namely that we need an “internal” way to construct the
fundamental $\infty$-groupoid. In fact, however, we have snuck up behind it
and are about ready to pounce. The secret lies with Lawvere’s fourth functor
$p_{!}$. In his 1-categorical context, it constructs the set of connected
components of a space, since a map from any space to a discrete one must be
constant on every component. However, when we generalize to the
$(\infty,1)$-categorical context, the analogous $p_{!}$ _is the fundamental
$\infty$-groupoid functor_! Unfortunately, to explain how this comes about
would take too much space here. Some insight may be gained from the proof of
Theorem 9.2 below; for more details see [46, Proposition 4.3.32] or [6, §3].

Just as $p^{*}p_{*}$ and $p^{!}p_{*}$ induce the operations $\flat$ and
$\sharp$ on the type theory of cohesive spaces, the composite $p^{*}p_{!}$
induces a third modality, a reflection into _discrete_ spaces that we call the
_shape_ and denote $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$. (See section
9 for discussion of the name “shape”.) With
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ in our type theory, we can at
least _state_ the desired relation between the circles: we should have
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$. The
existence of $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ alone does not
suffice to _prove_ this, however; what we need is an additional axiom
guaranteeing that $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is in fact
constructed out of continuous paths indexed by intervals in $\mathbb{R}$, as
we expect. To be precise, we assert that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is the “internal localization” at
$\mathbb{R}$, as in [46, Proposition 3.9.4] and [10, Proposition 8.3].

At last, we have a type theory in which we can reproduce the classical proof
of Brouwer’s fixed-point theorem, using synthetic homotopy theory in the
appropriate place. We perform the topological part of the proof in type
theory, using classical axioms such as our modified form of excluded middle
where appropriate. Then at the end we apply
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$, use our calculation that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$, and then
appeal to the synthetic proof of $\pi_{1}(S^{1})=\mathbb{Z}$ to reach a
contradiction.

The type theory formed by the addition of
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ to $\flat$ and $\sharp$ is called
_cohesive homotopy type theory_ , and was already sketched by [47]. Our theory
is a further enhancement of this which I call _real-cohesive homotopy type
theory_ , due to the special role played by the real numbers in defining
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ using continuous paths. As we
will see, the simple axiom of real-cohesion has many striking consequences,
especially combined with our modified classical axioms. In addition to
Brouwer’s fixed-point theorem, it implies versions of the Intermediate Value
Theorem, and characterizes the internal functions $\mathbb{R}\to\mathbb{R}$ as
being precisely those that are $\varepsilon$-$\delta$ continuous in the usual
sense. The present paper is a formal development of just enough real-cohesive
homotopy type theory to enable the proof of the Brouwer fixed-point theorem,
which we give in section 12.

### The problem of comonadic modalities

It should be noted before proceeding that there are in fact many subtly
different ways to represent the modalities
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$, $\flat$, and $\sharp$ in type
theory. The problems in trying to do this arise from the fact that everything
in ordinary type theory happens in an arbitrary context, which means that all
type-theoretic operations must correspond to category-theoretic operations
that apply in each slice category and are stable under pullback. For instance,
the naïve type-theoretic notion of “reflective subuniverse” [53, Definition
7.7.1] corresponds categorically not to a mere reflective subcategory, but to
a “reflective subfibration” of the self-indexing.

For $\sharp$ this is not a problem, since it is a left exact reflector (being
a composite of two right adjoints), and any left-exact-reflective subcategory
admits a canonical extension to a reflective subfibration. For
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$, which is a reflector but not
left exact, it is more of an issue; however, as long as
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ can be defined by an internal
localization — which categorically means that our topos is not just locally
connected but _stably_ locally connected [[, see]]johnstone:punctual-lc — it
can be extended to a reflective subfibration. (The category-theoretic side of
such modalities will be studied elsewhere; presently we are concerned with
their type-theoretic manifestation, with the category theory providing only
motivation. Internally in type theory, modalities of this sort were sketched
briefly by [53, §7.7] and will be studied in detail by [45].)

The real problem arises with the modality $\flat$, which is a _coreflector_ ,
and _cannot_ be extended to a “coreflective subfibration”. In fact, one can
prove a “no-go theorem” (Theorem 4.1) that the only coreflective subfibrations
are those of the form $\Box_{U}(A)=A\times U$ for a subterminal object $U$,
and $\flat$ is certainly not of this form. Thus, we must find some way to
represent $\flat$ that prevents it from being applied in arbitrary contexts.

[47] did this by using $\sharp\mathsf{Type}$. We cannot have $\flat$ as an
operation $\mathsf{Type}\to\mathsf{Type}$ on the universe itself, but we can
have it as an operation $\sharp\mathsf{Type}\to\sharp\mathsf{Type}$, i.e. a
“discontinuous” self-map of the universe. This choice had the advantage of
being formalizable in existing proof assistants, but the disadvantage that it
required developing large amounts of theory of $\sharp\mathsf{Type}$ as “the
external category of types” [[, which was mostly omitted by]]ss:qgftchtt. Even
worse, there is no way to “escape” from $\sharp\mathsf{Type}$, but it should
be the case that if we have a particular type defined in the empty context,
such as $\mathbb{N}$, we can define $\flat\mathbb{N}$ as an actual type,
rather than just an element of $\sharp\mathsf{Type}$. Finally, in [47] all the
modalities were obtained by asserting axioms, but for good formal behavior of
a type theory it is preferable to use rules rather than axioms, since axioms
interfere with canonicity.

For these reasons, in this paper we take a different approach, based on the
“judgmental reconstruction” of modal logic by [41]. We modify our base type
theory by introducing a new sort of hypothesis $x::A$, which we call _crisp_ ,
intended to mark whether dependence on a variable is continuous or
discontinuous. Based on this, we can then introduce $\flat$ and $\sharp$ using
the usual sort of rules for type constructors: formation, introduction,
elimination, and computation.

Our rules for $\flat$ are almost exactly those of [41] for $\Box$. If $B$ is a
type depending only on crisp hypotheses we can form $\flat B$, and similarly
if a term $M:B$ depends only on crisp hypotheses we can form $M^{\flat}:\flat
B$, while an element of $\flat B$ can always be assumed to be of this form.
However, although our $\sharp$ on its own behaves like the $\bigcirc$ of [41],
its rules are quite different (in particular, we have no judgment
“$M\sim:\hskip 3.0ptA$” like in [41]) and make it automatically right adjoint
to $\flat$. The resulting type theory, which requires no axioms yet, we call
_spatial type theory_ ; we expect that it corresponds semantically to _local
toposes_ , which have $p^{*}\dashv p_{*}\dashv p^{!}$ but no $p_{!}$. It
includes as a fragment the “modal logic of local toposes” of [2] and [3].

In particular, the rules of $\flat$ stipulate that it can only be applied in a
context of purely discontinuous dependence, circumventing the no-go theorem.
In addition to resolving all the above problems with $\sharp\mathsf{Type}$,
this has the additional advantage that we can apply $\flat$ not only in a
totally empty context, but in a context of other _discrete_ spaces.
Categorically speaking, this means we treat the topos of cohesive spaces as
_indexed over_ the base topos via $p^{*}$, which is exactly the right thing to
do for any geometric morphism [see][B3.1.2]ptj:elephant[and][Theorem
3.4.20]schreiber:dcct.

######  Remark .

One might argue that it would be better to include a separate kind of type
representing objects in the base category, and type constructors representing
the functors $p^{*}$, $p_{*}$, etc. rather than the monads and comonads they
induce. This would be in line with the “judgmental deconstruction” of [42]
that decomposes $\Box$ and $\bigcirc$ into pairs of adjoint functors. It could
be that this is indeed better; in fact, the current rules for $\flat$ and
$\sharp$ were deduced from a generalization of [42] developed by [28].

However, for now I have chosen to go with a simpler type theory in which there
is only one kind of type. Learning to keep track of the two kinds of variables
in spatial type theory is hard enough. Moreover, the theory of [28] is general
enough to include this case as well: unlike $\Box$ and $\bigcirc$, our
modalities $\flat$ and $\sharp$ are type-theoretically sensible in their own
right without needing to be deconstructed. There is also a philosophical
attractiveness to the position that _all_ types have topological structure,
even if that structure happens to be discrete or codiscrete.

######  Remark .

It is natural to wonder why we introduce crisp hypotheses $x::A$, when
semantically they are essentially just ordinary hypotheses $u:\flat A$. Why
not simply restrict the formation of $\flat B$ and $M^{\flat}$ to contexts
containing only variables of the form $u:\flat A$?

This might be simpler in some respects, but it would be bizarre in others. The
official type-theoretic reason is that, as noted by [41, §4.2], “substitution
would no longer be an admissible rule”. In less fancy language, that means
that we would not be able to determine the validity of an expression by plain
syntactic analysis, or else we would have to introduce a complicated calculus
of explicit substitutions.

For instance, if $M^{\flat}$ could be formed in a context of variables
$u:\flat A$, then we could define a function
$f\vcentcolon\equiv({\lambda}x.\,x^{\flat}):\flat B\to\flat\flat B$, since a
variable $x:\flat B$ has the correct form to allow us to write
$x^{\flat}:\flat\flat B$. Now suppose we also had a function $g:A\to\flat B$.
Then the composite $f\circ g$ would reduce to ${\lambda}a.\,g(a)^{\flat}$; but
$g(a)$ does _not_ have the correct form to allow us to apply $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\flat}$ to it! So if we allowed $g(a)^{\flat}$
as a valid expression, we would be unable to determine its validity by
inspection, but would have to “guess” that it was obtained by substituting
$g(a)$ into the valid $x^{\flat}$. Otherwise, we would have to write instead
$x^{\flat}[g(a)/x]$, where the substitution $[g(a)/x]$ is not, as usual, a
_defined operation_ on expressions, but a basic part of the grammar of
expressions (an “explicit substitution”).

The formalism of crisp variables avoids both horns of this dilemma. In this
setup, $f:\flat B\to\flat\flat B$ must be defined as
${\lambda}x.\,\mathsf{let}\;u^{\flat}\coloneqq
x\;\mathsf{in}\;u^{\flat}{}^{\flat}$ (see section 4), and when we compose it
with $g$ we get ${\lambda}a.\,\mathsf{let}\;u^{\flat}\coloneqq
g(a)\;\mathsf{in}\;u^{\flat}{}^{\flat}$. Now we are no longer applying
$(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\flat}$ directly to $g(a)$,
but to a crisp variable that it has been destructed into; thus the _syntactic_
invariant that indicates a correct application of $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\flat}$ is preserved.

With all that said, once the basic lemmas about $\flat$ are proven using crisp
variables, in most cases we will be able to blur the distinction between crisp
elements of $A$ and elements of $\flat A$, at least when working informally.

Now we have to choose how to represent
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$. One possibility would be to add
further new judgment forms so that it could be characterized similarly to
$\flat$ and $\sharp$. The general theory of [28] immediately suggests how to
do this, but the judgmental structure of the resulting theory would be
substantially more complicated. Moreover, semantically it seems likely to
correspond to indexing the base topos over the cohesive topos by means of
$p_{!}$, which is at least an odd thing to do. We would also need to take
special care that the rules didn’t force
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ to be left exact (whereas our
rules for $\flat$ and $\sharp$ do automatically make both of them left exact),
since in our desired models it is not.

For these reasons, I have chosen to introduce
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ axiomatically. However, rather
than asserting the modality itself as an axiom, we assert a set of
“generators” for it, enabling the modality itself to be constructed by a
higher inductive localization. This has some technical advantages, and it also
leads naturally into the stronger axiom of real-cohesion, where we can simply
assert that $\mathbb{R}$ alone is a sufficient generator for
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$. It seems highly unlikely that
the special position of $\mathbb{R}$ in real-cohesion could be obtained by
rules rather than an axiom, so we lose nothing in that regard by making
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ axiomatic already.

It should be clear from this discussion, however, that there is nothing sacred
about the particular choices made in this paper. Most of the length of this
paper is devoted to _proving_ from our rules and axioms that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$, $\flat$, and $\sharp$ satisfy
the correct relationships (which [47] just _assumed_ to be true).
Specifically, we need to know that $\sharp$ and
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ are reflectors (Theorems 3.4 and
9.4) and $\flat$ is a coreflector (section 6.2), that $\sharp$ is left exact
(Theorem 3.6), that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\dashv\flat\dashv\sharp$ (sections
6.3 and 9.5), that $\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ preserves
finite products and reflects into the same subcategory that $\flat$ coreflects
into, that the images of $\flat$ and $\sharp$ are equivalent (section 6.3) by
an equivalence that identifies $\flat$ with $\sharp$ (Theorem 6.12), and that
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ is generated by $\mathbb{R}$
(Axiom R$\flat$). Once these facts are established somehow, the contentful
theorems (such as
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}\mathbb{S}^{1}=S^{1}$ and the
Brouwer fixed-point theorem) are essentially independent of the underlying
type-theoretic machinery. I had to fix some particular choice of that
machinery in order to write the paper, but this choice made may very well turn
out not to be the optimal one.

Moreover, the behavior of “spatial type theory” as a type theory has not yet
been studied. It looks somewhat reasonable, in that $\sharp$ and $\flat$ have
introduction and elimination rules of roughly the usual sort. But for it to be
really respectable as a type theory one should prove various standard theorems
about it, such as normalization and canonicity, and this has not been done.
([28] did this for a more general class of “adjoint logic” type theories, but
only under the fairly severe simplifying assumptions of no dependent types and
only one variable in the context. [30] allows multi-variable contexts, but
still no dependent types, and has a rather fiddlier adequacy theorem.)
Eventually, one might hope to implement such a type theory in a proof
assistant.

### Outline of the paper

This paper has three parts; but rather than coming in sequential order, one of
the parts is interleaved through the other two. The first part, consisting of
sections 2 to 7, develops spatial type theory. It begins with the judgmental
structure (section 2), then moves on to $\sharp$ (section 3) and then $\flat$
(sections 4 to 6). In section 7 we sketch briefly the intended categorical
models of this theory, and use them to motivate the axioms to be introduced in
the third part.

The second, interleaved, part, consisting of sections 2.1, 3.1, 3.2, 6.4 and
8.3, studies classical axioms that can be added to spatial type theory without
destroying its topological content, such as the modified law of excluded
middle mentioned above. It is interleaved because the formulation and proof of
various classical principles requires more and more of the base type theory,
but at the same time provides useful motivation for the same. In section 2.1
we state the restricted law of excluded middle, and decide that in order to
state a similarly restricted axiom of choice we need $\sharp$. After
introducing $\sharp$, in section 3.1 we revisit excluded middle in some other
guises made possible by $\sharp$, and in section 3.2 we formulate the axiom of
choice, but note that there ought to be simpler versions available if we had
$\flat$. Thus, after introducing $\flat$, in section 6.4 we discuss these
versions and their applications. Finally, after stating the axioms of real-
cohesion, in section 8.3 we show that these axioms strengthen our classicality
axioms, and state one further such axiom.

The third part, consisting of sections 8, 9, 10, 11 and 12, adds additional
axioms to spatial type theory that make it cohesive and real-cohesive, and
applies them to prove the Brouwer fixed-point theorem. In section 8 we state
the cohesion and real-cohesion axioms in generator form and deduce some
consequences, and in section 9 we construct
$\mathord{\raisebox{0.5pt}{\text{\rm\esh}}}$ as a higher inductive type.
Section 10 relates our axioms back to the motivating topos-theoretic notions.
In section 11 we note some implications of real-cohesion for synthetic
topology that don’t require any higher homotopy, including some versions of
the Intermediate Value Theorem and a version of “Brouwer’s theorem” that all
functions $\mathbb{R}\to\mathbb{R}$ are continuous. Finally, in section 12 we
bring everything together to prove the Brouwer fixed-point theorem by
mimicking the classical proof, invoking synthetic homotopy theory and our
modified classicality axioms in the appropriate places. We also similarly
prove a constructive variant asserting only the existence of _approximate_
fixed points, but not requiring any classicality axioms.

### On axioms and notation

Because we are developing a hierarchy of type theories (spatial $<$ cohesive
$<$ real-cohesive), and using classical axioms in some places, we keep careful
track of which axioms are necessary for which theorems. In addition to our
classicality axioms (LEM, AC, and T) and (real-)cohesion axioms (C0, C1, C2,
and R$\flat$), we track uses of the full univalence axiom (UA). We do need UA
for our proof of the Brouwer fixed-point theorem, but most of the theory does
not require it, and hence should be valid in a 1-topos model in addition to an
$(\infty,1)$-topos model. We will, however, use without comment the axioms of
function extensionality, propositional resizing, and univalence restricted to
propositions (“propositional extensionality”), since these are all valid in a
1-topos.

We will generally adhere to the notation of [53]. For example, we write $x=y$
for the identity type, $M\equiv N$ for a judgmental equality, and
$a\vcentcolon\equiv P$ if $a$ is currently being defined to equal $P$.
However, as remarked above, we will call elements of $x=y$ “identifications”
or “equalities” rather than “paths”, and we write $S^{1}$ for the higher
inductive circle to reserve $\mathbb{S}^{1}$ for the topological one. We will
also call $(-1)$-truncated types simply _propositions_ rather than “mere
propositions”, as is common outside of [53]. Similarly, we pronounce the
$(-1)$-truncated existential (as in [53], $\exists_{x:A}P(x)$ means
$\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)}}}P(x)\right\|\mathclose{}$)
simply as “there exists”, rather than the “there merely exists” of [53]. This
also requires avoiding other terminology such as “propositional equality” and
“propositional uniqueness rule” since the notions in question are not
$(-1)$-truncated; for this purpose we introduce the new adjective _typal_ (to
contrast with _judgmental_).

### Vistas

The Brouwer fixed-point theorem is not itself of central importance; it serves
mainly as a convenient test case. The real point is the development of
spatial, cohesive, and real-cohesive type theory. Some possibilities for
further applications include the following.

  * •

Real-cohesion should also imply other applications of homotopy theory to
topology, such as the Lefschetz fixed-point theorem and the hairy ball
theorem.

  * •

In cohesive homotopy type theory, a topological group appears as an ordinary
internal (0-truncated) group, which can be delooped as in [27]. These
deloopings are classifying spaces for topological principal bundles up to
isomorphism (rather than the up-to-homotopy-equivalence classifying spaces of
classical algebraic topology); the classifying maps live in “continuous
cohomology theories”.

  * •

Matrix groups and their deloopings are important in classical algebraic
topology, but as $\infty$-groupoids they are hard to define in ordinary
homotopy type theory. In real-cohesive homotopy type theory, we can obtain
them as shapes of ordinary set-level definitions. The same is true for other
classical objects such as higher Hopf fibrations.

  * •

There are other local toposes than cohesive and real-cohesive ones, such as
Sierpinski cones, the topological topos of [18], and the relative
realizability topos of [3]. Each of these should motivate different axioms.

  * •

Similarly, there are cohesive toposes other than real-cohesive ones. Some,
which play an important role in [46], encode _smoothness_ rather than
continuity; these satisfy a version of Axiom R$\flat$ with $\mathbb{R}$
replaced by a type of “smooth reals”. Other interesting examples include the
_global homotopy theory_ of [43], the $\infty$-topos of simplicial
$\infty$-groupoids, and the tangent $\infty$-toposes of [35].

### On theft and honest toil

One of the advantages of type theory is that it enables us to “add structure
by failing to rule it out”. For instance, because type theory admits
topological models, if we define (say) a _group_ in type theory, as long as we
didn’t use any principles that are invalid topologically, we have
automatically defined a _topological group_ as well. Homotopy type theory
applies the same effect to $\infty$-groupoids: as long as we don’t use any
principles like UIP, everything we do in type theory is automatically
homotopical.444We do have to be careful that this happens in the right way.
For instance, the naïve definition of “group” doesn’t give the correct
$\infty$-groupoidal notion, but there is a different one that does. This is
especially valuable because working directly with $\infty$-groupoids can be
combinatorially complicated and require a lot of background in algebraic
topology and category theory.

Spatial and cohesive type theory extend this advantage even further: not only
does type theory apply automatically to spaces and to $\infty$-groupoids, it
also applies to _spatial $\infty$-groupoids_, which have both structures at
once. Moreover, even if we didn’t have any categorical models in mind to
specify what a “spatial $\infty$-groupoid” might mean, we could still
undertake to study them in type theory by simply _combining_ the axioms and
principles that pertain to spatial models (such as continuity principles
and/or modalities) and homotopical models (such as univalence and HITs).
Except for sections 7 and 10, the present paper can be read from such a
perspective.

It is true that mathematical honesty may demand that such models eventually be
produced, to ensure relative consistency and allow our “synthetic” results to
be translated into classical theorems. However, once _someone_ has undertaken
that toil [[, in our case, the toil includes]as well as future work that
remains to be done]lurie:higher-
topoi,schreiber:dcct,gk:univlcc,shulman:intext-codisc,shulman:rsfib-
factsys,klv:ssetmodel,lw:localuniv,ls:hits, we can continue to work in the
type theory without needing to think about or understand the model. This
principle should also apply to other possible enhancements of spatial type
theory.

### Acknowledgments

This paper owes a lot to many people. My understanding of cohesive
$(\infty,1)$-toposes developed over the course of many discussions with Urs
Schreiber, who also helped greatly with understanding the categorical
semantics of modalities (this joint work is represented in [47], which this
paper draws heavily on). Other participants at the $n$Forum and $n$-Category
Café have also been very helpful, particularly Zhen Lin. Andrej Bauer and
Martín Escardó patiently explained to me the relationship between different
classicality axioms and some existing theories of synthetic topology, and Bas
Spitters contributed the proof of section 8.3. Urs Schreiber, Bas Spitters,
Egbert Rijke, and Martín Escardó also gave useful feedback on drafts. Finally,
Dan Licata explained [41] to me, did most of the work on our joint paper
[*]ls:1var-adjoint-logic generalizing [42] that led to the spatial type theory
presented here, and has been generally indispensable in teaching me to sound
at least vaguely like a type theorist.

##  2\. Judgments of spatial type theory

As explained in the introduction, we take the point of view that _all types
have spatial structure, independently of their $\infty$-groupoid structure_,
and concomitantly _all ordinary type-theoretic constructions are continuous_.
Now, it does happen sometimes in mathematics that we want to talk about things
that are _not_ continuous. Our main target in this paper — the Brouwer fixed-
point theorem — is a prime example: fixed points of functions cannot be
selected _continuously_ with respect to the space of functions. For this
reason, we augment our type theory with technology that enables us to talk
about possibly-discontinuous constructions as well as continuous ones.

Recall that the basic judgment of type theory is $a:A$ for some specific type
$A$, expressing that $a$ is a point of the type $A$. This judgment is used in
two ways: for some specific _expression_ $a$ we can judge it to be true, or
for some _variable_ $x$ we can _suppose_ it to be true. For instance, in a
statement like “whenever $x:A$ then $f(x):B$” we see both uses: $x$ is a
variable hypothesized to be of type $A$, and under this hypothesis, $f(x)$ is
an expression judged to have type $B$. It is a distinguishing feature of type
theory that whenever $x:A$ is a _hypothesis_ , $x$ must be a _variable_ ; it
makes no sense to say “suppose that $f(x):B$” (in contrast to the behavior of
the membership predicate $\in$ of set theory).

In a world where types are spaces, all ordinary type-theoretic constructions
are continuous; thus a statement like “whenever $x:A$ then $f(x):B$” means
that $f(x)$ depends _continuously_ on $x$. We now augment our type theory with
new features to express the possibility that this dependence may _not_ be
continuous. In general, we might imagine doing this either by modifying the
hypothesis $x:A$ or the conclusion $f(x):B$. Since continuous functions are
also discontinuous,555We will use “discontinuous” to mean “not necessarily
continuous”, by analogy with other phrases such as “noncommutative ring”. the
variance of implication means that if we modify $x:A$, we would have to
replace it by a _stronger_ judgment (i.e. one that implies $x:A$), whereas if
we modify the conclusion $f(x):B$, we would have to replace it by a _weaker_
judgment (i.e. one that is implied by $f(x):B$).

We take the first route. Following [41], we denote the stronger judgment by

$x::A$

When we hypothesize $x::A$, this means that we allow ourselves to perform
constructions and proofs using $x$ that may not respect the topology of $A$
(but they still must respect the topology of any other ordinary hypotheses
$y:C$). In other words, _having_ $x::A$ is _more_ powerful than having $x:A$;
and thus, oppositely, _proving_ something with a hypothesis of $x::A$ says
_less_ than proving it with a hypothesis $x:A$.

We refer to $x::A$ as a crisp hypothesis, and $x$ as a crisp variable.666The
word “crisp” is chosen as having a connotation somewhat similar to “discrete”
(i.e. not flabby or deformable) and being relatively free of other
mathematical meanings. Its one existing mathematical usage that I am aware of
is in fuzzy-set theory, where it refers to ordinary (non-fuzzy) sets; this is
actually closely related to our usage, since many categories of fuzzy sets are
quasitoposes [55, Chapter 8] in which the crisp sets are what we would call
the codiscrete objects, so that they also “forget about the cohesion”. ([41],
whose focus is on logic, use the word _valid_.) A crisp variable can always be
used as an ordinary one, but also (potentially) in other ways. If we don’t
want to give a name to the variable, we may say that $A$ holds crisply. If
necessary, for contrast we will refer to an ordinary hypothesis or variable
$x:A$ as cohesive.

For consistency, we require that all variables appearing in the type of a
crisp hypothesis are themselves crisp. Moreover, a crisp variable can only be
substituted by expressions involving only other crisp variables. If $M:A$ is
an expression other than a variable, we will say that $M$ is crisp, and
sometimes write $M::A$, if the only _variables_ it contains are crisp. Thus,
as for [41] the notion of _crisp conclusion_ is not a basic part of the
theory, but rather is defined to mean an ordinary conclusion that depends only
upon crisp hypotheses.

All the ordinary rules of type theory ($\prod$-types, $\sum$-types, $=$-types,
$W$-types, HITs) are imported into our theory _only in the world of cohesive
variables_. Applications of these rules can involve dependence on “unaffected”
crisp variables; but the variables that are manipulated in the rules, as well
as their conclusions, are always cohesive. (We will eventually prove, however,
that in some cases this can be worked around.)

At a formal level, what we are doing is separating our _context_ into two
pieces: first a crisp one, then a cohesive one, maintaining the restriction
that the type of each variable can only contain variables occurring to its
left. We would therefore write our judgments as
$\Delta\mid\Gamma\vdash\mathcal{J}$. The previous paragraph means that the
ordinary rules of type theory leave the crisp context $\Delta$ untouched; for
example, the rules for $\prod$-types are shown in fig. 2.

Δ∣Γ⊢A:Type
Δ∣Γ,x:A⊢B:Type Δ∣Γ⊢∏_(x:A)B:Type Δ∣Γ,x:A⊢b:B Δ∣Γ⊢λx. b:∏_(x:A)B Δ∣Γ⊢f:∏_(x:A)B
Δ∣Γ⊢a:A Δ∣Γ⊢f(a):B[a/x] Δ∣Γ,x:A⊢b:B
Δ∣Γ⊢a:A Δ∣Γ⊢(λx. b)(a) ≡b[a/x] Δ∣Γ⊢f:∏_(x:A)B Δ∣Γ⊢f≡(λx. f(x))

Figure 2. $\prod$-types in spatial type theory

In what follows, we will attempt to describe all the rules of spatial type
theory in words, but we will also include some formal syntax of this sort for
precision. After introducing the rules, however, we will reason almost
entirely informally in the style of [53].

We will have occasion to use various _axioms_ (including axioms from [53] such
as function extensionality and univalence), so it is worth noting how these
interact with our split contexts. Ordinarily in type theory an _axiom_ means
an assumed element of some type. There are two ways of thinking about such
axioms in type theory: they can be premise-free rules added to the theory, or
they can be simply additional assumptions in the context that are never
discharged. According to the first approach, an axiomatic $a:A$ in our theory
would be given by the rule

$\inferrule{\ }{\Delta\mid\Gamma\vdash a:A}$

Note that because this rule is valid even if $\Gamma$ is empty, it implies
unavoidably that the term $a:A$ is _crisp_. The second approach is more
flexible: we can add assumptions to either the crisp context $\Delta$ or the
cohesive one $\Gamma$. However, _in this paper, whenever we speak of an axiom,
it is to be understood that it is crisp_.

We will also consider some “axioms” that are not stated as assumed elements of
a fixed type, e.g. because they quantify over crisp variables. These can,
however, always be formulated as “unjustified rules”; an example will occur
momentarily. Moreover, once we introduce $\flat$, all such axioms can be
reformulated in the usual way (modulo potential issues with universes, which
we ignore).

###  2.1. The law of excluded middle

With the tool of crisp hypotheses in hand, we can express a version of the law
of excluded middle that does not contradict topological models.

######  Axiom LEM.

(Crisp excluded middle) For any crisp $P::\mathsf{Prop}$, we have $P\vee\neg
P$.

######  Remark .

In ordinary mathematics, we blur the distinction between a _hypothetical
conclusion_ (or _entailment_) and an _implication_ (or _function_). That is,
when we write “if $x:A$ then $f(x):B(x)$”, we might mean that we have
constructed $f(x):B(x)$ under the hypothesis of $x:A$, or we might mean that
we have an element
$f:\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)}}}B(x)$.
These two statements are intimately connected by the introduction and
elimination rules for $\prod$, so no confusion results from failing to
distinguish between them.

However, when the hypothesis is crisp, we have as yet no type-former
corresponding to $\prod$: we cannot abstract over a crisp variable. Thus,
statements such as crisp excluded middle _must_ be read as hypothetical
conclusions. In type-theoretic language, we have to read Axiom LEM as an
“unjustified rule”:

$\inferrule{\Delta\mid\cdot\vdash
P:\mathsf{Prop}}{\Delta\mid\cdot\vdash\mathsf{lem}_{P}:P\vee\neg P}$

rather than an assumed element of some fixed type. (We write
“$\Delta\mid\cdot$” to indicate that the cohesive context is empty.)

Fortunately, in sections 3 and 4 we will introduce new type formers that will
allow us to mostly go back to ignoring this distinction. See section 1 for an
explanation of why we do this in two steps.

To understand why this law of excluded middle is sensible, we need to think a
bit about what a _predicate_ $P:A\to\mathsf{Prop}$ looks like topologically.
In the classical category of topological spaces, the monomorphisms are the
continuous injections; they need _not_ necessarily be subspace inclusions.
Therefore, given a subobject (i.e. a mono) $m:[P]\hookrightarrow A$, there is
a difference between saying that every _point_ of $A$ is in $[P]$ (which is to
say that the injection $m$ is actually a bijection) and saying that $m$ is a
homeomorphism. We regard the judgments “$P(x)$ for all $x::A$” and “$P(x)$ for
all $x:A$” as expressing this same dichotomy in our type theory. The latter
says that $P(x)$ holds for all $x$ _continuously_ as a function of $x$, so
that our monomorphism $m$ must have a section, and hence be a homeomorphism.

Now if $P:A\to\mathsf{Prop}$, its pointwise negation $\neg
P:A\to\mathsf{Prop}$ is, essentially by definition, the _largest subobject of
$A$ disjoint from $P$_. Topologically, this means the corresponding mono
$[\neg P]\hookrightarrow A$ should contain exactly those points of $A$ that
are not in $[P]$, but also that $[\neg P]\hookrightarrow A$ _must be a
subspace inclusion_ — for the inclusion of the subspace determined by those
points is certainly disjoint from $[P]$ and hence must be contained in $[\neg
P]$ as a subobject of $A$.

It should be clear now that the ordinary LEM cannot hold, for it would assert
that for any mono $m:[P]\hookrightarrow A$, the space $A$ is the disjoint
union of the space $[P]$ and the subspace determined by its complement. This
is not true in general even if $[P]$ is a subspace inclusion. However, since
$[P]$ and $[\neg P]$ together do contain all the _points_ of $A$, it is
sensible to assert that for any $x:A$ we have $P(x)\vee\neg P(x)$ _crisply_ ,
and this is what the crisp law of excluded middle gives us.

######  Remark .

It is natural to wonder how we can express internally in type theory the
property that a subobject is a subspace inclusion. The above analysis suggests
that the double negation $\neg\neg P:A\to\mathsf{Prop}$ should be the subspace
containing the same points as $P$, so that $P$ would itself be a subspace if
and only if
$\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)}}}\neg\neg
P(x)\to P(x)$. In section 3 we will introduce another way to express this
property, and in section 3.1 we will prove (using our axioms) that they are
equivalent.

######  Remark .

The assertion that every _subspace_ has a complementary subspace (such that
their disjoint union is the whole space) translates to
$\mathchoice{\prod_{P:\mathsf{Prop}}\,}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}\neg
P\vee\neg\neg P$. Thus, the latter assertion, which is sometimes called _de
Morgan’s law_ (since it is equivalent to the one direction of de Morgan’s laws
that is not constructively valid, $\neg(P\wedge Q)\to(\neg P\vee\neg Q)$), is
not acceptable for us either.

We can try to perform a similar analysis of the axiom of choice. There is one
subtlety: we must realize that the “surjections” of type theory correspond
topologically to _regular epimorphisms_ — which is to say, quotient maps —
rather than arbitrary epimorphisms. One way to see that this must be so is to
recall that any surjection between sets in type theory can be proven to be a
quotient of its domain by some equivalence relation, which is true of regular
epis of spaces but not ordinary ones. Another way is to recall that in type
theory we have a (surjection, embedding) factorization system, and
topologically the left class corresponding to the monomorphisms is the
quotient maps.

Now supposing that $Y\to X$ is a quotient map, of course there may not be any
continuous section of it. However, if the only source of non-classicality is
topology, it should have a _discontinuous_ section. Thus we may hope to be
able to formulate this principle in our type theory. However, if we inspect
the usual formulation of the axiom of choice from [53, Theorem 3.2.2]:

$\left(\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}\mathopen{}\left\|Y(x)\right\|\mathclose{}\right)\to\mathopen{}\left\|\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)\right\|\mathclose{}$

it is not clear how to do this with our current tools. What we want is for the
section
$f:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)$
on the right to be discontinuous. But at present we can only indicate
discontinuity by a conclusion $f(x):Y(x)$ with a crisp hypothesis $x::X$, and
we cannot apply a $\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|\mathclose{}$ _outside_ such a judgment. (The outer
$\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|\mathclose{}$ is, of course, necessary for consistency with
univalence.)

In the next section, therefore, we introduce a new type former $\sharp$ that
“internalizes” such judgments, allowing us to solve this problem (and many
others).

##  3\. The $\sharp$ modality and codiscreteness

Topologically, the function-type
$\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}Y(x)$
represents the space of _continuous_ functions; but as we saw in the last
section, we sometimes want to internalize the notion of a discontinuous
function. Since every function out of a discrete topological space is
continuous, and every function into a codiscrete space is continuous, to make
a discontinuous function continuous all we have to do is retopologize its
domain discretely or its codomain codiscretely. We represent these
“retopologizing” constructions by _modalities_ called $\flat$ and $\sharp$,
which “reify” judgments involving crisp hypotheses.

In this section we study $\sharp$ first, as it is somewhat simpler and stands
on its own better. Described in English, the rules are as follows; a type-
theoretic presentation is shown in fig. 3.

  * •

For any $A:\mathsf{Type}$ there is a type $\sharp A$.

  * •

If $a:A$, then $a^{\sharp}:\sharp A$.

  * •

All crisp variables appearing in $a$ can become cohesive ones in $a^{\sharp}$.
In other words, when we write $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}$, inside the $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$
we are free to use all variables introduced outside of it as if they were
crisp. In yet other words, when we “hit a $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}$” while parsing an expression, all
variables currently in the context become crisp. This expresses the fact that
all functions into a codiscrete space are continuous.

  * •

In the same way, all crisp variables appearing in a type $A$ can become
cohesive ones in $\sharp A$. This expresses the fact that the space of
codiscrete types is itself codiscrete (which may not be obvious, but is true;
we will explain it topologically in section 3.1).

  * •

From any _crisp_ element $x::\sharp A$, we can extract an element
$x_{\sharp}:A$. Of course, since $x$ is crisp, $x_{\sharp}$ is also crisp.

  * •

A computation rule, which says $(a^{\sharp})_{\sharp}\equiv a$. This requires
$(a^{\sharp})_{\sharp}$ to be well-typed, which means that only crisp
variables in the ambient context can occur in $a$. (The above rule says that
when writing $a^{\sharp}$, cohesive variables in the ambient context can be
used as crisp _inside_ $a$; but such variables remain cohesive in the term
$a^{\sharp}$, potentially preventing us from writing $(a^{\sharp})_{\sharp}$.)

  * •

A uniqueness rule, which says $(a_{\sharp})^{\sharp}\equiv a$. This likewise
requires both sides to be well-typed, but now the potential problem lies with
the right-hand side.777Note that if we view this rule as an “expansion”
$a\to_{\eta}(a_{\sharp})^{\sharp}$ rather than a reduction, as is common for
uniqueness rules, then it shares with the computation rule the property that
it can be applied to any well-typed input $a:\sharp A$. In writing
$(a_{\sharp})^{\sharp}$ the cohesive variables in the context might be treated
as crisp inside $a_{\sharp}$ and hence inside $a$, so that $a$ itself might
not be well-typed outside of $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}$.

Δ,Γ∣⋅⊢A:TypeΔ∣Γ⊢♯A : TypeΔ,Γ∣⋅⊢M:AΔ∣Γ⊢M^♯: ♯AΔ∣⋅⊢M:♯AΔ∣Γ⊢M_♯:
AΔ∣⋅⊢M:AΔ∣Γ⊢(M^♯)_♯≡M : AΔ∣Γ⊢M:♯AΔ∣Γ⊢(M_♯)^♯≡M : ♯A

Figure 3. Rules for $\sharp$

######  Remark .

$\sharp$ is a _negative_ type former. This means, roughly, that its
introduction rule(s) are chosen to match its elimination rule(s) rather than
vice versa. For instance, function types are negative because to introduce a
function we use $\lambda$-abstraction, which essentially means we have to say
what will happen when we apply the eliminator (application) on any input. In
the case of $\sharp$, the elimination rule says that we can get to $A$ if we
have a _crisp_ element of $\sharp A$; thus to introduce an element of $\sharp
A$, it suffices to give an element of $A$ under the assumption that everything
is crisp.

Negative type formers tend to require (judgmental) uniqueness rules (whereas
for positive ones, a typal uniqueness rule888Recall that we say “typal” to
mean that a rule is witnessed by an inhabitant of the identity type rather
than being a judgmental equality, avoiding the older term “propositional”
since it may not be a “proposition” in the $(-1)$-truncated sense. is usually
provable). This holds true for $\sharp$.

As our first application, we can make $\sharp$ into a functor: given $f:A\to
B$, we define $\sharp f:\sharp A\to\sharp B$ by

$\sharp f(u)\vcentcolon\equiv f(u_{\sharp})^{\sharp}.$

Note how the type-checking works: inside the $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}$, the variable $u::\sharp A$ is crisp,
so we can write $u_{\sharp}:A$ and apply $f$ to it. We can check
functoriality: if also $g:B\to C$, then

$\displaystyle\sharp g(\sharp f(u))$ $\displaystyle\equiv
g((f(u_{\sharp})^{\sharp})_{\sharp})^{\sharp}$ $\displaystyle\equiv
g(f(u_{\sharp}))^{\sharp}$ $\displaystyle\equiv\sharp(gf)(u).$

In addition, for any $A:\mathsf{Type}$, we have a map $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}:A\to\sharp A$, and we can check that
this is natural:

$\displaystyle\sharp f(x^{\sharp})$ $\displaystyle\equiv
f((x^{\sharp})_{\sharp})^{\sharp}$ $\displaystyle\equiv f(x)^{\sharp}.$

We will often omit parentheses around iterated sub- and superscripted
$\sharp$s (and, later, $\flat$s), maintaining only their order. Thus, for
instance, $g((f(u_{\sharp})^{\sharp})_{\sharp})^{\sharp}$ becomes instead
$g(f(u_{\sharp})^{\sharp}{}_{\sharp})^{\sharp}$, and
$f((x^{\sharp})_{\sharp})^{\sharp}$ becomes
$f(x^{\sharp}{}_{\sharp})^{\sharp}$. This avoids proliferation of parentheses.

Now, recall that our intent was that $\sharp A$ would be $A$ retopologized
codiscretely. Thus, a type should be called _codiscrete_ just when this
operation does nothing to it.

######  Definition .

A type $A:\mathsf{Type}$ is codiscrete if $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}:A\to\sharp A$ is an equivalence.

The rules for $\sharp$ transfer over to theorems about codiscrete types. For
instance, we have:

######  Theorem 3.1.

If $P$ is codiscrete, then when constructing an element of $P$ we may assume
that all variables in the context are crisp.

###### Proof.

Since $P$ is codiscrete, we have an inverse $r:\sharp P\to P$. Thus, it
suffices to construct an element of $\sharp P$. But now we can apply
$(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$, which allows us to
assume all variables are crisp. ∎

######  Theorem 3.2.

If $P:\sharp A\to\mathsf{Type}$ is such that each $P(v)$ is codiscrete, and we
have
$f:\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(x^{\sharp})$,
then we have $g:\mathchoice{\prod_{v:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp A)}}}P(v)$ such that
$g(x^{\sharp})=f(x)$ for all $x:A$. We refer to this principle as
$\sharp$-induction.

###### Proof.

Since each $P(v)$ is codiscrete, we have inverses $r_{v}:\sharp P(v)\to P(v)$.
Thus, to construct $g$ it will suffice to construct for each $v:\sharp A$ an
element of $\sharp P(v)$, and for this it suffices to construct an element of
$P(v)$ assuming a crisp $v::\sharp A$. Now of course we have $v_{\sharp}:A$,
and hence $f(v_{\sharp}):P(v_{\sharp}{}^{\sharp})\equiv P(v)$, as desired. In
symbols,

$g(v)\vcentcolon\equiv r_{v}(f(v_{\sharp})^{\sharp}).$

Finally, we have

$g(x^{\sharp})\equiv r_{v}(f(x^{\sharp}{}_{\sharp})^{\sharp})\equiv
r_{v}(f(x)^{\sharp})=f(x)$

using the computation rule for $\sharp$ and the fact that $r_{v}$ is an
inverse of $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$. ∎

We now show that the codiscrete types form a _reflective subuniverse_ in the
sense of [53, §7.7].

######  Theorem 3.3.

For any $A:\mathsf{Type}$, the type $\sharp A$ is codiscrete.

###### Proof.

Given $z:\sharp\sharp A$, to define an element of $\sharp A$ it suffices to
define an element of $A$ assuming $z$ is crisp. But then we have
$z_{\sharp}{}_{\sharp}:A$. In other words,

$({\lambda}z.\,z_{\sharp}{}_{\sharp}{}^{\sharp}):\sharp\sharp A\to\sharp A.$

Note that we cannot reduce $z_{\sharp}{}_{\sharp}{}^{\sharp}$ to $z_{\sharp}$
using the uniqueness rule, since $z_{\sharp}$ is not well-typed for an
arbitrary (cohesive) $z$.

We now show that this map is inverse to $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}:\sharp A\to\sharp\sharp A$. In one direction, if $z$ is
$y^{\sharp}$ for $y:\sharp A$, we have

$y^{\sharp}{}_{\sharp}{}_{\sharp}{}^{\sharp}\equiv y_{\sharp}{}^{\sharp}\equiv
y$

using the computation rule followed by the uniqueness rule. Note that we could
not do this computation in the other order, because $y^{\sharp}{}_{\sharp}$ is
not well-typed on its own: $y$ is not crisp, so neither is $y^{\sharp}$. In
the other direction, for any $z:\sharp\sharp A$ we have

$z_{\sharp}{}_{\sharp}{}^{\sharp}{}^{\sharp}\equiv z_{\sharp}{}^{\sharp}\equiv
z$

using the uniqueness rule twice; the first use is valid because $z_{\sharp}$
_is_ well-typed inside the outer $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}$. ∎

######  Theorem 3.4.

If $B:\mathsf{Type}$ is codiscrete, then for any $A:\mathsf{Type}$,
precomposition with $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}:A\to\sharp A$ is an equivalence

$(\sharp A\to B)\simeq(A\to B).$

More generally, if $B:\sharp A\to\mathsf{Type}$ has each $B(v)$ codiscrete,
then precomposition with $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}$ is an equivalence

$\left(\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}B(v)\right)\simeq\left(\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}B(x^{\sharp})\right).$

###### Proof.

We prove the more general statement. Since each $B(v)$ is codiscrete,
postcomposition with $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}:B(v)\to\sharp B(v)$ is an equivalence. Thus, by the 2-out-
of-3 property of equivalences, it will suffice to show that the precomposition
map

$\left(\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp A)}}\sharp
B(v)\right)\to\left(\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}\sharp
B(x^{\sharp})\right)$

is an equivalence. Now in the opposite direction, given
$f:\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)}}}\sharp
B(x^{\sharp})$, we can construct $g:\mathchoice{\prod_{v:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp A)}}}\sharp B(v)$ by

$g(v)\vcentcolon\equiv f(v_{\sharp})_{\sharp}{}^{\sharp}.$

Note that this has the form of the left-hand-side of the uniqueness rule, but
that rule doesn’t apply: “$f(v_{\sharp})$” would not be well-typed since $v$
is not a crisp variable. On the other hand, it has the correct type $\sharp
B(v)$ _because_ the uniqueness rule says $v_{\sharp}{}^{\sharp}\equiv v$ since
$v$ is crisp inside the $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}$, hence $f(v_{\sharp}):\sharp
B(v_{\sharp}{}^{\sharp})\equiv\sharp B(v)$.

If we precompose $g$ with $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}:A\to\sharp A$, we get

$g(y^{\sharp})\equiv f(y^{\sharp}{}_{\sharp})_{\sharp}{}^{\sharp}\equiv
f(y)_{\sharp}{}^{\sharp}\equiv f(y)$

where now we have been able to apply the uniqueness rule since $f(y)$ is well-
typed on its own. On the other hand, if we start with $h:\sharp A\to\sharp B$,
precompose it with $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$,
and then extend the result back to $\sharp A$ as above, we get the function
sending $v:\sharp A$ to

$h(v_{\sharp}{}^{\sharp})_{\sharp}{}^{\sharp}\equiv
h(v)_{\sharp}{}^{\sharp}\equiv h(v)$

using the uniqueness rule twice. Applying function extensionality on both
sides completes the proof. ∎

Combining this with Theorem 3.2, by [53, Theorem 7.7.4] we see that the
codiscrete types are actually a _modality_ in the sense of [53, §7.7].
However, in the present paper we are using the word “modality” more generally
to include coreflectors such as $\flat$ in addition to reflectors such as
$\sharp$, so we will refer to modalities in the sense of [53, §7.7] as monadic
modalities.

The fact that $\sharp$ is a monadic modality formally implies many useful
consequences. In particular, essentially all properties of the $n$-truncation
from [53, Chapter 7] that don’t refer to more than one value of $n$ are true
for all monadic modalities, and hence in particular for $\sharp$. Monadic
modalities will be studied further by [45]; here we list some of the main
results, specialized to $\sharp$.

  1. (1)

A type $A$ is codiscrete if and only if $(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}:A\to\sharp A$ admits a retraction.

  2. (2)

If $A,B,C$ are codiscrete, and we have $x,y:A$ and functions $f:B\to A$ and
$g:C\to A$, then the following types are also codiscrete: $\mathbf{1}$A×Bx =_A
yfib_f(x) B×_A C A≃Bis-n-type(A)

  3. (3)

If $A$ is any type and $P:A\to\mathsf{Type}$ is such that each $P(x)$ is
codiscrete, then
$\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}P(x)$
is codiscrete. If in addition $A$ is codiscrete, then
$\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}P(x)$
is also codiscrete.

  4. (4)

For any $A,B$, the canonical map $\sharp(A\times B)\to\sharp A\times\sharp B$
is an equivalence.

  5. (5)

If $A$ is a proposition, so is $\sharp A$.

In fact, $\sharp$ is even a _left exact_ monadic modality, i.e. it preserves
pullbacks. To show this, we begin with an “encode-decode” characterization of
the identity types of $\sharp A$.

######  Theorem 3.5.

For any $x,y:A$, we have an equivalence
$(x^{\sharp}=y^{\sharp})\simeq\sharp(x=y)$ such that the following triangle
commutes:

(3.1)
---
$\textstyle{(x^{\sharp}=y^{\sharp})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{(x=y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{ap}_{(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}}}$$\scriptstyle{(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}}$$\textstyle{\sharp(x=y)}$

###### Proof.

We define $\mathsf{code}:\sharp A\to\sharp A\to\mathsf{Type}$ by

$\mathsf{code}(u,v)\vcentcolon\equiv\sharp(u_{\sharp}=v_{\sharp}).$

Here we use the fact that variables may be assumed crisp inside
$\sharp(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ as well as inside
$(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$. Note that for
$x,y:A$ we have $\mathsf{code}(x^{\sharp},y^{\sharp})\equiv\sharp(x=y)$.

We also have $\mathsf{r}:\mathchoice{\prod_{u:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(u:\sharp A)}}}{\prod_{(u:\sharp
A)}}{\prod_{(u:\sharp A)}}{\prod_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u:\sharp A)}}}{\prod_{(u:\sharp
A)}}{\prod_{(u:\sharp A)}}{\prod_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u:\sharp A)}}}{\prod_{(u:\sharp
A)}}{\prod_{(u:\sharp A)}}{\prod_{(u:\sharp A)}}}\mathsf{code}(u,u)$. For by
Theorem 3.3 $\mathsf{code}(u,u)$ is codiscrete; thus by $\sharp$-induction the
goal reduces to
$\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)}}}\sharp(x=x)$,
which is inhabited by ${\lambda}x.\,\mathsf{refl}_{x}{}^{\sharp}$.

Now we define

$\mathsf{encode}:\mathchoice{\prod_{u,v:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}(u=v)\to\mathsf{code}(u,v)$

in the usual way, $\mathsf{encode}(u,v,p)\vcentcolon\equiv
p_{*}(\mathsf{r}(u))$. To define

$\mathsf{decode}:\mathchoice{\prod_{u,v:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(u,v:\sharp A)}}}{\prod_{(u,v:\sharp
A)}}{\prod_{(u,v:\sharp A)}}{\prod_{(u,v:\sharp
A)}}}\mathsf{code}(u,v)\to(u=v)$

we proceed as follows. Since $\sharp A$ is codiscrete, so is $u=v$, and hence
so are $\mathsf{code}(u,v)\to(u=v)$ and $\mathchoice{\prod_{v:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(v:\sharp A)}}}{\prod_{(v:\sharp
A)}}{\prod_{(v:\sharp A)}}{\prod_{(v:\sharp A)}}}\mathsf{code}(u,v)\to(u=v)$.
Thus we can apply $\sharp$-induction twice, reducing the goal to
$\mathchoice{\prod_{x,y:A}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}\mathsf{code}(x^{\sharp},y^{\sharp})\to(x^{\sharp}=y^{\sharp})$.
But $\mathsf{code}(x^{\sharp},y^{\sharp})\equiv\sharp(x=y)$, so we can use
$\sharp$-induction again followed by $\mathsf{ap}_{(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}}$.

It now suffices to show that $\mathsf{encode}\circ\mathsf{decode}$ is the
identity, since for each $u$ that will exhibit $\mathchoice{\sum_{v:\sharp
A}\,}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp A)}}}\mathsf{code}(u,v)$ as a
retract of the contractible $\mathchoice{\sum_{v:\sharp
A}\,}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp A)}}}{\sum_{(v:\sharp
A)}}{\sum_{(v:\sharp A)}}{\sum_{(v:\sharp A)}}}(u=v)$, hence itself
contractible. Now the goal $\mathsf{encode}(u,v,\mathsf{decode}(u,v,c))=c$ is
an equality in $\mathsf{code}(u,v)$, which is codiscrete by Theorem 3.3. Thus,
the goal is also codiscrete, so we can do $\sharp$-induction again, replacing
$u$ and $v$ by $x^{\sharp}$ and $y^{\sharp}$ respectively, and then
$c:\sharp(x=y)$ by $p^{\sharp}$ for $p:x=y$, so that the goal becomes
$(\mathsf{ap}_{(\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt})^{\sharp}}(p))_{*}((\mathsf{refl}_{x})^{\sharp})=p^{\sharp}$. Finally,
an Id-induction on $p$ completes the proof of equivalence.

To see that (3.1) commutes, we do Id-induction on $p$ again, then compute

$\mathsf{encode}(x^{\sharp},x^{\sharp},\mathsf{ap}_{\sharp}(\mathsf{refl}_{x}))\equiv\mathsf{encode}(x^{\sharp},x^{\sharp},\mathsf{refl}_{x^{\sharp}})\equiv(\mathsf{refl}_{x^{\sharp}})_{*}(\mathsf{r}(x^{\sharp}))\equiv\mathsf{r}(x^{\sharp})=\mathsf{refl}_{x}{}^{\sharp}.\qed$

We remark in passing that this implies that $\sharp$ is “functorial on
homotopies” as well. Given $f,g:A\to B$ and $H:f\sim g$, i.e.
$H:\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)}}}f(x)=g(x)$,
for any $u:\sharp A$ we have
$H(u_{\sharp})^{\sharp}:\sharp(f(u_{\sharp})=g(u_{\sharp}))$, which by Theorem
3.5 can be decoded to give $f(u_{\sharp})^{\sharp}=g(u_{\sharp})^{\sharp}$,
i.e. $\sharp f(u)=\sharp g(u)$. We could also go on to construct higher-
dimensional aspects of a “coherent $\infty$-functor” structure on $\sharp$.

Returning to left-exactness of $\sharp$, this is actually implied formally by
the conclusion of Theorem 3.5 [[, see]]rss:modalities,hottcoq. However, using
the special properties of $\sharp$ we can give a more direct proof, beginning
with a sense in which $\sharp$ “preserves $\sum$s”.

######  Lemma .

For any $A:\mathsf{Type}$ and $B:A\to\mathsf{Type}$, we have

$\sharp\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)}}}B(x)\right)\;\simeq\;\mathchoice{\sum_{u:\sharp
A}\,}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp A)}}}\sharp B(u_{\sharp}).$

(The right-hand side makes sense because inside $\sharp(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})$ we may use $u$ as crisp.)

###### Proof.

The right-hand side is codiscrete, so we can construct a map from left to
right by $\sharp$-induction, sending $(a,b)$ to $(a^{\sharp},b^{\sharp})$.
(Note that if $u$ is $a^{\sharp}$, then $\sharp
B(a^{\sharp}{}_{\sharp})\equiv\sharp B(a)$, so this is well-typed.) In the
other direction it suffices to construct an element of
$\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)}}}B(x)$
supposing crisp hypotheses $u::\sharp A$ and $v::\sharp B(u_{\sharp})$; but
then we have
$(u_{\sharp},v_{\sharp}):\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)}}}B(x)$.
Finally, since both sides are codiscrete, both round-trip composites can be
compared to identities with further $\sharp$-inductions. ∎

######  Theorem 3.6.

$\sharp$ preserves pullbacks.

###### Proof.

Given $f:A\to C$ and $g:B\to C$, recall that the pullback $A\times_{C}B$ is
$\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)}}}\mathchoice{\sum_{(y:B)}\,}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{\sum_{(y:B)}}{\sum_{(y:B)}}}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{\sum_{(y:B)}}{\sum_{(y:B)}}}{\mathchoice{{\textstyle\sum_{(y:B)}}}{\sum_{(y:B)}}{\sum_{(y:B)}}{\sum_{(y:B)}}}(f(x)=g(y))$.
By section 3, we have

$\sharp(A\times_{C}B)\;\simeq\;\mathchoice{\sum_{(u:\sharp
A)}\,}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp A)}}}\mathchoice{\sum_{(v:\sharp
B)}\,}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp
B)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp
B)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp
B)}}}\sharp(f(u_{\sharp})=g(v_{\sharp})).$

while

$\sharp A\times_{\sharp C}\sharp B\;\simeq\;\mathchoice{\sum_{(u:\sharp
A)}\,}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(u:\sharp A)}}}{\sum_{(u:\sharp
A)}}{\sum_{(u:\sharp A)}}{\sum_{(u:\sharp A)}}}\mathchoice{\sum_{(v:\sharp
B)}\,}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp
B)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp
B)}}}{\mathchoice{{\textstyle\sum_{(v:\sharp B)}}}{\sum_{(v:\sharp
B)}}{\sum_{(v:\sharp B)}}{\sum_{(v:\sharp B)}}}(\sharp f(u)=\sharp g(v))$

Thus, it will suffice to prove that for all $u:\sharp A$ and $v:\sharp B$ we
have

$\sharp(f(u_{\sharp})=g(v_{\sharp}))\;\simeq\;(\sharp f(u)=\sharp g(v)).$

But by definition of the functoriality of $\sharp$, the right-hand side is
$f(u_{\sharp})^{\sharp}=g(v_{\sharp})^{\sharp}$. Thus the result follows from
Theorem 3.5. ∎

Left exact monadic modalities also have many nice features, for most of which
we refer to [45] (and which are formalized in [17]). One particularly
important one is the following:

######  Corollary .

$\sharp$ preserves $n$-types for all $n$.

###### Proof.

We induct on $n$. The base case $n=-2$ (i.e.
$\sharp\mathbf{1}\simeq\mathbf{1}$) is true for any monadic modality. Thus,
suppose $\sharp$ preserves $n$-types for some $n$, let $A$ be an $(n+1)$-type,
and let $u,v:\sharp A$. Then $(u=v)$ is codiscrete, hence so is the
proposition “$(u=v)$ is an $n$-type”, so we can use $\sharp$-induction on $u$
and $v$. But by Theorem 3.5, for $x,y:A$ we have
$(x^{\sharp}=y^{\sharp})\simeq\sharp(x=y)$, which is an $n$-type by the
inductive hypothesis. ∎

[45] and [17] show that if a left-exact monadic modality is also _accessible_
in a technical sense (defined there; see also section 9), then the universe of
modal types is modal. We can prove this for $\sharp$ without accessibility,
because of our formation rule for $\sharp A$. The marker {UA} means that we
need the full univalence axiom (although of course for the subuniverse of
propositions we would need only propositional extensionality).

######  Theorem {UA} 3.7.

The universe
$\mathsf{Codisc}\vcentcolon\equiv\mathchoice{{\textstyle\sum_{(A:\mathsf{Type})}}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}\mathsf{iscodiscrete}(A)$
of codiscrete types is codiscrete.

###### Proof.

Suppose $X:\sharp\mathsf{Codisc}$; we want to construct an element of
$\mathsf{Codisc}$ (to define a retraction). The first component of it will be
$\sharp$ of some type, and for the purpose of constructing that type we may
assume $X$ is crisp. Thus, we have $X_{\sharp}:\mathsf{Codisc}$, which we can
destruct further as $(A,c)$ for $A:\mathsf{Type}$ and
$c:\mathsf{iscodiscrete}(A)$. Now we use $A$ to be the type required.
Explicitly, from $X:\sharp\mathsf{Codisc}$ we have constructed

$\sharp(\mathsf{pr}_{1}(X_{\sharp})):\mathsf{Type}$

By Theorem 3.3, this type is codiscrete, so gives an element of
$\mathsf{Codisc}$.

To show that this is a retraction, if $X$ is of the form $Y^{\sharp}$, then we
have

$\sharp(\mathsf{pr}_{1}(Y^{\sharp}{}_{\sharp}))\equiv\sharp(\mathsf{pr}_{1}(Y))$

which is equivalent to $\mathsf{pr}_{1}(Y)$, since by $\mathsf{pr}_{2}(Y)$ the
latter is codiscrete. This completes the proof since codiscreteness is a
proposition. ∎

It follows that we can interpret the formal syntax of ordinary type theory
(with only one kind of context) entirely into the codiscrete types, with
$\mathsf{Codisc}$ playing the role of _the_ universe, obtaining a model with
$\prod$-types, $\sum$-types, a unit type, and identity types. We can also
obtain some (higher) inductive types in this model, at least up to homotopy
[[, in the sense of]§5.5]hottbook, simply by applying $\sharp$ to their
ordinary versions; this includes binary sums, the empty type, the natural
numbers, $n$-truncations, suspensions, and more general colimits.

This doesn’t appear to work for general W-types, however; if $W$ is generated
by a constructor
$\mathsf{sup}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(B(a)\to
W)\to W$, there isn’t even any obvious way to define a function
$\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(B(a)\to\sharp
W)\to\sharp W$. It may be tempting to write
“${\lambda}a.\,{\lambda}b.\,\mathsf{sup}(a,{\lambda}y.\,b(y)_{\sharp})^{\sharp}$”,
but this is ill-typed: although the outer $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})^{\sharp}$ makes all variables in the _current_
context crisp, the inner $\lambda y$ binds a _new_ , _cohesive_ variable $y$,
so that $b(y)$ is not crisp and we cannot apply $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt})_{\sharp}$ to it.

We could work around this if $\sharp$ were accessible, by adding the
appropriate localization constructors to any HIT. Accessibility is a perfectly
reasonable axiom, since it holds in all known examples. But in this paper we
have no need for it, and moreover we want the base spatial type theory of this
part (as opposed to the real-cohesive extension of it in the next part) to be
free of axioms.

As an example of translating type theory into the codiscrete universe, let us
define the Dedekind real numbers codiscretely. Since the types $\mathbb{Z}$
and $\mathbb{Q}$ are abstractly equivalent to $\mathbb{N}$, and
$\sharp\mathbb{N}$ is the natural numbers in the codiscrete world, it follows
that the codiscrete versions of $\mathbb{Z}$ and $\mathbb{Q}$ will be
equivalent to $\sharp\mathbb{Z}$ and $\sharp\mathbb{Q}$ respectively. Now if
we expand out the usual definition of the Dedekind reals $\mathbb{R}$ into the
basic type constructors, we obtain the type shown first in fig. 4.

$\displaystyle\mathbb{R}$
$\displaystyle\vcentcolon\equiv\mathchoice{{\textstyle\sum_{(L,U:\mathbb{Q}\to\mathsf{Prop})}}}{\sum_{(L,U:\mathbb{Q}\to\mathsf{Prop})}}{\sum_{(L,U:\mathbb{Q}\to\mathsf{Prop})}}{\sum_{(L,U:\mathbb{Q}\to\mathsf{Prop})}}\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(q:\mathbb{Q})}}}{\sum_{(q:\mathbb{Q})}}{\sum_{(q:\mathbb{Q})}}{\sum_{(q:\mathbb{Q})}}L(q)\right\|\mathclose{}\times\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(r:\mathbb{Q})}}}{\sum_{(r:\mathbb{Q})}}{\sum_{(r:\mathbb{Q})}}{\sum_{(r:\mathbb{Q})}}U(r)\right\|\mathclose{}$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(q:\mathbb{Q})}}}{\prod_{(q:\mathbb{Q})}}{\prod_{(q:\mathbb{Q})}}{\prod_{(q:\mathbb{Q})}}L(q)\leftrightarrow\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(r:\mathbb{Q})}}}{\sum_{(r:\mathbb{Q})}}{\sum_{(r:\mathbb{Q})}}{\sum_{(r:\mathbb{Q})}}(q<r)\times
L(r)\right\|\mathclose{}\right)$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(r:\mathbb{Q})}}}{\prod_{(r:\mathbb{Q})}}{\prod_{(r:\mathbb{Q})}}{\prod_{(r:\mathbb{Q})}}U(r)\leftrightarrow\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(q:\mathbb{Q})}}}{\sum_{(q:\mathbb{Q})}}{\sum_{(q:\mathbb{Q})}}{\sum_{(q:\mathbb{Q})}}U(q)\times(q<r)\right\|\mathclose{}\right)$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(q:\mathbb{Q})}}}{\prod_{(q:\mathbb{Q})}}{\prod_{(q:\mathbb{Q})}}{\prod_{(q:\mathbb{Q})}}(L(q)\times
U(q))\to\emptyset\right)\land\left(\mathchoice{{\textstyle\prod_{(q,r:\mathbb{Q})}}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}{\prod_{(q,r:\mathbb{Q})}}(q<r)\rightarrow\mathopen{}\left\|L(q)+U(r)\right\|\mathclose{}\right)$
$\displaystyle\mathbb{R}^{\prime}$
$\displaystyle\vcentcolon\equiv\mathchoice{{\textstyle\sum_{(L,U:\sharp\mathbb{Q}\to\mathsf{CodiscProp})}}}{\sum_{(L,U:\sharp\mathbb{Q}\to\mathsf{CodiscProp})}}{\sum_{(L,U:\sharp\mathbb{Q}\to\mathsf{CodiscProp})}}{\sum_{(L,U:\sharp\mathbb{Q}\to\mathsf{CodiscProp})}}\sharp\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(q:\sharp\mathbb{Q})}}}{\sum_{(q:\sharp\mathbb{Q})}}{\sum_{(q:\sharp\mathbb{Q})}}{\sum_{(q:\sharp\mathbb{Q})}}L(q)\right\|\mathclose{}\times\sharp\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(r:\sharp\mathbb{Q})}}}{\sum_{(r:\sharp\mathbb{Q})}}{\sum_{(r:\sharp\mathbb{Q})}}{\sum_{(r:\sharp\mathbb{Q})}}U(r)\right\|\mathclose{}$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(q:\sharp\mathbb{Q})}}}{\prod_{(q:\sharp\mathbb{Q})}}{\prod_{(q:\sharp\mathbb{Q})}}{\prod_{(q:\sharp\mathbb{Q})}}L(q)\leftrightarrow\sharp\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(r:\sharp\mathbb{Q})}}}{\sum_{(r:\sharp\mathbb{Q})}}{\sum_{(r:\sharp\mathbb{Q})}}{\sum_{(r:\sharp\mathbb{Q})}}(q<^{\prime}r)\times
L(r)\right\|\mathclose{}\right)$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(r:\sharp\mathbb{Q})}}}{\prod_{(r:\sharp\mathbb{Q})}}{\prod_{(r:\sharp\mathbb{Q})}}{\prod_{(r:\sharp\mathbb{Q})}}U(r)\leftrightarrow\sharp\mathopen{}\left\|\mathchoice{{\textstyle\sum_{(q:\sharp\mathbb{Q})}}}{\sum_{(q:\sharp\mathbb{Q})}}{\sum_{(q:\sharp\mathbb{Q})}}{\sum_{(q:\sharp\mathbb{Q})}}U(q)\times(q<^{\prime}r)\right\|\mathclose{}\right)$
$\displaystyle\land\left(\mathchoice{{\textstyle\prod_{(q:\sharp\mathbb{Q})}}}{\prod_{(q:\sharp\mathbb{Q})}}{\prod_{(q:\sharp\mathbb{Q})}}{\prod_{(q:\sharp\mathbb{Q})}}(L(q)\times
U(q))\to\sharp\emptyset\right)\land\left(\mathchoice{{\textstyle\prod_{(q,r:\sharp\mathbb{Q})}}}{\prod_{(q,r:\sharp\mathbb{Q})}}{\prod_{(q,r:\sharp\mathbb{Q})}}{\prod_{(q,r:\sharp\mathbb{Q})}}(q<^{\prime}r)\rightarrow\sharp\mathopen{}\left\|\sharp(L(q)+U(r))\right\|\mathclose{}\right)$
Figure 4. The Dedekind reals and their codiscrete version

Thus, their codiscrete version should be the type $\mathbb{R}^{\prime}$ shown
second in fig. 4. In contrast to $\mathbb{Z}$ and $\mathbb{Q}$, it is not at
all obvious that $\mathbb{R}^{\prime}$ has anything to do with
$\sharp\mathbb{R}$; in the former all intermediate constructions are
discontinuous, whereas in the latter we do everything continuously and then at
the very end forget the resulting topology.

We will see later on that they _are_ in fact equivalent (Theorem 6.17), but
this is a very special property of $\mathbb{R}$. In most cases, the
“codiscrete version” of a type $A$ is very different from $\sharp A$. For
instance, $\sharp(\mathbb{R}\to\mathbb{R})$ should be the set of _continuous_
functions $\mathbb{R}\to\mathbb{R}$ topologized codiscretely, whereas
$\mathbb{R}^{\prime}\to\mathbb{R}^{\prime}$ is the set of _discontinuous_
functions.

######  Remark .

The overall conclusion of this section so far can be summarized as “$\sharp$
is a left-exact monadic modality” (plus Theorem 3.7, which could be obtained
from accessibility). This is a purely cohesive statement, i.e. it can be
stated without any need for crisp variables. In [47], using ordinary type
theory without crispness, we took this statement as the axiomatic definition
of $\sharp$. The benefit of instead deriving it from rules involving crisp
variables is that, as we will see in section 4, $\sharp$ then automatically
has the correct relationship to $\flat$.

###  3.1. Excluded middle revisited

With $\sharp$ in hand, we can reformulate the crisp law of excluded middle
(Axiom LEM) as a single term (modulo universe polymorphism).

######  Lemma {LEM} (The sharp law of excluded middle).

$\mathchoice{\prod_{P:\mathsf{Prop}}\,}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}\sharp(P\vee\neg
P)$.

###### Proof.

Assume $P:\mathsf{Prop}$. By the introduction rule for $\sharp$, it suffices
to prove $P\vee\neg P$ assuming a crisp $P::\mathsf{Prop}$. But this is
exactly Axiom LEM. ∎

Let us now return to the topological viewpoint, where codiscrete types have
the codiscrete topology. More generally, if $P:A\to\mathsf{Type}$ and each
$P(x)$ is codiscrete, then
$\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)}}}P(x)$
must have the “final topology” induced by the first projection, i.e. the
coarsest possible topology such that the first projection is continuous. To
see this, note that sections
$\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(x)$
are equivalent to sections
$\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)}}}\sharp
P(x)$, and hence to conclusions $f(x):P(x)$ under crisp hypothesis $x::A$; but
by our topological gloss, these are supposed to be simply discontinuous
sections. Thus, the sections
$\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(x)$
take no account of any topology on $P$, so it must be that $P$ has the final
topology.

######  Remark .

This topological gloss explains why the universe of codiscrete types must
itself be codiscrete. A map into $A$ whose domain has the final topology is
uniquely specified by a map into the underlying set (or $\infty$-groupoid) of
$A$, i.e. it takes no account of the topology of $A$. Thus, a family of
codiscrete types over $A$ should be the same as such a family over $\sharp A$,
which is to say that any map $P:A\to\mathsf{Codisc}$ must factor through
$\sharp A$; thus $\mathsf{Codisc}$ must be codiscrete.

In particular, to say that a predicate $P:A\to\mathsf{Prop}$ is pointwise
codiscrete must mean that it is a _subspace_ , with the induced topology. We
have already seen in section 2.1 a different type-theoretic property that
ought also to characterize subspaces, namely that $P$ is $\neg\neg$-closed. It
turns out that one simple assumption beyond Axiom LEM guarantees that these
two properties coincide. [[, See also]Corollary 4.5.]lm:ac-cohesive

######  Axiom $\sharp\emptyset$.

$\emptyset$ is codiscrete.

######  Theorem {LEM,$\sharp\emptyset$} 3.8.

  1. (1)

A proposition $P$ is codiscrete if and only if $\neg\neg P\to P$.

  2. (2)

For any proposition $P$ we have $\sharp P\simeq\neg\neg P$.

  3. (3)

For any type $A$ we have
$\sharp\mathopen{}\left\|A\right\|\mathclose{}\simeq\neg\neg A$.

###### Proof.

We prove (1) first. Since $P\to\neg\neg P$ always, we have $\neg\neg P\to P$
if and only if $\neg\neg P=P$. Now since $\emptyset$ is codiscrete, so is
$\neg\neg P$ for any $P$. Thus if $\neg\neg P=P$, then $P$ is also codiscrete.

Conversely, suppose $P$ is codiscrete, and suppose that $\neg\neg P$; we must
show $P$. By crisp excluded middle, we have $\sharp(P\vee\neg P)$. Since our
goal $P$ is codiscrete, by $\sharp$-induction we have $P\vee\neg P$. But since
$\neg\neg P$, it must be that $P$. (Note that each of the two assumptions
Axiom LEM and Axiom $\sharp\emptyset$ is used in exactly one direction of this
equivalence.)

Now (2) follows because $\sharp$ and $\neg\neg$ both reflect a proposition
into the sub-poset of codiscrete propositions. Likewise, (3) follows because
$\sharp\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|\mathclose{}$ and $\neg\neg$ both reflect an arbitrary type into
that same poset (since $\neg\neg A$ is always a proposition). ∎

In particular, in this case the statement of section 3.1 is equivalent to

$\mathchoice{\prod_{P:\mathsf{Prop}}\,}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}{\mathchoice{{\textstyle\prod_{(P:\mathsf{Prop})}}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}{\prod_{(P:\mathsf{Prop})}}}\neg\neg(P\vee\neg
P)$

which is a provable statement in type theory. Of course, we used Axiom LEM in
proving Theorem 3.8, so this doesn’t in any way absolve us from having to
assume Axiom LEM. But it is nice to see that the cohesive version of excluded
middle implied by our Axiom LEM is just the one that is already provable in
constructive type theory.

###  3.2. The axiom of choice

We can now revisit the axiom of choice. First, however, let us consider all
the ways of saying that a family $P:A\to\mathsf{Type}$ is “inhabited”, of
which we now have _four_. Here is a list of them with their intended
topological meanings.

  1. (1)

$\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(x)$
says that
$\mathsf{pr}_{1}:(\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)}}}P(x))\to
A$ has a continuous section.

  2. (2)

$\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)}}}\sharp
P(x)$ says that this projection has a _discontinuous_ section.

  3. (3)

$\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)}}}\mathopen{}\left\|P(x)\right\|\mathclose{}$
says that this projection is a quotient map.

  4. (4)

$\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}$
says that this projection is surjective on points.
(Assuming Axiom LEM, this is equivalent to
$\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)}}}\neg\neg{P(x)}$.)

These topological glosses are mainly for our intuition, but in some cases we
can prove precise versions of them in type theory. For instance, statement (1)
makes sense internally and is obviously true. Regarding (2), we can prove:

######  Lemma .

$\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)}}}\sharp
P(x)$ if and only if
$\sharp\mathsf{pr}_{1}:\sharp(\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)}}}P(x))\to\sharp
A$ has a section.

###### Proof.

By $\sharp$-induction
$\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)}}}\sharp
P(x)$ is equivalent to $\mathchoice{\prod_{x:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp A)}}}\sharp P(x_{\sharp})$. This,
in turn, is equivalent to saying that
$\mathsf{pr}_{1}:(\mathchoice{\sum_{x:\sharp
A}\,}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp A)}}}\sharp P(x_{\sharp}))\to\sharp
A$ has a section. But by section 3,
$\sharp(\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)}}}P(x))\simeq\mathchoice{\sum_{x:\sharp
A}\,}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\sum_{(x:\sharp A)}}}{\sum_{(x:\sharp
A)}}{\sum_{(x:\sharp A)}}{\sum_{(x:\sharp A)}}}\sharp P(x_{\sharp})$, and it
is easy to see that the projections match up. ∎

As for (3), if $A$ and $P$ are sets we can consider it justified by [53,
Theorem 10.1.5] (surjections of sets are regular epimorphisms). The general
case requires a more refined notion of “quotient map”, but is also true when
suitably formulated [[, see]]kraus:nonrec-hit,vandoorn:proptrunc-
nonrec,rijke:join.

Finally, regarding (4) we can say the following.

######  Lemma .

$\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}$
if and only if
$\sharp\mathsf{pr}_{1}:\sharp(\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)}}}P(x))\to\sharp
A$ is “codiscretely surjective”, i.e. for all $x:\sharp A$ we have
$\sharp\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$.

Note that “codiscretely surjective” is what we get by interpreting
“surjective” in the universe of codiscrete types, as discussed at the end of
section 3. Thus, it is the appropriate way to say that a map of codiscrete
types “is surjective” in the untopologized world.

###### Proof.

By $\sharp$-induction
$\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}$
is equivalent to $\mathchoice{\prod_{x:\sharp
A}\,}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp
A)}}}{\mathchoice{{\textstyle\prod_{(x:\sharp A)}}}{\prod_{(x:\sharp
A)}}{\prod_{(x:\sharp A)}}{\prod_{(x:\sharp
A)}}}\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$. Thus, it will
suffice to show that for any $x:\sharp A$ we have
$\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}\leftrightarrow\sharp\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$.

Suppose first that
$q:\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$; we will show
$\sharp\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$.
We apply $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$, making our
goal
$\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$
and our hypotheses crisp, allowing us to form
$q_{\sharp}:\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$. Now by
functoriality of $\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|\mathclose{}$, it suffices to assume $p:P(x_{\sharp})$ and prove
$\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)$. But then
$(x_{\sharp},p)^{\sharp}:\sharp(\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)}}}P(x))$,
and

$\sharp\mathsf{pr}_{1}((x_{\sharp},p)^{\sharp})\equiv\mathsf{pr}_{1}(x_{\sharp},p)^{\sharp}\equiv
x_{\sharp}{}^{\sharp}\equiv x.$

Next suppose that
$z:\sharp\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$;
we will show $\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$.
Since $\sharp$ takes values in codiscrete types, it suffices to show
$\sharp\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$. Thus, we
can apply $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})^{\sharp}$ to make our
hypotheses crisp while keeping the goal
$\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$. Now we can form
$z_{\sharp}:\mathopen{}\left\|\mathsf{fib}_{\sharp\mathsf{pr}_{1}}(x)\right\|\mathclose{}$,
and since $\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$ is a
proposition we can destruct $z_{\sharp}$ to obtain
$q:\sharp(\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)}}}P(x))$
and $\sharp\mathsf{pr}_{1}(q)=x$. Next, by $\sharp$-induction we can assume
$q$ is $(y,p)^{\sharp}$ for some $y:A$ and $p:P(y)$. But
$\sharp\mathsf{pr}_{1}((y,p)^{\sharp})\equiv\mathsf{pr}_{1}(y,p)^{\sharp}\equiv
y^{\sharp}$, so we have $y^{\sharp}=x$. And since $x$ is crisp we have
$x\equiv x_{\sharp}{}^{\sharp}$, so $y^{\sharp}=x_{\sharp}{}^{\sharp}$. But by
Theorem 3.5 this type is equivalent to $\sharp(y=x_{\sharp})$. Thus, with
another $\sharp$-induction we obtain $s:y=x_{\sharp}$, so we can transport $p$
along $s$ to get an element of $P(x_{\sharp})$, and finally map it into
$\sharp\mathopen{}\left\|P(x_{\sharp})\right\|\mathclose{}$. ∎

######  Corollary .

If $f:A\to B$ is an embedding and
$\mathchoice{\prod_{x:B}\,}{\mathchoice{{\textstyle\prod_{(x:B)}}}{\prod_{(x:B)}}{\prod_{(x:B)}}{\prod_{(x:B)}}}{\mathchoice{{\textstyle\prod_{(x:B)}}}{\prod_{(x:B)}}{\prod_{(x:B)}}{\prod_{(x:B)}}}{\mathchoice{{\textstyle\prod_{(x:B)}}}{\prod_{(x:B)}}{\prod_{(x:B)}}{\prod_{(x:B)}}}\sharp\mathsf{fib}_{f}(x)$,
then $\sharp f$ is an equivalence.

###### Proof.

Since $f$ is an embedding, so is $\sharp f$. Moreover, $\sharp f$ has
codiscrete fibers. Thus, section 3.2 is sufficient to ensure that it is an
equivalence. ∎

Now, since we cannot expect every surjection to have a continuous section, the
conclusion of our axiom of choice should be
$\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)}}}\sharp
P(x)$. Therefore, it ought to suffice as a hypothesis that it be surjective on
points, i.e.
$\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}$.
Of course, the conclusion must be further $(-1)$-truncated outside the
$\prod$, to be consistent with univalence. This might lead us to state the
axiom of choice as

(3.2)
$\left(\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}\right)\to\mathopen{}\left\|\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)}}}\sharp
P(x)\right\|\mathclose{}.$

However, I believe this is not yet quite right either. Remember that the
entire statement is also parametrized by $A$ and $P$. Thus, (3.2) is actually
asserting that one subobject of
$\mathchoice{\sum_{A:\mathsf{Type}}\,}{\mathchoice{{\textstyle\sum_{(A:\mathsf{Type})}}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}}{\mathchoice{{\textstyle\sum_{(A:\mathsf{Type})}}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}}{\mathchoice{{\textstyle\sum_{(A:\mathsf{Type})}}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}{\sum_{(A:\mathsf{Type})}}}(A\to\mathsf{Type})$
is contained in another. But the first subobject is codiscrete — i.e. has the
subspace topology — whereas the second is _not_ , at least not by definition:
$\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip
1.0pt}\right\|\mathclose{}$ doesn’t preserve codiscreteness. Moreover, the
reverse implication always holds; thus (3.2) is actually asserting that these
two subobjects agree, and hence that the one on the right is a subspace even
though we haven’t forced it to be. This seems unreasonable (although I do not
currently have a concrete counterexample). Thus, instead we take the
following:

######  Axiom AC.

(Sharp axiom of choice) For any set $A$ and type family $P:A\to\mathsf{Type}$,
we have

(3.3)
$\left(\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)}}}\sharp\mathopen{}\left\|P(x)\right\|\mathclose{}\right)\to\sharp\mathopen{}\left\|\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)}}}\sharp
P(x)\right\|\mathclose{}.$

This is admittedly quite a mouthful, and one is left wondering whether it is
good for anything. Are there simpler special cases? What about, for instance,
the _countable_ axiom of choice, where $A=\mathbb{N}$; surely there shouldn’t
be any topology on $\mathbb{N}$ to get in the way. Thus, we now turn to making
sense of what it means to have a _discrete_ topology.

##  4\. The $\flat$ modality

###  4.1. A no-go theorem

Discreteness is encoded by the modality $\flat$ that is dual to $\sharp$.
Whereas $\sharp$ is a reflector into the subcategory of codiscrete types,
$\flat$ is a coreflector into the subcategory of discrete types. However,
unlike $\sharp$, the behavior of $\flat$ cannot be stated as ordinary type-
theoretic rules or axioms, because the resulting pullback-stability would
cause it to degenerate. This is the conclusion of the following “no-go
theorem”.

######  Theorem 4.1.

Suppose we have the following data:

  1. (1)

A predicate $\mathsf{in}_{\Box}:\mathsf{Type}\to\mathsf{Prop}$ that is
invariant under equivalence, i.e. $(A\simeq
B)\to\mathsf{in}_{\Box}(A)\to\mathsf{in}_{\Box}(B)$. (This condition is, of
course, automatic with univalence.)

  2. (2)

An operation $\Box:\mathsf{Type}\to\mathsf{Type}$, such that
$\mathsf{in}_{\Box}(\Box(A))$ for all $A$.

  3. (3)

For each $A:\mathsf{Type}$, a function $\varepsilon_{A}:\Box A\to A$.

  4. (4)

If $\mathsf{in}_{\Box}(B)$, then postcomposition with $\varepsilon_{A}$ is an
equivalence $(B\to\Box A)\simeq(B\to A)$.

Then there exists $U:\mathsf{Prop}$ such that for all $A$ we have

  1. (a)

$\mathsf{in}_{\Box}(A)\leftrightarrow(A\to U)$ and

  2. (b)

$\Box A\simeq(A\times U)$

###### Proof.

Firstly, we observe that if $A$ is a proposition, so is $\Box A$. For if
$x,y:\Box A$, then we have two functions
$\mathsf{const}_{x},\mathsf{const}_{y}:\Box A\to\Box A$ whose composites with
$\varepsilon_{A}$ are equal. Hence $\mathsf{const}_{x}=\mathsf{const}_{y}$ and
thus (evaluating them at $x$, say) $x=y$.

Secondly, we observe that if $\varepsilon_{A}:\Box A\to A$ has a section
$s:A\to\Box A$, then $\mathsf{in}_{\Box}(A)$. It suffices to show that
$s\circ\varepsilon_{A}=\mathsf{id}_{\Box A}$; but these are again two maps
$\Box A\to\Box A$ having the same composite with $\varepsilon_{A}$.

Thirdly, we can extend $\Box$ to a functor such that $\varepsilon$ is a
natural transformation from $\Box$ to the identity. (This is also the dual of
facts we observed in section 3 for $\sharp$.)

Now let $U\vcentcolon\equiv\Box\mathbf{1}$. First we prove (a). On one hand,
if $\mathsf{in}_{\Box}(A)$, then $A\to\mathbf{1}$ factors through $U$. On the
other hand, suppose $f:A\to U$; we will construct a section $s:A\to\Box A$.
For any $x:A$ we have $\mathsf{const}_{x}:\mathbf{1}\to A$, and hence by
functoriality $\Box\mathsf{const}_{x}:\Box\mathbf{1}\to\Box A$. But
$f:A\to\Box\mathbf{1}$, so we have $\Box\mathsf{const}_{x}(f(x)):\Box A$; we
define this to be $s(x)$. Now by naturality of $\varepsilon$, we have

$\varepsilon_{A}(s(x))=\varepsilon_{A}(\Box\mathsf{const}_{x}(f(x)))=\mathsf{const}_{x}(\varepsilon_{\mathbf{1}}(f(x)))=x.$

Thus, $\mathsf{in}_{\Box}(A)$; this completes the proof of (a).

Now we prove (b). By (a), we have $\mathsf{in}_{\Box}(A\times U)$; thus the
projection $\mathsf{pr}_{1}:A\times U\to A$ factors through $\varepsilon_{A}$
by some $g:A\times U\to\Box A$. On the other hand, since
$\mathsf{in}_{\Box}(\Box A)$ we have $f:\Box A\to U$, and thus
$(\varepsilon_{A},f):\Box A\to A\times U$. The composite in one direction is

$(\varepsilon_{A},f)\circ g=(\varepsilon_{A}\circ g,f\circ
g)=(\mathsf{pr}_{1},\mathsf{pr}_{2})=\mathsf{id}_{A\times U}$

where $\varepsilon_{A}\circ g=\mathsf{id}_{A}$ by definition of $g$, while
$f\circ g=\mathsf{id}_{U}$ since $U$ is a proposition. The composite in the
other direction is a map $\Box A\to\Box A$ whose composite with
$\varepsilon_{A}$ is $\varepsilon_{A}$, hence it must be the identity. This
shows (b). ∎

We certainly don’t expect $\flat$ to be of the form $(\mathord{\hskip
1.0pt\text{--}\hskip 1.0pt}\times U)$, so this means that we cannot describe
$\flat$ as ordinary type-theoretic rules or axioms. The central point of
Theorem 4.1 is that the universal property (4) can be applied in an arbitrary
context; this is what enables us to construct a section $A\to\Box A$ from a
map $A\to\Box\mathbf{1}$. Thus, in order to describe a more general
coreflection, we need to restrict the context in which it and its universal
property can be applied. In our current setup, an obvious restriction to try
is that the context should include only crisp variables. This is what we will
do.

###  4.2. The rules for $\flat$

We now describe our rules for $\flat$ in English; a type-theoretic
presentation is shown in fig. 5.

  * •

For any _crisp_ type $A::\mathsf{Type}$, there is a type $\flat A$.

  * •

For any _crisp_ $a::A$, we have $a^{\flat}:\flat A$.

  * •

An element of $\flat A$ may always be assumed to be of the form $u^{\flat}$
for some crisp variable $u::A$. This is called $\flat$-induction.
Syntactically, if $C$ is a type depending on $x:\flat A$, and
$N:C[u^{\flat}/x]$ is an expression depending on a crisp variable $u::A$,
while we have an element $M:\flat A$, we have an induced element

$(\mathsf{let}\;u^{\flat}\coloneqq M\;\mathsf{in}\;N):C[M/x].$

Here the notation $C[M/x]$ indicates that the expression $M$ is substituted
for the variable $x$ in $C$. [53] used function notation when discussing
induction principles, but for $\flat$ we cannot since we do not have a basic
notion of “function of a crisp variable” (indeed, one of the purposes of
$\flat$ is to provide such a notion); thus we have to talk about substituting
into expressions rather than evaluating functions.

  * •

The expected computation rule: $(\mathsf{let}\;u^{\flat}\coloneqq
M^{\flat}\;\mathsf{in}\;N)\equiv N[M/u]$ if $M::A$ is crisp.

It is crucial that we cannot apply $\flat$ to types containing cohesive
variables. This reflects the fact that, by Theorem 4.1, “retopologizing
discretely” is not a _continuous_ operation on the space of spaces. (It _is_
possible to do this for “retopologizing codiscretely”, so that $\sharp$
requires no such restriction. Indeed, by Theorem 3.7 the type of codiscrete
types is codiscrete, so any function into it is automatically continuous.)

Δ∣⋅⊢A:TypeΔ∣Γ⊢♭A :Type Δ∣⋅⊢M:AΔ∣Γ⊢M^♭: ♭A Δ∣Γ,x:♭A ⊢C:Type
Δ∣Γ⊢M:♭A
Δ,u::A∣Γ⊢N:C[u^♭/x]Δ∣Γ⊢(let u^♭ ≔ M in N):C[M/x] Δ∣Γ,x:♭A ⊢C:Type
Δ∣⋅⊢M:A
Δ,u::A∣Γ⊢N:C[u^♭/x]Δ∣Γ⊢(let u^♭ ≔ M^♭ in N) ≡N[M/u] : C[M^♭/x]

Figure 5. Rules for $\flat$

######  Remark .

Strictly speaking, the syntax “$\mathsf{let}\;u^{\flat}\coloneqq
M\;\mathsf{in}\;N$” should also notate the type family $C$, since that is not
generally uniquely inferrable. However, when working informally this will not
matter much.

######  Remark .

Dually to $\sharp$ (see section 3), $\flat$ is a _positive_ type
former.999Well, at least in the usual sense that this adjective is used for
dependent type theories. In the sequent calculus of [28], $\flat$ is
(conjecturally) positive in the precise sense of “focusing”, but our
presentation of $\flat$ breaks some of this positivity. However, this often
happens to positive types when translating from sequent calculus into
dependent type theory. This means, roughly, that its elimination rule is
chosen to match its introduction rule(s). For instance, the coproduct $A+B$ is
positive because to define a (dependent) function _out_ of it, we use case
analysis, which essentially means we have to specify the values of that
function on all the ways to construct an element of $A+B$ (namely via
$\mathsf{inl}$ or $\mathsf{inr}$). In the case of $\flat$, the introduction
rule says that the way to get an element of $\flat A$ is to have a crisp
element of $A$; thus the elimination rule says that to define a function out
of $\flat A$ it suffices to assume we have a crisp element of $A$.

In contrast to negative type formers, whose uniqueness principles tend to be
judgmental rules, positive type formers tend to have uniqueness principles
that are only typal, but can be proven from their elimination and computation
rules. As we will now see, this is also the case for $\flat$.

######  Lemma  (Uniqueness principle for $\flat$).

Let $A::\mathsf{Type}$, $C:\flat A\to\mathsf{Type}$, and
$f:\mathchoice{\prod_{x:\flat A}\,}{\mathchoice{{\textstyle\prod_{(x:\flat
A)}}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat
A)}}}{\mathchoice{{\textstyle\prod_{(x:\flat A)}}}{\prod_{(x:\flat
A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat
A)}}}{\mathchoice{{\textstyle\prod_{(x:\flat A)}}}{\prod_{(x:\flat
A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat A)}}}C(x)$. For any $x:\flat A$ we
have

$(\mathsf{let}\;u^{\flat}\coloneqq x\;\mathsf{in}\;f(u^{\flat}))=f(x).$

###### Proof.

Let $P(x)\vcentcolon\equiv((\mathsf{let}\;u^{\flat}\coloneqq
x\;\mathsf{in}\;f(u^{\flat}))=f(x))$; then $P:\flat A\to\mathsf{Type}$. Thus,
in proving $\mathchoice{\prod_{x:\flat
A}\,}{\mathchoice{{\textstyle\prod_{(x:\flat A)}}}{\prod_{(x:\flat
A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat
A)}}}{\mathchoice{{\textstyle\prod_{(x:\flat A)}}}{\prod_{(x:\flat
A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat
A)}}}{\mathchoice{{\textstyle\prod_{(x:\flat A)}}}{\prod_{(x:\flat
A)}}{\prod_{(x:\flat A)}}{\prod_{(x:\flat A)}}}P(x)$ we can use
$\flat$-induction. But when $x$ is $v^{\flat}$, we have
$P(v^{\flat})\equiv(f(v^{\flat})=f(v^{\flat}))$, using the computation rule
for $\flat$ on the left-hand side, and this is trivial by reflexivity. In
symbols, we have

$(\mathsf{let}\;v^{\flat}\coloneqq
x\;\mathsf{in}\;\mathsf{refl}_{f(v^{\flat})})\;:\;(\mathsf{let}\;u^{\flat}\coloneqq
x\;\mathsf{in}\;f(u^{\flat}))=f(x).\qed$

As with $\sharp$, we can make $\flat$ into a functor, at least on crisp
functions: given $A,B::\mathsf{Type}$ and $f::A\to B$, we define $\flat
f:\flat A\to\flat B$ by

(4.1) $\flat f(x)\vcentcolon\equiv(\mathsf{let}\;u^{\flat}\coloneqq
x\;\mathsf{in}\;f(u)^{\flat}).$