CHAPTER: LOGICAL PRELIMINARIES
logic|(type theory|(

In this chapter, we transition from an external point of view to an internal one. In
<ref> we defined the interval domain $\IR$, and in
<ref> we defined a quotient $\BaseTopos\cong\Shv{\BaseSite}$ of its
topos of sheaves. A main goal of this book is to define a temporal type theory—including one atomic predicate and
ten axioms—that has semantics in $\BaseTopos$; we do this in <ref>. In the present
chapter, we attempt to provide the reader with a self-contained account of the sort of type theory
and logic we will be using, as well as some important concepts definable therein.

We begin in <ref> with an informal introduction to our type theory and
logic, as well as its relation to toposes. We then discuss modalities in
<ref>,modality, which are the internal view of what in topos theory
literature are often called Lawvere-Tierney topologies or local operators. Logically, modalities are
internal monads on the type $\Prop$ of propositions, whereas semantically they correspond to
subtoposes. Finally in <ref>, we discuss numeric types, e.g. the Dedekind real
numbers and related types, relative to an arbitrary modality. In this section we also discuss
inequalities between, and the arithmetic of, numeric types.

§ INFORMAL INTRODUCTION TO TYPE THEORY

In this section we will informally introduce the type theory we use in the remainder of the book. We
justify the lack of formality in three ways. First, most of what we do is relatively standard
material: higher-order logic on top of the simply-typed lambda
calculuslambda calculus, simply typed with sum typestype!sum and a type of natural
numberstype!of natural numbers, plus subtypestype!subtype and quotient
typestype!quotient. However, we also make very limited use of dependent
typestype!dependent, so providing full details of our type theory would be a major endeavor.
This is the second reason: a full account would simply take too much space to be worthwhile. And the
third reason is that we want to be users of logic—not logicians—here. Thus we will present
enough information to get readers started; for those who want a full account of categorical logic
and type theory, we recommend <cit.>.

What will matter most is that our type theory is constructivelogic!constructive and has an
object $\Prop$ of propositions—and hence has a higher-order logic.logic!higher order It is
well-known that this logic has semantics in any topos <cit.>. Sometimes we
use dependent types, subtypes, and quotient types; it is less well-known but true that these also
have semantics in any topos <cit.>. While we were not able to find a reference, we
believe that the Calculus of Constructions (<cit.>)—used in the automated proof
assistants Lean and
CoqCoq|see automated proof assistantLean|see automated proof assistant—also
has sound semantics in any topos, so the system we present below could be formalized in either proof
The dependent type theory in <cit.> is sound and complete for 1-toposes, relying
heavily on extensivity of typestype!extensive. This is fine for 1-toposes, but it makes
computability impossible and hence is not useful for a proof assistant like Coq. On the other
hand, the Calculus of Constructions (<cit.>) and related formalisms used in Coq
and Lean are formulated using a hierarchy of universes. We believe this aspect of the Calculus of
Constructions is sound for toposes, and we believe this follows from <cit.>, but
could not find an explicit reference.

§.§ Notions from the simply-typed lambda calculus
lambda calculus, simply typed|(

In this section (<ref>) we give an informal account of the simply-typed lambda
calculus. The material is standard; see e.g. <cit.>. The key words
we will discuss are: types, variables, contexts, terms, substitution, and
conversion rules. As we get into <ref> and begin to talk about logic, we will add
propositions, premises, and truth judgments.typevariablecontexttermsubstitutionconversion rulepropositionpremisetruth judgment

It is important to understand the relationship between a type theory and its semantics in the
appropriate kind of category, say a topos $\cat{E}$, without conflating the two.semantics!of a type theory Each has value
independent of the other; for example, computers do not work on semantics, they work on syntax.
Having a syntax that “compiles” to our chosen semantics can be quite freeing, because proofs in
the logic are far easier to check than those in the semantics they compile to. Moreover, there is
not always a perfect correspondence between what is important in type theory and what is important
in semantics. For example, variables and contexts in a type theory have little semantic meaning.
Still, the connection between the type theory and its $\cat{E}$-semantics is important, so we
summarize the touch points now, and will continue to do so throughout the section.

Types in our type theory correspond to objects in $\cat{E}$. Variables and contexts—which are
lists of variables and types—mainly serve a bookkeeping role. They gain semantic meaning when they
are attached to terms. That is, a well-formed term always has a context and a type; it looks like

\begin{equation}\label{eqn:sample_term}
a:A, b_1:B, b_2:B\vdash f(a,g(b_1,b_2),a):C
\end{equation}

Here, $A$, $B$, and $C$ are types; $a$, $b_1$, and $b_2$ are variables; $a$, $b_1$, $b_2$,
$g(b_1,b_2)$, and $f(a,g(b_1,b_2),a)$ are terms. These terms appear in the context $a:A, b_1:B, b_2:B$ and, for example the term $f(a,g(b_1,b_2),a)$
has type $C$. A term corresponds to a morphism in $\cat{E}$; its domain is the product of types in
its context, and its codomain is its type. So in the above example, $f(a,g(b_1,b_2),a)$ presents a
morphism $A\times B\times B\to C$.

There is a grammar for types and a grammar for terms, meaning that new types and terms can be
produced from old using what are called type constructors and term constructors.constructor!typeconstructor!term There
are several rules that dictate when the resulting types and terms are well-formed and when two terms
are declared equal; the latter are the conversion rules. Issues like which variables are free and
how substitution works for replacing a variable by a term (one must be careful that variables are
not accidentally bound in the process)variable!free/bound, can be carefully worked out. This is important for computer
applications, and may be interesting, but it will not concern us much here because mathematicians
have generally developed an engineer's sense of how to work with types and terms without needing to
know much about what goes on under the hood.

We now expand on the above summary of the simply-typed lambda calculus and its semantics.

We begin with types. One may declare atomic types $\const{T}_1,\const{T}_2,\ldots$ (though we will
not need to do so in this book). The type $\Prop$ of propositions, the type $\tNN$ of natural
numbers, the empty type $\const{empty}$, and the unit type $1$ are given as a base types, without
needing to declare them. From these, one may form new types by taking finite products, finite sums,
and arrow types; these are the type constructors. So suppose we declare $\const{T}$ to be our only
atomic type. Then we also have, for example, the three following types:constructor!typetype!atomictype!unittype!producttype!emptytype!of natural numberstype!of propositionstype!arrow

\[
\const{T}\times \const{T}\times \const{T},\quad
1, \quad
\const{T}\times\Prop\to(\tNN\to (\const{T}+1)).
\]

To give types semantics in $\cat{E}$, one must choose an object for each atomic type
($\const{T}_i$). The rest is automatic: the type $\Prop$ corresponds to the subobject classifier in
$\Cat{E}$, the type $\tNN$ corresponds to the natural numbers object in $\cat{E}$, the types
$\const{empty}$ and $1$ correspond to the initial and final objects of $\cat{E}$, the product types
correspond to products in $\cat{E}$, and arrow types correspond to exponential objects in $\cat{E}$.

Before moving on, we make two notes. First, there is a common convention to reduce parenthetical clutter: a sequence of
arrow-types is parsed by “right associativity”.associativity!right That is, $\tau_1\to(\tau_2\to\tau_3)$ can be
written simply as $\tau_1\to\tau_2\to\tau_3$. Second, we mentioned that one can declare some atomic types. We will later see that one can declare atomic terms and atomic predicates as well. All of these declarations make up what is called a signature. We will present a specific signature for temporal type theory in <ref>.signature

Variables and contexts.

One assumes that an infinite set of symbols $V$ has been fixed in advance for use as variables. Then saying “$a$
is a variable” just means $a\in V$. We also assume that $V$ is disjoint from all other sets of
symbols we use, to avoid ambiguity.variable

On its own, a variable $a\in V$ has no type. For expressions involving $a$ to be meaningful, a type
for $a$ must first be declared. As mentioned above, a context is a list of distinct variables, each with a
type declarationcontext. For example, if $\tau_1$ and $\tau_2$ are types and $x$, $y$, and $z$ are
variables then $x:\tau_1,\,y:\tau_2,\,z:\tau_2$ is a context. Thus every expression will
be considered relative to some (explicit or implicit) context, which defines the type of each variable used
in the expression. To make contexts explicit, we use the standard notation
$x:\tau_1,\,y:\tau_2\vdash e$ to state that the expression $e$ is being considered in the context
$x:\tau_1,\,y:\tau_2$. While contexts are technically lists, type theories such as ours have rules
that ensure that order does not matter.

A context, such as $x_1:\tau_1,\ldots,x_n:\tau_n$, is often denoted $\Gamma$; if $\Gamma'$ is
another context, we may write $\Gamma,\Gamma'$ to denote the union of these contexts.

Terms are certain expressions which represent “elements” of types. A term $t$ may contain
variables as in <ref>, in which case $t$ represents a parameterized family of elements. We require that
every term $t$ be explicitly paired with a context declaring the types of all free variables
occuring in $t$, and we also require that every term itself has a unique type. We write
$\Gamma\vdash t:\tau$ to record that the term $t$ has type $\tau$ in context $\Gamma$.

As part of a signaturesignatureterm!atomic, one may declare a finite number of atomic terms $c:\tau$, each having a specified type, in this case $c$ has type
$\tau$. Each declared atomic term is valid in the empty context, e.g. $\vdash c:\tau$ would be
judged “valid”. A variable of a given type is also a term, but it is only valid in a context
containing it. For example, $a:\tNN, b:\const{T}\vdash a:\tNN$ is judged valid, assuming
$a$ and $b$ are variables.

For the base types $\Prop$, $\tNN$, $\const{empty}$, and $1$, as well as for each type constructor,
there are associated term constructors. We will hold off discussing $\Prop$ until <ref>,
because it is the most complex, in order to focus on the main idea here.constructor!typeconstructor!term

The type $\tNN$ has three term constructors:

* $\vdash 0:\tNN$,

* $a:\tNN\;\vdash s(a):\tNN$,  and

* $e:\tau,\;f:\tau\to\tau,\;g:\tNN\;\vdash\const{rec}(e,f,g):\tau$,

where the last exists for any type $\tau$. Similarly,

* product types have term constructors called tupling and projecting;

* sum types have term constructors called co-tupling and co-projecting; and

* arrow types have term constructors called lambda abstraction and application.

All of these are standard,
[Note that what we call sum types are called “coproduct types” in <cit.>.]
but we discuss the last of these to give more of the flavor.

We begin with the term constructor for evaluation, because it is straightforward:evaluation

\[
f:\tau_1\to\tau_2,\;a:\tau_1\;\vdash \const{ap}(f,a):\tau_2.
\]

We often denote $\const{ap}(f,a)$ simply by $f(a)$ or $fa$.

lambda abstractionThe lambda abstraction term constructor is a bit more subtle. The corresponding mathematical idiom
is something like this: “Suppose $a$ is an integer. Using $a$ we can define a rational $b$ as
follows $\ldots$. This defines a function $\tZZ\to\tQQ$, given by $a\mapsto b$.” For any context
$\Gamma$, types $\tau_1,\tau_2$, and term $\Gamma,\;a:\tau_1\vdash b:\tau_2$, where obviously $b$ is
allowed to use variables from the context, there is a term $\Gamma\vdash\lambda(a:\tau_1)\ldotp

In case the notation is not clear, this says $\lambda(a:\tau_1)\ldotp b$ has arrow type

In the expression $\lambda(a:\tau_1)\ldotp b$, the variable $a$ has been boundvariable!free/bound, meaning it is
no longer free. This has two consequences. The first is that the variable $a$ can be replaced by any
other variable without changing the term; this is called $\alpha$-conversion and we mention it
briefly when we discuss conversion rules; see <ref>. The second is that one
can no longer substitute an arbitrary expression for $a$; we discuss substitution next.conversion!$\alpha$

As always, a variable of type $\tau$ represents an indeterminate value of type $\tau$. Thus, if
$x:\tau\vdash e:\tau'$ is a term—so $e$ may contain the variable $x$—then we are free to replace
$x$ throughout $e$ with any concrete term of type $\tau$.

In this sense, terms can be substituted for free variables. Suppose $a:X$ is a variable of some type $X$ and
$\Gamma\vdash e:X$ is a term of the same type. Then $[a\coloneqq e]$ denotes a sort of
search-and-replace function, sending terms to terms. That is, for any term of the form
$\Gamma',a:X\vdash f:\tau$, we can search for free occurrences of $a$ in $f$ and replace them with
$e$, and the result is the term $\Gamma',\Gamma\vdash [a\coloneqq e]f:\tau$.

As the $[a\coloneqq e]$ notation can get unwieldy, we introduce a convenient shorthand. If
$\Gamma,x:\tau\vdash e:\tau'$ is a term, then we can write $\Gamma,x:\tau\vdash e(x):\tau'$ to draw
attention to the fact that the variable $x$ occurs in $e$ (even though other variables from $\Gamma$
might also occur in $e$). Then instead of $[x\coloneqq t]e$, we can more simply write $e(t)$.

Conversion rules.conversionconversion!universal properity as
The term constructors are meant to express universal properties about our various type constructors,
and we want to force these to be true in the $\cat{E}$-semantics. So far, we have constructed the
terms—which correspond to morphisms in $\cat{E}$—but we have not specified anything that says
the appropriate diagrams commute. This is the job of conversion rules.

A conversion rule is a rule of the form

\[
\Gamma\vdash e_1\equiv e_2:\tau,
\]

where $\Gamma\vdash e_1:\tau$ and $\Gamma\vdash e_2:\tau$ are terms. There are conversion rules for
each type constructor, but again they are standard as well as straightforward, so we only write out
a few, namely those for natural numbers and arrow types. We also leave out the context and the
typing to clarify the idea:

\begin{equation}\label{eqn:example_conversions}
\begin{aligned}
\const{rec}(e,f,0)&\equiv e&\text{base case}\\
\const{rec}(e,f,s(g))&\equiv f(\const{rec}(e,f,g))&\hspace{1in}\text{recursive step}\\
(\lambda(a:\tau_1)\ldotp f(a))(e)&\equiv f(e)&\text{$\beta$-reduction}\\
\lambda(a:\tau_1)\ldotp f(a) &\equiv f&\text{$\eta$-conversion}\\
\lambda(a:\tau_1)\ldotp f(a)&\equiv\lambda(b:\tau_1)\ldotp f(b)&\text{$\alpha$-conversion}
\end{aligned}
\end{equation}

If we want to be a bit more pedantic and add back in the context and type, the first above is

\[
e:\tau,\;f:\tau\to\tau,\;g:\tNN\vdash\const{rec}(e,f,0)\equiv e:\tau,
\]

etc. Hopefully the necessary context in each of the cases from <ref> is
clear enough.

[Arithmetic of natural numbers]arithmetic!of natural numbers
Suppose we want to construct a term $m:\tNN,n:\tNN\vdash \const{plus}(m,n):\tNN$ for addition of
natural numbers. Define it to be

\begin{equation}\label{eqn:addition_of_nats}
m:\tNN,n:\tNN\vdash\const{rec}(m,\lambda(x:\tNN)\ldotp s(x),n):\tNN,
\end{equation}

where $s$ is the successor. We use the usual infix notation $m+n$ as shorthand for this term.
In fact, we could have written <ref> before discussing conversion rules, but now that we have conversion rule we check that our definition
actually does what we want: $m+0\equiv m$ and $m+s(n)\equiv s(m+n)$.
Multiplication of natural numbers is given by

\[
m:\tNN,n:\tNN\vdash\const{rec}(0,\lambda(p:\tNN)\ldotp m+p, n).
\]

We can also define a function $+\colon(\tNN\times\tNN)\to\tNN$ by lambda abstraction:
$+(m,n)\coloneqq\lambda((m,n):\tNN\times\tNN)\ldotp\const{plus}(m,n)$, and similarly for

Propositions, premises, and truth judgments.propositionpremisetruth judgment
From the perspective of specifying a type theory and logic, one has—in addition to types, terms,
etc.—things called propositions $P$, which have a status similar to types and terms. While
a type is something that intuitively has “elements”, and the type theory provides rules for
constructing terms of that type, a proposition is something that intuitively has a “truth value”,
and the type theory provides rules for constructing proofs of that proposition.

We are presenting a higher-order logic, which means there is a special type $\Prop$, and
propositions are identified with terms of type $\Prop$. We will describe how to build new
propositions from old in <ref>.

Before getting to that, we will quickly explain premises and truth judgments. A premise is
like a context: it is a finite list of propositions. That is, if $P_1,\ldots,P_n$ are valid
propositions, then $\Theta=\{P_1,\ldots,P_n\}$ is a premise. Finally a truth judgment consists of a
context $\Gamma$, a premise $\Theta$, and a proposition $Q$; it looks like this:context!premise

\begin{equation}\label{eqn:truth_judgment}
\Gamma\mid\Theta\vdash Q.
\end{equation}

<Ref> basically says that, in the context $\Gamma$ (where all the variables used in $P_1,\ldots,P_n$
and $Q$ are defined), the conjunction of $P_1$ through $P_n$ is enough to conclude $Q$. But we will
explain this more in the next section, where we discuss how one decides which truth judgments are
lambda calculus, simply typed|)

§.§ Higher order logic
logic!higher order

Logic is a set of rules about propositions and predicates, by which we can decide validity. We
discussed the type $\Prop$ of propositions above; a predicate is just a term of type $\Prop$,
say $\Gamma\vdash P:\Prop$.predicatepredicate!atomic We often refer to $P$
simply as a proposition, since it is a term of type $\Prop$, rather than as a predicate. In other
words, the fact that there is a context—possibly empty—is assumed, as usual.

Just like a type theory begins with a set of atomic types and a set of atomic terms, it also begins
with a set of atomic predicates, again of the form $\Gamma\vdash P:\Prop$. Together the atomic types, terms, and predicates make up a signaturesignature.

§.§.§ Obtaining new propositions from old

One important way to form a proposition is by equality. Namely, given a type $\tau$ and terms
$a:\tau$ and $b:\tau$, there is a proposition $(a=b):\Prop$. There are also the logical connectives:
given propositions $\Gamma\vdash P:\Prop$ and $\Gamma\vdash Q:\Prop$, we have

\begin{gather*}
\top:\Prop\qquad
\bot:\Prop\qquad
P\wedge Q:\Prop\qquad
P\vee Q:\Prop\qquad
P\imp Q:\Prop
\end{gather*}

all in the context $\Gamma$.
[The propositions $\neg P$ and $P\iff Q$ are just shorthands for $P\imp\bot$ and $(P\imp Q)\wedge(Q\imp P)$.]
These are pronounced true, false, $P$ and $Q$, $P$ or $Q$, and $P$ implies $Q$, respectively. Given a predicate $\Gamma,x:\tau\vdash P:\Prop$, one also has the quantifiers

\[
\Gamma\vdash\forall(x:\tau)\ldotp P:\Prop \qquad
\Gamma\vdash\exists(x:\tau)\ldotp P:\Prop
\]

pronounced for all $x$ of type $\tau$, $P$ and there exists $x$ of type $\tau$ such that $P$. Note that, just like lambda abstraction binds a variable in a term, the quantifiers bind a variable
in a proposition.

Before moving on, we note a common convention to reduce parenthetical clutter: a sequence of
implications is parsed by “right associativity”. That is, $P\imp(Q\imp R)$ can be written simply
as $P\imp Q\imp R$. Once we have rules for deduction, we will be able to deduce that $P\imp Q\imp R$
is equivalent to $(P\wedge Q)\imp R$.associativity!right

§.§.§ Valid truth judgments
truth judgment|(

To do logic, one begins with a set of axiomsaxiom, and proceeds to judge which propositions are true. The
technical form of this is the truth judgment <ref>. In this section we give the
rules for determining which truth judgments are valid in a given premise context $\Gamma\mid\Theta$,
given a set $\cat{A}$ of axioms. Validity of a truth judgment is inductively derived using
certain allowable steps, called proof rules. We divide the proof rules into four main
subgroups: premises and axioms, equalities, the connectives, and the quantifiers.

Premises and axioms.

An axiom is a truth judgment, i.e. a statement of the form $\Gamma\mid\Theta\vdash P$. Axioms are
automatically valid as truth judgments. Similarly, $\top$ is always valid. If $P:\Prop$ is in the
list of propositions defining a premise $\Theta$ then $\Gamma\mid\Theta\vdash P$ is valid. Technically, these
three rules could be written as follows:

\begin{equation}\label{eqn:premise_axiom}
\begin{prooftree}
\Hypo{\Gamma\vdash\Theta\Prem}
\Infer1{\Gamma\mid\Theta\vdash\top}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\vdash\Theta\Prem}
\Infer[left label={\side{P\in\Theta}}]1{\Gamma\mid\Theta\vdash P}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Infer[left label={\side{(\Gamma\mid\Theta\vdash P)\in\cat{A}}}]0{\Gamma\mid\Theta\vdash P}
\end{prooftree}
\end{equation}

The first says that if $\Theta$ is a valid premise in context $\Gamma$ (i.e. if all the symbols
used in the propositions in $\Theta$ are defined in $\Gamma$), then $\Gamma\mid\Theta\vdash\top$ is
valid. The second is similar, but adds a side condition that $P$ is one of the propositions in
$\Theta$, in which case $\Gamma\mid\Theta\vdash P$ is valid. The third says that axioms are
automatically valid.

As expected, one can prove by induction that if one increases the premise by adding a new
proposition, the set of valid truths one can derive does not decrease. This is called
weakening. Thus if $\Gamma\vdash Q:\Prop$ is a term and
$\Gamma\mid\Theta\vdash Q$ is a valid truth judgment, then so is $\Gamma\mid\Theta,P\vdash Q$ for
any proposition $P$ in the same context, $\Gamma\vdash P:\Prop$.

Recall the notion of conversion rules from <ref>, page
page:conversion_rules. These are of the form $\Gamma\vdash e_1\equiv e_2:\tau$. Every such
conversion rule gives rise to a valid truth judgment $\Gamma\vdash e_1=e_2$. Written more

\[
\begin{prooftree}
\Hypo{\Gamma\vdash\Theta\Prem}
\Hypo{\Gamma\vdash e_1\equiv e_2:\tau}
\Infer2{\Gamma\mid\Theta\vdash e_1=e_2}
\end{prooftree}
\]

New valid truth judgments of the form $\Gamma\vdash e_1=e_2$ can be generated from old by
reflexivity, symmetry, and transitivity, as well as by substitution. For example, we also have

\[
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash e_1=e_2}
\Hypo{\Gamma\mid\Theta\vdash e_2=e_3}
\Infer2{\Gamma\mid\Theta\vdash e_1=e_3}
\end{prooftree}
\]

The connectives.

Most of the valid truth judgments coming from connectives and quantifiers are fairly obvious, but
there are differences between classical logic and constructive logic, so we should be a bit careful.
This difference only makes an appearance in disjunction $\vee$ and existential quantification
$\exists$. Instead of starting there, we begin with a familiar case, namely conjunction. The rules
for conjunction are

\[
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\phi_1}
\Hypo{\Gamma\mid\Theta\vdash\phi_2}
\Infer2{\Gamma\mid\Theta\vdash\phi_1\wedge\phi_2}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\phi_1\wedge\phi_2}
\Infer1{\Gamma\mid\Theta\vdash\phi_1}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\phi_1\wedge\phi_2}
\Infer1{\Gamma\mid\Theta\vdash\phi_2}
\end{prooftree}
\]

These correspond to mathematical idioms such as “We have $\phi_1$ and $\phi_2$, so in particular we
have $\phi_1$.”

The rules for implication are:

\[
\begin{prooftree}
\Hypo{\Gamma\mid\Theta,\phi_1\vdash\phi_2}
\Infer1{\Gamma\mid\Theta\vdash\phi_1\imp\phi_2}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\phi_1\imp\phi_2}
\Hypo{\Gamma\mid\Theta\vdash\phi_1}
\Infer2{\Gamma\mid\Theta\vdash\phi_2}
\end{prooftree}
\]

The first corresponds to the mathematical idiom “To prove $\phi_1\imp\phi_2$, we assume $\phi_1$
and attempt to show $\phi_2$,” while the second corresponds to the idiom “We know that $\phi_1$
implies $\phi_2$, so since $\phi_1$ holds, so does $\phi_2$.”

The constant $\bot$, representing falsehood, may seem at first sight rather useless, but it plays an
important role in constructive logic. Its only rule is the following, which says intuitively “if we
can prove false, then we can prove anything”:

\[
\begin{prooftree}
\Hypo{\Gamma\vdash\phi:\Prop}
\Hypo{\Gamma\mid\Theta\vdash\bot}
\Infer2{\Gamma\mid\Theta\vdash\phi}
\end{prooftree}
\]

In constructive logic, negation is not a primitive connective. Rather, $\neg P$ is simply shorthand
for $P\imp\bot$. Thus $\neg P$ means precisely “if $P$ were true, we could prove false.”
So trivially, we have that $P\imp\bot$ implies $\neg P$, but it is emphatically not the case
that $\neg P\imp \bot$ implies $P$. That is, in constructive logic there is no
“proof-by-contradiction”: just because assuming $P$ is false leads to a contradiction, that does
not provide a proof that $P$ is true. Instead, all we can say is that $\neg P\imp \bot$ implies
$\neg\neg P$. As an exercise, the reader might try proving that $\neg\neg\neg P$ implies $\neg P$.

There are three rules for disjunction. The first corresponds to the idiom “We know that either
$\phi_1$ or $\phi_2$ holds. Either way we can prove $\phi_3$, so $\phi_3$ holds.”

\[
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\phi_1\vee\phi_2}
\Hypo{\Gamma\mid\Theta,\phi_1\vdash\phi_3}
\Hypo{\Gamma\mid\Theta,\phi_2\vdash\phi_3}
\Infer3{\Gamma\mid\Theta\vdash\phi_3}
\end{prooftree}
\]

The next two are more obvious, but note that—other than via axioms—there is no way to derive
$\phi\vee\neg\phi$. The only way to derive a disjunction is to derive one of the disjuncts.
Similarly, given $\phi_1\imp\phi_2$, it does not necessarily follow that $\neg\phi_1\vee\phi_2$.

\[
\begin{prooftree}
\Hypo{\Gamma\vdash\phi_2:\Prop}
\Hypo{\Gamma\mid\Theta\vdash\phi_1}
\Infer2{\Gamma\mid\Theta\vdash\phi_1\vee\phi_2}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\vdash\phi_1\Prop}
\Hypo{\Gamma\mid\Theta\vdash\phi_2}
\Infer2{\Gamma\mid\Theta\vdash\phi_1\vee\phi_2}
\end{prooftree}
\]

The quantifiers.

Like lambda-abstraction, the quantifiers change the context by binding variables. Here are the proof
rules for the universal quantifier:

\[
\begin{prooftree}
\Hypo{\Gamma,x:\tau\mid\Theta\vdash\phi}
\Infer[left label={\side{x\notin\fv(\Theta)}}]1{\Gamma\mid\Theta\vdash\forall(x:\tau)\ldotp\phi}
\end{prooftree}
\hspace{.5in}
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\forall(x:\tau)\ldotp\phi(x)}
\Hypo{\Gamma\vdash e:\tau}
\Infer2{\Gamma\mid\Theta\vdash\phi(e)}
\end{prooftree}
\]

The first rule corresponds to the mathematical idiom, “To prove $\forall(x:\tau)\ldotp\phi$, it
suffices to take an arbitrary element $x$ of type $\tau$ and prove $\phi$.” The word “arbitrary”
signifies that $x$ is not already being used in the assumptions $\Theta$, which is formalized by
saying $x$ is not in the set $\fv(\Theta)$ of free variables occurring in $\Theta$. The second rule
corresponds to the idiom, “Since $\phi$ holds for all $x$ of type $\tau$, it holds in particular
for $e$.”

Finally, we have the existential quantifier. The first proof rule corresponds to the idiom, “To
prove that $\exists(x:\tau)\ldotp\phi$ holds, it suffices to find a witness $e$ such that $\phi(e)$ holds.”

\[
\begin{prooftree}
\Hypo{\Gamma,x:\tau\vdash\phi(x):\Prop}
\Hypo{\Gamma\vdash e:\tau}
\Hypo{\Gamma\mid\Theta\vdash\phi(e)}
\Infer3{\Gamma\mid\Theta\vdash\exists(x:\tau)\ldotp\phi(x)}
\end{prooftree}
\]

The second proof rule corresponds to the idiom, “We know that there exists an $x$ for which
$\phi_1$ holds, and we know that for an arbitrary $x$, if $\phi_1$ holds then so does $\phi_2$, so
it follows that $\phi_2$ also holds.”

\[
\begin{prooftree}
\Hypo{\Gamma\mid\Theta\vdash\exists(x:\tau)\ldotp\phi_1}
\Hypo{\Gamma,x:\tau\mid\Theta,\phi_1\vdash\phi_2}
\Infer[left label={\side{ x\notin\fv(\Theta,\phi_2)}}]2{\Gamma\mid\Theta\vdash\phi_2}
\end{prooftree}
\]

Higher order logic is extremely expressive, and the logic we have presented has considerable
redundancy. In fact, with the higher order proposition type $\Prop$, only implication and
universal quantification are needed. That is, we have the following equivalences:

\begin{align*}
\bot &\quad\iff\quad \forall(\alpha:\Prop)\ldotp \alpha \\
\top &\quad\iff\quad \bot \imp \bot \\
\phi \vee \psi &\quad\iff\quad
\forall(\alpha:\Prop)\ldotp (\phi\imp\alpha) \imp (\psi\imp\alpha) \imp \alpha \\
\phi \wedge \psi &\quad\iff\quad
\forall(\alpha:\Prop)\ldotp (\phi \imp \psi \imp \alpha) \imp \alpha \\
\exists(x:\tau)\ldotp \phi &\quad\iff\quad
\forall(\alpha:\Prop)\ldotp (\forall(x:\tau)\ldotp \phi \imp \alpha) \imp \alpha.
\end{align*}

Even equality can be defined in this way. Given terms $e_1,e_2:\tau$,

\[
e_1 = e_2 \quad\iff\quad \forall(P:\tau\to\Prop)\ldotp P(e_1) \imp P(e_2).
\]

We mention this to give the reader an idea of some of the unexpected consequences of the type
$\Prop$. However, the rules stated in <ref>, before this remark, are easier to work with and—unlike the above higher-order reformulations—trivially generalize to the
non-higher-order setting.

truth judgment|)

§.§.§ The extensionality axioms
propositional extensionality|see extensionality, propositionalextensionality!propositionalfunction extensionality|see extensionality, functionextensionality!function
Propositional extensionality says that equivalent propositions are automatically equal:
$\forall(P,Q:\Prop)\ldotp(P\iff Q)\imp(P=Q)$. This is an axiom that we will assume throughout the
book. It is sound in any Grothendieck topos because propositions correspond externally to closed
sieves (see e.g. <cit.>, which form a partial order, not just
a preorder). Moreover, propositional extensionality is assumed in proof assistants like Coq and Lean.

Function extensionality, like propositional extensionality, is sound in any topos and commonly assumed in proof assistants. It says that two functions $X\to Y$ are equal if and only if their values are equal on all $x:X$.

[Extensionality axioms]

Propositional extensionality

\[
P:\Prop,Q:\Prop\mid P\iff Q\vdash P=Q
\]

Function extensionality
Let $X$ and $Y$ be types. Then

\[
f:X\to Y, g:X\to Y\mid\forall(x:X)\ldotp fx=gx\vdash f=g
\]

Using <ref>, the extensionality axioms can be used in derivations of valid truth judgments. The
specific type signature we give in <ref> will contain ten more axioms, all of which
fit into the logic at the same point as this one. Again, the reason we do not include propositional
extensionality with the other ten is that it is sound in any topos, and is not specific to ours.

Often we will write axioms, propositions, definitions etc. more informally, e.g. replacing the formal syntax of the statements in <ref> with something like the following.

Propositional extensionality Suppose that $P$ and $Q$ are propositions, and assume that $P\iff Q$ holds. Then $P=Q$.

Function extensionality Suppose that $X$ and $Y$ are types and that $f,g:X\to Y$ are functions. If $\forall(x:X)\ldotp fx=gx$ holds, then $f=g$.

§.§ Subtypes and quotient types

Here we add two new type constructors: subtypes and quotient types. We could not have covered these earlier,
when discussing the other type constructors, because these two depend on the logical layer.

Let $\tau$ be a type, and suppose given a predicate in the one-variable context, $x:\tau\vdash
\phi:\Prop$. The corresponding subtype is denoted $\{x:\tau\mid\phi\}$.
[It is natural to want to
extend this idea to contexts with more than one variable, but that takes us into dependent types;
see <ref>.]

There are two term constructors, two conversion rules, and a truth judgment for subtypes. The first
term constructor says that if $\Gamma\vdash e:\tau$ is a term and
$\Gamma\mid\varnothing\vdash\phi(e)$ is a valid truth judgment, then there is a new term
$\Gamma\vdash\textsf{i}(e):\{x:\tau\mid\phi\}$. The second term constructor says that if
$\Gamma\vdash e':\{x:\tau\mid\phi\}$ then there is a new term $\Gamma\vdash \textsf{o}(e'):\tau$.
Then conversion rules say $\textsf{o}(\textsf{i}(e))\equiv e$ and $\textsf{i}(\textsf{o}(e'))\equiv
e'$. However, in practice it is more convenient to simply drop the $\textsf{i}$'s and

The truth judgment for subtypes is that if $\Gamma,x:\tau\mid\Theta(x),\phi(x)\vdash\psi(x)$ is a
valid truth judgment, then so is
$y:\{z:\tau\mid\phi(z)\}\mid\Theta(\textsf{o}(y))\vdash\psi(\textsf{o}(y))$. With the informal
notation drapping $\textsf{i}$'s and $\textsf{o}$'s, this can be simplified to

We saw in <ref> that all of the first-order logic connectives can be defined
in terms of just $\imp$ and $\forall$, by making clever use of the higher-order proposition type
$\Prop$. With the addition of subtypes, this surprising expressivity of higher-order logic extends
to the type theory. For example, the rules for sum types are redundant. The sum of two types $A$
and $B$ can be defined as

\begin{multline}\label{eq:HOL_sum_type}
A+B \quad\coloneqq\quad
\{ (\phi,\psi) : (A\to\Prop)\times(B\to\Prop) \mid \\
(\mathrm{is\_sing}(\phi) \wedge \mathrm{is\_empty}(\psi)) \vee
(\mathrm{is\_empty}(\phi) \wedge \mathrm{is\_sing}(\psi)) \}
\end{multline}

\begin{align*}
\mathrm{is\_sing}(\phi) &\coloneqq \exists(a:A)\ldotp \phi(a) \wedge
\forall(a':A)\ldotp \phi(a') \imp a=a' \\
\mathrm{is\_empty}(\phi) &\coloneqq \forall(a:A)\ldotp \neg\phi(a).
\end{align*}

This can be made precise in two ways. First, if we have explicit sum types in the type theory, then it is
possible to construct an isomorphism between the “real” sum $A+B$ and the type defined in
(<ref>). Second, even without explicit sum types, it is possible to prove that the
type defined in (<ref>) satisfies all of the rules that define a sum type.

Again, it is more convenient to just use the explicit sum type rules. However, there are
properties of sum types which hold in a higher-order logic—and which can be proven from
(<ref>)—which are not provable in non-higher-order logic. We will see an example
of such a property in <ref>, where we show that the sum of two types with decidable equality has decidable equality.

Quotient types.type!quotient
Let $\tau$ be a type, and suppose given a predicate in the two-variable context, also known as a
binary relation, $x:\tau,y:\tau\vdash R(x,y):\Prop$relation!binary. The corresponding quotient type is denoted
[As with subtypes, it is natural to want to extend the above idea to contexts with more
than two variables of the same type, but doing so takes us into dependent types; see

There are two term constructors, two conversion rules, and a truth judgment for quotient types. The
first term constructor says that if $\Gamma\vdash e:\tau$ is a term, then there is a new term
$\Gamma\vdash[e]_R:\tau/R$. We read $[e]_R$ as “the equivalence class of $e$.” The second says
that if $\Gamma,z:\tau\vdash e'(z):\tau'$ is a term and $\Gamma,x:\tau,y:\tau\mid R(x,y)\vdash
e'(x)=e'(y)$ is a valid truth judgment, then there is a new term $\Gamma,a:\tau/R\vdash\textsf{pick
}x\textsf{ from }a\textsf{ in }e'(x):\tau'$. The intuition is that $a$ represents an equivalence
class, so we can pick some representative $x$ from $a$ and form the term $e'(x)$, with the guarantee
that it doesn't matter which representative we choose. The first conversion rule says
$\textsf{pick }x\textsf{ from }[e]_R\textsf{ in }e'(x)\equiv e'(e)$, and the second says
$\textsf{pick }x \textsf{ from }Q\textsf{ in }e'([x]_R)\equiv e'(Q)$.

The truth judgment for quotient types is that if $\Gamma\vdash e:\tau$ and $\Gamma\vdash e':\tau$
are terms, then $\Gamma\mid R(e,e')\vdash [e]_R=[e']_R$ is a valid truth judgment.

type!of integerstype!of rationals
Recall the definition of addition and multiplication of natural numbers from
<ref>. We can also define the inequality $\leq$ for natural numbers,
$m:\tNN,n:\tNN\vdash\const{leq}(m,n)$, to be the term
$\const{leq}(m,n)\coloneqq\exists(p:\tNN)\ldotp n+p=m$. Write $m\leq n$ if $\const{leq}(m,n)$.

With quotient types in hand, we can define the types $\tZZ$ and $\tQQ$. For the former, let $R$ be
the following equivalence relation on $\tNN\times\tNN$,

\[
(p,m):\tNN\times\tNN, (p',m'):\tNN\times\tNN\vdash p+m'=p'+m:\Prop
\]

Then $\tZZ$ is defined to be the type $(\tNN\times\tNN)/R$. One can construct addition,
subtraction, and multiplication for $\tZZ$ using the term constructors for quotient types. For
example, addition in $\tZZ$ is given by the term

\[
z:\tZZ, z':\tZZ\vdash\textsf{pick }(p,m)\textsf{ from }z\textsf{ in }(\textsf{pick
}(p',m')\textsf{ from }z'\textsf{ in }[p+p',m+m']_R:\tZZ.
\]

To construct this term—as mentioned above—one must check that the terms $p+p'$ and $m+m'$ are well-defined, i.e.  independent of the choice of $(p,m)$ and $(p',m')$.

Similarly, for $\tQQ$, let $\tNN_+$ denote the subset type $\tNN_+\coloneqq\{n:\tNN\mid n\geq
1\}$. Then define $S$ be the following equivalence relation on $\tZZ\times\tNN_+$,

\[
(n,d):\tZZ\times\tNN_+, (n',d'):\tZZ\times\tNN_+\vdash d'*n=d*n':\Prop
\]

and let $\tQQ=(\tZZ\times\tNN_+)/S$. Again, one can construct addition, subtraction, and
multiplication for $\tQQ$, as well as the partial reciprocal function, using the term constructors
for quotient types.

§.§ Dependent types

Consider the inequality $x:\tNN, y:\tNN \vdash x\leq y$. Then it is natural to form the subtype
$\tNN_{\leq y}\coloneqq\{x:\tNN \mid x\leq y\}$. However, this type depends on a variable
$y$, which the type theory we have sketched so far is unable to handle. Intuitively, it is best to
think of the type $\{x:\tNN \mid x\leq y\}$ as a family of types, parameterized by $y:\tNN$.
In particular, for each concrete term such as $4:\tNN$ (where $4$ is shorthand for $ssss0$; see page
page:Nats), there is a type $\tNN_{\leq 4}\coloneqq\{x:\tNN \mid x\leq 4\}$ obtained by
substitution $[y\coloneqq 4]$.type!family

While such type families are an intuitively natural and useful concept, formalizing dependent type
theory (where types are allowed to depend on terms) is significantly more subtle than the simple
type theory we have so far described. As an illustration of the extra difficulty, consider the type
families $\{x:\tNN \mid x\leq y\}$ and $\{x:\tNN \mid x\leq (y+0)\}$. We know that $y\equiv y+0$ by
the definition of addition—i.e. we consider $y$ and $y+0$ to be the same term—and as
such we should consider $\tNN_{\leq y}$ and $\tNN_{\leq(y+0)}$ to be the same type, even
though they are syntactically different. Thus in a dependent type theory, one must extend the
conversion relation to types as well as terms.

In the theory presented in the rest of this book, there are a few occasions where we need to
consider subtypes and quotient types which are technically only well-formed in a dependent type
theory, such as $\tNN_{\leq y}$. We trust that it will be intuitively clear how to work with these
types, and we refer the reader interested in the details of dependent type theory to sources such as

Recall the basic idea of the semantics of type theory in a topos $\cat{E}$: each type is
assigned an object of $\cat{E}$, each term is assigned a morphism, and propositions
$a:A\vdash\phi:\Prop$ correspond to subobjects of $A$, i.e. monomorphisms
$\{a:A\mid\phi\}\hookrightarrow A$. The semantics of a dependent type $a:A\vdash B$ is an arbitrary morphism $B\to A$. So one can think of dependent types as
generalizing subtypes: a proposition that is dependent on a context determines a monomorphism into the context, whereas a
type that is dependent on a context determines an arbitrary morphism into the context. For example, the dependent
type $y:\tNN\vdash\tNN_{\leq y}$—which we think of as a family of types parameterized by $y$—is represented by the composite

\[
\{x:\tNN,y:\tNN\mid x\leq y\} \hookrightarrow \tNN\times\tNN \To{\tn{pr}_2} \tNN.
\]

A concrete member of the family, such as $\tNN_{\leq 4}$, is represented by a fiber of this
map, e.g. $\tNN_{\leq 4}$ is represented by the pullback

\[
\begin{tikzcd}
\tNN_{\leq 4} \ar[r] \ar[dd] \ar[ddr,phantom,"\lrcorner"{very near start}]
& \{x:\tNN,y:\tNN\mid x\leq y\} \ar[d] \\
& \tNN\times\tNN \ar[d,"\tn{pr}_2"] \\
1 \ar[r,"4"'] & \tNN
\end{tikzcd}
\]

In general, a helpful intuition is that non-dependent types (with no free variables) are represented
by objects of $\cat{E}$, while dependent types in the context $(x_1:A_1,\dots,x_n:A_n)$ are
represented by objects of the slice category $\cat{E}/(A_1\times\cdots\times A_n)$.

§ MODALITIES

modalitytopos!modality in|see modality

Now that we have informally laid out the basics of the type theory we use in this book, we proceed to discuss some constructions one can do with it. In this section we discuss how modalities allow one to consider subtoposes within the type theory of the larger topos.

A modality is a term of type $\Prop\to\Prop$ satisfying a few axioms. Topos-theoretically, a modality is precisely what <cit.> calls a
Lawvere-Tierney topology and what <cit.> calls a local operator; we
use the term “modality” to emphasize the logical viewpoint.local operator|see
modalitytopology!Lawvere-Tierney|see modality

We define modalities in <ref>, discuss various related notions—such as closed propositions and sheaves—in <ref>, and finally discuss the relationship between modalities and subtoposes in <ref>.

§.§ Definition of modality

In any topos, a modality is an internal monadmonad!on $\Prop$ on $\Prop$, considered as an
internal poset. The definition can be given type-theoretically as follows:

A modality is a map $j:\Prop\to\Prop$ satisfying the following three conditions for any $P,Q:\Prop$,

* $P\imp jP$,

* $jjP\imp jP$, and

* $(P\imp Q)\imp jP\imp jQ$.

The third condition can be replaced by various equivalent statements, as we now show.

Suppose $j:\Prop\to\Prop$ satisfies $P\imp jP$ and $jjP\imp jP$ for any $P:\Prop$. Then the
following are equivalent:

* $(P\imp Q)\imp jP\imp jQ$,

* $jP\imp (P\imp jQ)\imp jQ$,

* $j(P\imp Q)\imp jP\imp jQ$.

* $(jP\wedge jQ)\iff j(P\wedge Q)$.

$2\imp 1$ and $3\imp 1$ are easy. $1\imp 2$ follows from $jjQ\imp jQ$. We next show $1\imp 3$. But 3
is equivalent to $jP\imp j(P\imp Q)\imp jQ$, so first assume $jP$. Assuming 1, we have $(P\imp
Q)\imp jQ$. So if we apply 1 again on this last implication and assume $j(P\imp Q)$ then we have $jjQ$
hence $jQ$.

Next we show $3\imp 4$. It is easy to show
$j(P\wedge Q)\imp jP$ and hence $j(P\wedge Q)\imp(jP\wedge jQ)$. We need to show the converse
$(jP\wedge jQ)\imp j(P\wedge Q)$, which is equivalent to $jP\imp jQ\imp j(P\wedge Q)$. Clearly
$P\imp (Q\imp P\wedge Q)$, so applying $j$ and using 3 with the assumption $jP$ and again with
$jQ$, we obtain $j(P\wedge Q)$ as desired.

Finally for $4\imp 1$, note that $(P\imp Q)$ is equivalent to $(P\wedge Q)\iff P$ and hence to
$(P\wedge Q)=P$ by propositional extensionality, <ref>. Assuming $(P\wedge Q)=P$ and $jP$ we have
$j(P\wedge Q)$ and hence $jQ$ by 4.

modality!order on
Modalities can be ordered by reverse implication, $j\leq j'$ iff $j'P\imp jP$ for
all $P:\Prop$. The top element in this ordering is the identity modality $P\mapsto P$. The bottom
element is the constant modality $P\mapsto\top$. Somewhere in between is the
double-negationmodality!double negation modality $P\mapsto\neg\neg P$. We will discuss the
relationship between modalities and subtoposes in <ref>.
poset!of modalities|seemodalities, order on

§.§ $j$-closed propositions, $j$-separated types, and $j$-sheaves

Given a modality $j$ and a type $X$, we can internally express the semantic notion that the sheaf
associated to $X$ is $j$-separated or a $j$-sheaf.

A proposition $P:\Prop$ is called $j$-closed if it satisfies $jP\imp P$. A predicate
$P:X\to\Prop$ is called $j$-closed if $\forall(x:X)\ldotp jPx\imp Px$.

For any modality $j$, the reflection sending a proposition to a $j$-closed proposition is given by $P\mapsto jP$.

The following remark is straightforward to verify but very useful in practice. We hope the reader takes careful note of it, because we will use it often. Reading a proof and wondering “where did the $j$'s go?” is a sign that the reader should revisit this remark. The goal is to understand how logic in the $j$-subtopos is constructed in the larger topos.

logic!relative to a modality
Let $j$ be a modality. If $P:\Prop$ is written as a complex expression, $jP$ can often be simplified
recursively. For example, we have the following equivalences and implications:

\begin{equation}\label{eqn:j_logic}
\begin{gathered}
\hspace{.7in}
j(\phi\wedge\psi)\Leftrightarrow j\phi\wedge j\psi
\hspace{.7in}
j(\psi\imp\phi)\imp(\psi\imp j\phi)
\\
j\forall(x:X)\ldotp\phi(x)\imp\forall(x:X)\ldotp j\phi(x)
\hspace{.7in}
\exists(x:X)\ldotp j\phi(x)\imp j\exists(x:X)\ldotp\phi(x)
\end{gathered}
\end{equation}

Now assume $\phi$ is $j$-closed. We can replace two of the implications by equivalences:

\begin{gather*}
\hspace{.7in}
\end{gather*}

and, quite usefully, when proving $\phi$ we can drop $j$ from the front of all hypotheses:

\[
[(\psi_1\wedge\cdots\wedge\psi_n)\imp\phi]\iff[(j\psi_1\wedge\cdots\wedge j\psi_n)\imp\phi].
\]

Here is an example of a proof that uses the above remark. We go through it slowly.

Suppose $P:\Prop$ is decidable, i.e. $P\vee\neg P$ holds. For any $Q:\Prop$ we have $j(P\vee Q)\iff P\vee jQ$.

For one direction we suppose $j(P\vee Q)$ and prove $P\vee jQ$. If $P$ holds we are done, so suppose $\neg P$. We will prove $jQ$, so by <ref> we can drop $j$ from the hypothesis, at which point we have $P\vee Q$ and thus $Q$.

The other direction is easier and does not depend on $P$ being decidable. In case $P$, we have $P\vee Q$ so $j(P\vee Q)$. In case $jQ$ we can drop the $j$, and $Q$ implies $P\vee Q$ and hence $j(P\vee Q$).

type!$j$-separatedtype!$j$-sheafsheaf!for a modality $j$|see type, $j$-sheaf
A type $X$ is $j$-separated iff it satisfies $\forall(x,x':X)\ldotp j(x=x')\imp(x=x')$.
The $j$-separification of $X$separification, denoted $\mathrm{sep}_jX$ is the
quotient of $X$ by the internal equivalence relation $j(x=x')$. The $j$-sheafification of
$X$,sheafification denoted $\asSh_j(X)$, is the subtype of predicates $\phi:X\to\Prop$

$j$-closed predicate: $\forall(x:X)\ldotp j\phi(x)\imp\phi(x)$,

$j$-local singleton: $j\exists(x:X)\ldotp\forall(x':X)\ldotp \phi(x')\iff j(x=x').$
If $X$ is separated, one may drop the inner $j$ from the $j$-local singleton condition. If $\{\cdot\}:X\to(X\to\Prop)$ is the usual singleton function, then the $j$-local singleton condition is equivalent to $j\exists(x:X)\ldotp j(\phi=\{x\})$.

There is a map $\eta_j\colon X\to \asSh_j(X)$; it sends $x:X$ to the predicate
$\eta_j(x):X\to\Prop$ given on $x':X$ by

\begin{equation}\label{eqn:sheafification_inclusion}
\eta_j(x)(x')\coloneqq j(x=x').
\end{equation}

It is easy to check that $\eta_j(x)$ is $j$-closed and $j$-locally singleton, and $X$ is
$j$-separated iff $\eta_j$ is an internal injection. $X$ is called a $j$-sheaf if $\eta_j$
is also an internal surjection, i.e. satisfies

A type $X$ is a $j$-sheaf iff it is $j$-separated and, for any $j$-closed predicate
$\phi:X\to\Prop$ the singleton condition on $\phi$ is $j$-closed in the sense that

\begin{equation}\label{eqn:sheaf2}
j\big(\exists(x:X)\ldotp\forall(x':X)\ldotp\phi(x') \iff (x=x')\big)
\imp \exists(x:X)\ldotp\forall(x':X)\ldotp\phi(x') \iff (x=x').
\end{equation}

By <ref>, we may assume $X$ is $j$-separated, and we need to show that
$\eta_j$ is surjective iff <ref> holds for every $j$-closed predicate $\phi$. First
suppose $\eta_j$ is surjective and that $\phi$ is a $j$-closed predicate that satisfies the
hypothesis of implication (<ref>). Then by definition we have $\phi:\asSh_j(X)$, so
$\exists(x:X)\ldotp\phi=\eta_j(x)$, which is the conclusion of (<ref>). For the other
direction, if every $j$-closed predicate $\phi:X\to\Prop$ satisfies (<ref>) then
$\eta_j$ is surjective.

For any modality $j$, the type $\Prop_j\coloneqq\{P:\Prop\mid jP\imp P\}$ is a

It is easy to check that $\Prop_j$ is $j$-separated. So choose a $j$-closed predicate
$\phi:\Prop_j\to\Prop$ and assume the hypothesis of (<ref>). Let
$P\coloneqq\forall(Q:\Prop_j)\ldotp\phi(Q)\imp Q$, which is $j$-closed by <ref>. It
is our candidate for the required existential; i.e. using <ref> we
will be done if we can show $\forall(P':\Prop_j)\ldotp \phi(P')\iff (P=P')$. One checks using
<ref> that $P$ is $j$-closed. Thus we can drop the $j$ from our hypothesis, so we
have some $x:\Prop_j$ satisfying $\forall(x':\Prop_j)\ldotp\phi(x')\iff (x=x')$.

First we show $\phi(P)$. It is easy to show $P\imp x$, because we have $\phi(x)$ by hypothesis.
But we also have $x\imp P$ because for any $Q:\Prop_j$ such that $\phi(Q)$, we have $Q=x$. Thus
$x=P$, so $\phi(P)$, as desired. Choosing $P':\Prop_j$, it remains to show that
$\phi(P')\imp(P=P')$. But given $\phi(P')$ and the already-established $\phi(P)$, we have $P=x=P'$
by hypothesis, so we are done.

Given a $j$-sheaf $X$ and a $j$-closed predicate $\psi:X\to\Prop_j$, the subtype $\{x:X\mid\psi
x\}$ is a $j$-sheaf.

Any subtype of a separated type is separated, so it suffices to prove (<ref>) for any
$\phi:\{x:X\mid\psi x\}\to\Prop_j$. The hypothesis says $j\exists(x:X)\ldotp\psi
x\wedge\forall(x':X)\ldotp\psi x'\imp(\phi x\iff (x=x'))$. It follows easily that
$j\exists(x:X)\ldotp\forall(x':X)\ldotp(\psi x'\wedge\phi x)\iff (x=x')$, and we may drop the $j$
because $X$ is a $j$-sheaf. The conclusion of (<ref>) follows directly.

sheaf!product of
The product of $j$-sheaves is a $j$-sheaf.

We use <ref>. It is easy to see that the product of separated sheaves
is separated. Supposing $j\exists((x_1,x_2):X_1\times X_2)\ldotp\forall((x_1',x_2'):X_1\times
X_2)\ldotp\phi(x_1',x_2')\iff(x_1,x_2)=(x_1,'x_2')$, one proves

\[
\forall(x_1':X_1)(x_2':X_2)\ldotp \phi(x_1',x_2') \iff \phi_1(x_1')\wedge\phi_2(x_2')
\]

by taking $(x_1,x_2)$ from the hypothesis and letting $\phi_i(x_i')\coloneqq(x_i=x_i')$ for
$i=1,2$. We now obtain $j\exists(x_i:X_i)\forall(x_i':X_i)\ldotp\phi_1(x_i')\iff(x_i=x_i')$, and
the result follows from <ref>.

Let $X$ a type. Suppose that $j$ is a modality satisfying

\[\forall(P:X\to\Prop)\ldotp[j\exists(x:X)\ldotp Px]\imp[\exists(x:X)\ldotp jPx].\]

Then the map $\eta_j:X\to\asSh_j(X)$ is surjective.

Suppose $\phi:X\to\Prop_j$ satisfies $j\exists(x:X)\ldotp\forall(x':X)\ldotp\phi(x')\iff(x=x')$.
Then by hypothesis, there is some $x:X$ satisfying $j\forall(x':X)\ldotp\phi(x')\iff(x=x')$, and this implies $\forall(x':X)\ldotp j(\phi(x')\iff(x=x'))$, which in turn implies $\forall(x':X)\ldotp \phi(x')\iff j(x=x')$.

Suppose $X$ has decidable equality. If $j$ is a dense modality (i.e. $j\bot=\bot$) then $X$ is

If $X$ has decidable equality then it is easy to check $j(x_1=x_2)\imp(x_1=x_2)$.

Suppose $X$ decidable equality. Let $j$ be a modality and let $X\to\mathrm{sep}_j(X)$ denote its
$j$-separification. Then the natural map below is an isomorphism:

\[
\]

The map $f:(X\to\Prop_j)\to(\mathrm{sep}_j(X)\to\Prop_j)$, applied to any $P:X\to\Prop_j$ is given
as follows. Any $y:\mathrm{sep}_j(X)$ is represented by some $x:X$, so we may let $f(P)(y)=P(x)$
and it remains to prove that this respects the equivalence relation: $j(x=x')\imp (P(x)=P(x'))$.
$x=x'$ implies $Px\iff Px'$, so it suffices to see that $Px\iff Px'$ is $j$-closed; see

§.§ Modalities and subtoposes

In this section we discuss how the logical notion of modality corresponds to the semantic notion of
subtopos. Much of the following is taken from <cit.>; again, what
we call modalities are called local operators there.modality!order on
topos!subtopos ofsubtopos!corresponding to a modality

There are several equivalent definitions of subtoposes of $\cat{E}$. One is a subcategory $\cat{E}'\ss\cat{E}$ with a left-exact left-adjoint. Another is a modality $j$ on $\cat{E}$, by which one can define the subcategory $\cat{E}_j$ of $j$-sheaves and the left-exact left adjoint $\asSh_j$ defined in <ref>.

As mentioned in <ref>, there is a partial order on modalities: $j\leq j'$ iff
$\forall(P:\Prop)\ldotp j'P\imp jP$. With this partial order, modalities on a topos $\cat{E}$ form a
lattice (in fact a co-Heyting algebra), and there is a poset isomorphism between that of modalities
and that of subtoposes of $\cat{E}$ under inclusion.

To every proposition $U:\Prop$ we can associate three modalities: the open modality
$o(U)$modality!open, the closed modality $c(U)$modality!closed, and the quasi-closed
modality $q(U)$modality!quasi-closed. A topos of sheaves for one of these is respectively called an open subtopos, a closed subtopos, and a quasi-closed subtopos. If $\cat{E}=\Shv{L}$ for some locale $L$, then $U$ can be identified with an open subspace $U\ss L$, and its topos of sheaves is equivalent to $\Shv{L}_{o(U)}$. Similarly, $\Shv{L}_{c(U)}$ is equivalent to the topos of sheaves on the closed subspace complementary to $U$, and $\Shv{L}_{q(U)}$ is equivalent to the topos of sheaves on the localic intersection of all dense subspaces of the complement of $U$. Logically, these modalities are defined as follows:

* $o(U)P \coloneqq U \imp P$,

* $c(U)P \coloneqq U \vee P$,

* $q(U)P \coloneqq (P \imp U) \imp U$.

We say that a modality $j$ is open if there exists $U:\Prop$ such that $j=o(U)$, and
similarly that $j$ is closed or quasi-closed if there exists $U:\Prop$ such that $j=c(U)$ or $j=q(U)$.

In a boolean topos, the closed modality $U\vee P$ is the same as the open modality $\neg U\imp P$,
but not in an arbitrary topos.

Consider the case $U=\bot$, corresponding to the empty subtopos. The associated open modality
$o(U)$ sends $P$ to $\top$, i.e. it is the terminal modality. The associated closed modality
$c(U)$ is the identity, i.e. it is the initial modality.

The most interesting is the associated quasi-closed modality $q(U)$, which in this case is
double-negation, sending $P$ to $\neg\neg P$. It corresponds to a boolean subtopos which is dense
in $\cat{E}$. Semantically, the double-negation modalitymodality!double negation can be
thought of as “almost always”. Every quasi-closed modality $q(U)$ is a double-negation modality, relative to
the closed modality $j=c(U)$, in the sense that $q(U)P=(P\imp j\bot)\imp j\bot$.

As mentioned above, $j_1$ corresponds to a subtopos of $j_2$ iff $j_2(P)\imp j_1(P)$ for all
propositions $P$. For example, it is easy to check that for any proposition $U$, we have
$\forall(P:\Prop)\ldotp c(U)(P)\imp q(U)(P)$. In the lattice of modalities, the join of $j_1$ and
$j_2$ is given by ($j_1(P)\wedge j_2(P)$) of modalities. If terms $c:\tConst$ of a constant sheaf
index modalities $j_c$, then $\forall (c:\tConst)\ldotp j_c$ is a modality, and it corresponds to
their $\tConst$-indexed join.

If $j_1$ and $j_2$ are modalities then it is not necessarily the case that $j_1j_2$ will be a modality. It is easy to prove directly from definitions that $j_1j_2$ is a modality if either $j_1$ is open or $j_2$ is closed. If $j_1j_2$ is a modality then it is the meet of $j_1$ and $j_2$. Modalities $j_1$ and $j_2$ are
called disjointmodality!disjoint if their meet $j$ is the bottom element, i.e. if
$j\bot$ holds.

§ DEDEKIND $J$-NUMERIC TYPES

real number!Dedekind
real number|seealso numeric objectreal numbers|seealso type, of real numbers
object!real numberstype!of real numbers
real numbers|seealso object, real numbers

We continue to work within the type theory discussed in <ref>. Using the notion of modality discussed in <ref>, we define various sorts of numeric objects that exist and are internally definable for any topos $\cat{E}$ and modality $j$.

§.§ Background

From our work in <ref>, and in particular <ref>, we
have seen that the types $\tNN$, $\tZZ$, and $\tQQ$, together with their additive and multiplicative
structures (see <ref>) exist in our type theory. It turns out that,
semantically, the sheaves corresponding to $\tNN$, $\tZZ$, and $\tQQ$ are (locally) constant in any
topos, corresponding to the images of the sets $\NN,\ZZ,\QQ$ under the inverse image part of the
unique geometric morphism $\cat{E}\leftrightarrows\Cat{Set}$.

One manifestation of this constancy is that the $=$ and $<$ relations on $\tNN$, $\tZZ$, or $\tQQ$
are decidable in any topos. Another is that one can get away with blurring the distinction between
internal rational numbers—i.e. terms of the type $\tQQ$ in the internal language—and external
rational numbers; similarly for $\tNN$ and $\tZZ$.

With $\tQQ$ in hand, the standard construction of the type $\tRR$ of real numbers from the rationals by Dedekind cuts can also be
carried out in the type theory with good results. However, unlike $\tNN$, $\tZZ$, and $\tQQ$, one should not expect the type $\tRR$ of real numbers to be semantically constant in an arbitrary topos, and similarly one should expect neither the $=$ nor the $<$ relation to be decidable.
It will turn out that the type $\tRR$ of real numbers is constant in our main topos of interest, $\BaseTopos$, but not in many of the subtoposes we consider. For example the type $\tRR_\pi$ of real numbers in $\BaseTopos_\pi$ does not have decidable equality, roughly because continuous functions that are unequal globally may become equal locally.
In particular one cannot generally regard a section of $\tRR$ as an ordinary real number. Perhaps the best
intuition in an arbitrary topos is that terms of the type $\tRR$ correspond semantically to
continuous real-valued functions on the topos (as a generalized topological space).

In Dedekind's construction of the real numbers <cit.>, a real number $x:\tRR$ is
defined in terms of two subsets of rational numbers: those that are less than $x$ and those that are
greater than $x$. In our context, we replace the external notion, “two subsets of $\QQ$” with the
internal notion, “two subtypes of $\tQQ$”. They are classified by predicates $\delta:\tQQ\to\Prop$
and $\upsilon:\tQQ\to\Prop$, which roughly correspond to the predicates “is less than $x$” and
“is greater than $x$”.
Throughout this book, we use $\delta$ (delta) and $d$ for “down” and $\upsilon$ (upsilon) and
$u$ for “up”. Thus $\delta$ classifies a “down-set” of $\tQQ$, and $\upsilon$ classifies an “up-set”.

These satisfy several axioms: for example for any $q_1<x$, there exists $q_2$ such that $q_1<q_2$ and $q_2<x$. This is translated into the logical statement

\begin{equation}\label{eqn:roundedness_example}
\forall(q_1:\tQQ)\ldotp\delta q_1\imp\exists(q_2:\tQQ)\ldotp (q_1<q_2)\wedge\delta q_2.
\end{equation}

This is one of the usual Dedekind axioms—often called roundedness—which forces $\delta$ to act like $<$ rather than $\leq$. As mentioned above, the Dedekind axioms make sense in any topos $\cat{E}$, giving the standard construction of the type $\tRR$ of real numbers in $\cat{E}$; see e.g. <cit.>.

However, we make two slightly non-standard moves. The first is that we will be interested in several numeric types—not just the real numbers—which are defined by relaxing some of the Dedekind axioms. Doing so in the topos $\Cat{Set}$ would yield a definition of the sets $\LR$, $\UR$, $\II$, $\IR$, and $\RR$, discussed in
<ref>; in this book we will want to consider the analogous objects in other toposes.

The other non-standard move is that we want to work relative to an arbitrary modality $j$, as defined in <ref>. To do so, we take each of the standard Dedekind axioms and apply $j$
“at every position”; the result will be an axiom for the associated numeric type in the $j$-subtopos. For example, the roundedness
axiom (<ref>) becomes

\[
j\forall(q_1:\tQQ)\ldotp j[j\delta q_1\imp j\exists(q_2:\tQQ)\ldotp j(q_1<q_2)\wedge j\delta q_2].
\]

But if $\delta$ is a $j$-closed proposition, then we can use $j$-logic (see <ref>) to find an equivalent statement that is much simpler:

\[
\forall(q_1:\tQQ)\ldotp \delta q_1\imp j\exists(q_2:\tQQ)\ldotp (q_1<q_2)\wedge\delta q_2.
\]

We make similar replacements of all the axioms from <cit.>.

The result of our two non-standard moves is that we obtain what we call the Dedekind $j$-numeric
types, which we now formally define.

§.§ Definition of the Dedekind $j$-numeric types

In the definition below, one can simply remove the $j$'s (i.e. use the identity modality $jP=P$) to obtain the usual notion of Dedekind real numbers, and related numeric types.

numeric type
Dedekind numeric type|see numeric type
Let $\cat{E}$ be a topos, let $\tQQ$ be the type of rational numberstype!rational numbers,
and let $j$ be a modality on $\cat{E}$.modality Consider the following conditions on
predicates $\delta:\tQQ\to\Prop$ and $\upsilon:\tQQ\to\Prop$,

0̄a.  $̄∀(q:)j(δq)δq$\hspace{1.2in}\=
0b.\quad\= $\forall(q:\tQQ)\ldotp j(\upsilon q)\imp\upsilon q$

1a. $\forall q_1,q_2\ldotp (q_1<q_2)\imp\delta q_2\imp\delta q_1$
1b. $\forall q_1,q_2\ldotp(q_1<q_2)\imp\upsilon q_1\imp\upsilon q_2$

2a. $\forall q_1\ldotp\delta q_1\imp j\exists q_2\ldotp (q_1<q_2)\wedge\delta q_2$
2b. $\forall q_2\ldotp\upsilon q_2\imp j\exists q_1\ldotp (q_1<q_2)\wedge\upsilon q_1$

3a. $j\exists q\ldotp\delta q$
3b. $j\exists q\ldotp\upsilon q$

4. $\forall q\ldotp(\delta q \wedge \upsilon q)\imp j\bot$

5. $\forall q_1,q_2\ldotp (q_1<q_2) \imp j(\delta q_1\vee\upsilon q_2)$

We refer to these conditions as $j$-closed (0),cut!$j$-closed down/up-closed (1),
$j$-rounded (2),cut!$j$-rounded $j$-bounded (3)cut!$j$-bounded, $j$-disjoint
(4)cuts!$j$-disjoint, and $j$-located (5)cuts!$j$-located. It is easy to check that
the $j$-disjointness condition is equivalent to $\forall(q_1,q_2:\tQQ)\ldotp\delta
q_1\imp\upsilon q_2\imp j(q_1<q_2)$.

When $j=\id$ is the trivial modality, we refer to the conditions simply as rounded, bounded, etc. In
particular, axioms 0a and 0b can be dropped entirely when $j=\id$.

We define ten real-number-like types, including the usual type of Dedekind real numbers $\tRR_j$
for the subtopos $\cat{E}_j$, by using various subsets of these axioms. We call these
Dedekind $j$-numeric types; see <ref>.numeric type!$j$-local

type!of intervalstype!of lower real numberstype!of improper intervals
type!of upper real numberstype!of real numberstype!of unbounded intervals
type!of unbounded lower real numberstype!of unbounded improper intervals
type!of unbounded upper real numberstype!of unbounded real numbers

\[
\renewcommand{\arraystretch}{1.45}
\begin{array}{l|l|l}
\text{Name of type in }\cat{E}&\text{Notation}&\text{Definition}\\\hline
\text{$j$-local unbounded lower reals}&\tLRub_j&\{\delta\mid\text{0a, 1a, 2a}\}\\
\text{$j$-local unbounded upper reals}&\tURub_j&\{\upsilon\mid\text{0b, 1b, 2b}\}\\
\text{$j$-local unbounded improper intervals}&\tIIub_j&\{(\delta,\upsilon)\mid\text{0, 1, 2}\}\\
\text{$j$-local unbounded (proper) intervals}&\tIRub_j&\{(\delta,\upsilon)\mid\text{0, 1, 2, 4}\}\\
\text{$j$-local unbounded reals}&\tRRub_j&\{(\delta,\upsilon)\mid\text{0, 1, 2, 4, 5}\}\\
\text{$j$-local lower reals}&\tLR_j&\{\delta\mid\text{0a, 1a, 2a, 3a}\}\\
\text{$j$-local upper reals}&\tUR_j&\{\upsilon\mid\text{0b, 1b, 2b, 3b}\}\\
\text{$j$-local improper intervals}&\tII_j&\{(\delta,\upsilon)\mid\text{0, 1, 2, 3}\}\\
\text{$j$-local (proper) intervals}&\tIR_j&\{(\delta,\upsilon)\mid\text{0, 1, 2, 3, 4}\}\\
\text{$j$-local real numbers}&\tRR_j&\{(\delta,\upsilon)\mid\text{0, 1, 2, 3, 4, 5}\}
\end{array}
\]

Ten Dedekind $j$-numeric types

We refer to those having only one cut ($\tLR_j$, $\tUR_j$, $\tLRub_j$, and $\tURub_j$) as
one-sided and to those having both cuts ($\tRR_j$, $\tIR_j$, $\tII_j$, $\tRRub_j$,
$\tIRub_j$, and $\tIIub_j$) as two-sided. We refer to those without the locatedness axiom
($\tLR_j$, $\tUR_j$, $\tLRub_j$, $\tURub_j$, $\tIR_j$, $\tII_j$, $\tIRub_j$, and $\tIIub_j$) as
the $j$-numeric domains, a name that will be justified in
<ref>.numeric type!one-sidednumeric
type!two-sidednumeric type!domainnumeric domain|see numeric type, domain

Given unbounded reals $r=(\delta,\upsilon):\tRRub_j$ and $r'=(\delta',\upsilon'):\tRRub_j$, we often
use the more familiar notation for inequalities between them or involving a rational $q:\tQQ$:inequality!$j$-local

\begin{align*}
q<r&\coloneqq\delta q&
r<q&\coloneqq\upsilon q&
r<_jr'&\coloneqq j\exists(q:\tQQ)\ldotp (r<q)\wedge(q<r')\\
r\leq_j q&\coloneqq\delta q\imp j\bot&
q\leq_j r&\coloneqq\upsilon q\imp j\bot&
r'\leq_j r&\coloneqq(r<_jr')\imp j\bot
\end{align*}

The same notation makes sense when $r,r':\tRR_j$ are (bounded) reals, but one should be a bit careful with other $j$-numeric types. We will discuss this more in <ref>.

We associate to any $q:\tQQ$ a pair of cuts $(\delta_q,\upsilon_q)$, defined as follows on

\begin{equation}\label{eqn:q_cuts}
\delta_q q'\iff j(q<q')
\qquad\text{and}\qquad
\upsilon_q q'\iff j(q'<q).
\end{equation}

It is easy to check that $(\delta_q,\upsilon_q)$ is a $j$-local real number, so we have a map
$\tQQ\to\tRR_j$. In particular, for $r=(\delta_r,\upsilon_r):\tRR_j$, we write $q=r$ to mean
$\forall(q':\tQQ)\ldotp (\delta_q q' \iff \delta_r q') \wedge (\upsilon_q q' \iff \upsilon_r q')$.

There are also obvious isomorphisms $\tII_j\cong\tLR_j\times\tUR_j$ and $\tIIub_j \cong \tLRub_j
\times \tURub_j$. Here is a diagram of relationships among the Dedekind $j$-numeric types:

\begin{equation}\label{eqn:relations_among_Dedekinds}
\begin{tikzcd}[column sep=15pt, row sep = 5pt]
\tQQ\ar[rr,hook]&&\tRR_j\ar[dd, hook]\ar[rr, hook]&&
\tIR_j\ar[dd, hook]\ar[rr, hook]&&
\tII_j\ar[dd, hook]\ar[dl, two heads]\ar[dr, two heads]
\\
\tUR_j
\\
\tRRub_j\ar[rr, hook]&&
\tIRub_j\ar[rr, hook]&&
\tIIub_j\ar[dl, two heads]\ar[dr, two heads]
\\
&\tLRub_j\ar[from=uu, hook, crossing over]&&
\tURub_j\ar[from=uu, hook, crossing over]
\end{tikzcd}
\end{equation}

separated!$j$-numeric types as
Each of the Dedekind $j$-numeric types, $\tRR_j$, $\tIR_j$, $\tII_j$, $\tLR_j$, $\tUR_j$,
$\tRRub_j$, $\tIRub_j$, $\tIIub_j$, $\tLRub_j$, and $\tURub_j$ is a $j$-sheaf. Proving this requires function extensionality; see <ref>.extensionality!function

§.§ Some preliminary numerical facts

Most of the material in this section is taken from <cit.>. The results here will mainly be used in the next
section, to show that addition and multiplication preserve locatedness; see
<ref>. Throughout the section, $j$ is an arbitrary modality.

Archimedean property

\[\forall(q_1,q_2:\tQQ)\ldotp(q_1>0\wedge q_2>0)\imp\exists(k:\tNN)\ldotp q_2<k*q_1.\]

We may assume $q_1=\frac{a+1}{m+1}$ and $q_2=\frac{b+1}{n+1}$ for $a,b,m,n\in\tNN$. Then we can set $k\coloneqq(m+1)*(b+1)$.

For any $n:\tNN$, rationals $q_0<q_1<\cdots<q_{n+2}$, and real $r:\tRR_j$, we have

\[
q_0<r<q_{n+2}\imp j\exists(k:\tNN)\ldotp (0\leq k\leq n) \wedge (q_k<r<q_{k+2}).
\]

We proceed by induction on $n$. The claim is trivial for $n=0$, so suppose it is true for arbitrary $n$. Suppose further that there are rationals $q_0<q_1<\cdots<q_{n+3}$ and $q_0<r<q_{n+3}$. By locatedness, $j(q_{n+1}<r\vee r<q_{n+2})$; we can drop the $j$ by <ref>,
[Throughout this section, we will use <ref> without mentioning it.]
to obtain $q_{n+1}<r\vee r<q_{n+2}$. In the first case we have $q_{n+1}<r<q_{n+3}$ and in the second we use the inductive hypothesis.

The next two propositions say that any real number can be bounded between rationals that are arbitrarily close together, in the additive and the multiplicative sense.

Any $r:\tRR_j$ is $j$-arithmetically located in the sense that

\[
\forall(p:\tQQ)\ldotp p>0\imp j\exists(d,u:\tQQ)\ldotp(d<r<u)\wedge(0<u-d<p).
\]

By boundedness, $j\exists(d',u':\tQQ)\ldotp d'<r<u'$, and by the Archimedean property (<ref>), $\exists(k:\tNN)\ldotp u'-d'<k*\frac{p}{3}$. For each $i:\tNN$, let $q_i\coloneqq d'+i*\frac{p}{3}$, so $d'=q_0<q_1<\cdots<q_{k+2}$ and $u'<q_k<q_{k+2}$. By <ref>, there is some $i$ with $0\leq i\leq k$ with $q_i<r<q_{i+2}$. The conclusion is satisfied using $d\coloneqq q_i$ and $u\coloneqq q_{i+2}$, because $u-d=\frac{2p}{3}<p$.

Any $r:\tRR_j$ with $0<r$ is $j$-multiplicatively located in the sense that

\[
\forall(p,p':\tQQ)\ldotp 0<p<p'\imp j\exists(d,u:\tQQ)\ldotp
\]

By roundedness $j\exists(q:\tQQ)\ldotp 0<q<r$. Choose $q':\tQQ$ such that $0<q'<q(p'-p)$. By
arithmetic locatedness, $j\exists(d,u:\tQQ)\ldotp(d<r<u)\wedge(0<u-d<\frac{q'}{p'})$. Then $q<u$
by disjointness, so $p'(u-d)<q'<q(p'-p)<u(p'-p)$, hence $up<p'd$ and $\frac{u}{d}<\frac{p'}{p}$.

The standard definition of addition of unbounded improper
intervalsarithmetic!additionfunction!arithmetic|see arithmetic, relativized to the $j$-modality, is given by
$(\delta_1,\upsilon_1)+(\delta_2,\upsilon_2)=(\delta',\upsilon')$, where

\begin{equation}\label{eqn:addition_unbounded_improper}
\begin{aligned}
\delta'q&\iff j\exists(q_1,q_2:\tQQ)\ldotp\delta_1q_1\wedge\delta_2q_2\wedge(q<q_1+q_2)\\
\upsilon'q&\iff j\exists(q_1,q_2:\tQQ)\ldotp\upsilon_1 q_1\wedge\upsilon_2 q_2\wedge(q_1+q_2<q).
\end{aligned}
\end{equation}

monoid!numeric objects as
The type $\tIIub_j$ has the structure of a commutative monoid, with the addition operation $+$ from <ref>. Each of the types in <ref> is closed under this operation, and each of the maps shown there is a monoid homomorphism.

We begin by working only with lower cuts; upper cuts are similar. It is easy to see that $+$ is commutative and associative. For example the lower cut for both sides of $r_1+(r_2+r_3)=(r_1+r_2)+r_3$ will be equivalent to

\[j\exists(q_1,q_2,q_3:\tQQ)\ldotp\delta_1q_1\wedge\delta_2q_2\wedge\delta_3q_3\wedge(q<q_1+q_2+q_3).
\]

The additive unit is $0:\tQQ$; indeed it suffices to check the following equivalence for any lower cut $\delta$ and rational $q$:

\[
\delta q\iff j\exists (q_1,q_2:\tQQ)\ldotp q_1<0\wedge \delta q_2\wedge(q<q_1+q_2).
\]

For the backwards direction, the existential is equivalent to $\exists(q_2:\tQQ)\ldotp \delta q_2\wedge(q<q_2)$, so we obtain $\delta q$ by down-closure (1a) and $j$-closure (0a). For the forwards direction, suppose $\delta q$. Then by roundedness (2a) twice, $\exists(q',q'':\tQQ)\ldotp(q<q'<q'')\wedge\delta q''$, and the conclusion is satisfied by letting $q_1\coloneq q'-q''$ and $q_2\coloneqq q''$.

Thus $\tIIub_j$ has the structure of a commutative monoid. It is straightforward to check that if $\delta_1$ and $\delta_2$ are bounded (3a) then so is their sum, so the operation restricts to one on $\tII_j$, which then also has the structure of a commutative monoid.

For $j$-disjointness (4) and $j$-locatedness (5), we consider both lower and upper cuts. If $r_1$ and $r_2$ are $j$-disjoint then we want to see that $(\delta',\upsilon')=r_1+r_2$ is too. Suppose $\delta'q\wedge\upsilon'q$; we want to show $j\bot$. From

\[
\]

one obtains $q_1'+q_2'<q_1+q_2$ and by Trichotomy of rationals, $(q_1'<q_1)\vee(q_2'<q_2)$. Either way, we obtain $j\bot$ from down/up closure and disjointness.

Suppose $r_1,r_2:\tRR_j$; we need to show $r_1+r_2$ is $j$-located, so take $q<q'$ and let $p\coloneqq\frac{q'-q}{2}$. By <ref>, we can find rationals $q_1<r_1<q_1'$ and $q_2<r_2<q_2'$ such that $(q_1'-q_1)<p$ and $(q_2'-q_2)<p$. It is easy to check that $q_1+q_2<r_1+r_2<q_1'+q_2'$. Either $q<q_1+q_2$ or $q\geq q_1+q_2$; in the first case we get $q<r_1+r_2$ and in the second case we can get $r_1+r_2<q'$, as desired.

group, real numbers as
The monoid structure on $\tRR_j$ is in fact that of a group.

Take any $(\delta_1,\upsilon_1):\tRR_j$ and define cuts $\delta_2,\upsilon_2$ on $q:\tQQ$ by

\[
\delta_2q\iff\upsilon_1(-q)
\qquad\text{and}\qquad
\upsilon_2q\iff\delta_1(-q).
\]

It is easy to check that $(\delta_2,\upsilon_2)$ is a $j$-local real. Let $(\delta',\upsilon')\coloneqq(\delta_1,\upsilon)+(\delta_2,\upsilon_2)$ be their sum, as in <ref>. We want to show $\delta'q\iff j(q<0)$ and $\upsilon'q\iff j(0<q)$. Consider the latter, the former being similar; we must check

\[j(0<q)\iff j\exists(q_1,q_2:\tQQ)\ldotp\upsilon_1q_1\wedge\delta_1(-q_2)\wedge(q_1+q_2<q).\]

The forward direction is <ref>; the backwards direction comes down to the fact that $(\delta_1,\upsilon_1)$ is $j$-disjoint.

§.§ Numeric domains

In <ref> we referred to eight of the $j$-numeric types as $j$-numeric domains. In this section, specifically <ref>, we show that they actually are domains
internal to $\cat{E}$.

In fact, these eight domains correspond to the
eight predomains we defined in <ref>. Though the subject of predomains is a bit technical, its value to us it that predomains
provide a very useful tool for defining arithmetic operations between numeric types.numeric
type!as $j$-rounded ideals

Again, the eight predomains from <ref> can be defined internally to any topos.
Write $\tLRpre$, $\tURpre$, $\tIIpre$, $\tIRpre[j]$, $\tLRubpre$, $\tURubpre$, $\tIIubpre$, and
$\tIRubpre[j]$ to denote the corresponding internal constructions in any topos $\cat{E}$ and
modality $j$. For example $\tLRpre$ is just the rationals with the usual $<$ ordering: $\tLRpre=(\tQQ,<)$. Because our type theory has sum types (see <ref>) we can also make sense of the unbounded predomains, such as  $\tLRubpre=(\tQQ+\{\infty\},<)$.

Recall the $j$-local rounded ideal construction from <ref>.

Let $\cat{E}$ be a topos, and let $j$ be a modality on $\cat{E}$. Then we have
isomorphismsnumeric type!domain

\begin{align*}
\tLR_j&\cong\RId_j(\tLRpre)&
\tUR_j&\cong\RId_j(\tURpre)&
\tII_j&\cong\RId_j(\tIIpre)&
\tIR_j&\cong\RId_j(\tIRpre[j])\\
\tLRub_j&\cong\RId_j(\tLRubpre)&
\tURub_j&\cong\RId_j(\tURubpre)&
\tIIub_j&\cong\RId_j(\tIIubpre)&
\tIRub_j&\cong\RId_j(\tIRubpre[j])
\end{align*}

Thus each $j$-numeric domain in the sense of <ref> is in fact an internal domain—and in
particular an internal topological space—in the subtopos
$\cat{E}_j$.internal!domainnumeric type!domain

Consider the four conditions in the definition of $j$-rounded ideal found in
<ref>; below we will refer to them 0', 1', 2', 3'. They match exactly with
the $j$-closed, up/down-closed, $j$-roundedness, and $j$-boundedness conditions of
<ref>. The first two isomorphisms are hence direct. <Ref> is
easily modified to the context of a modality $j$, showing that

\begin{equation}\label{eqn:rounded_ideal_product_Q}
\RId_j(\tIIpre) = \RId_j(\tLRpre\times\tURpre) \cong \RId_j(\tLRpre)\times\RId_j(\tURpre)
\cong \tLR\times\tUR \cong \tII,
\end{equation}

giving the third isomorphism. It is not quite as automatic, but still easy to see that we have the
fourth isomorphism $\tIR_j\cong\RId_j(\tIRpre[j])$, because a rounded ideal $I\ss\tIIpre$ is
contained in $\tIRpre[j]$ iff $(q,q')\in I\imp j(q<q')$ iff $\delta q\imp\upsilon q'\imp j(q<q')$
iff $I$ is $j$-disjoint.

The bottom row is more interesting; we consider only the case for unbounded lower reals, the
others being similar. We want to obtain the isomorphism

\[
\{\delta':\tQQ\sqcup\{-\infty\}\to\Prop\mid\text{0', 1', 2', 3'}\}
\cong
\{\delta:\tQQ\to\Prop\mid\text{0a, 1a, 2a}\}
\]

because the left-hand side is $\RId_j(\tLRubpre)$ and the right-hand side is $\tLRub$.

Given $\delta'$ on the left, define $\delta q\coloneqq\delta' q$; it is easy to check that it
satisfies 0a, 1a, 2a. Conversely, given $\delta$ on the right, define $\delta' q'$ to be $\delta
q'$ if $q'\in\tQQ$ and $\top$ if $q'=-\infty$. Recall from <ref> that we defined
the order relation so that $-\infty<-\infty$. With that in mind, the conditions 0', 1', 2', 3' are

The second statement follows directly from <ref>.

Domains have two useful relations, $\sqss$ and $\ll$; see <ref>. Thus by <ref>, these
symbols make sense for each of the eight $j$-numeric domains.

way-below!for numeric types
specialization order!for numeric types
Suppose that $\delta,\delta':\tLR_j$ or $\delta,\delta':\tLRub_j$. And suppose that
$\upsilon,\upsilon':\tUR_j$ or $\upsilon,\upsilon':\tURub_j$. Then

\begin{align*}
\delta'\sqss\delta&\iff\forall(q:\tQQ)\ldotp\delta' q\imp\delta q&
\delta'\ll\delta&\iff j\exists(q:\tQQ)\ldotp\delta q\wedge(\delta'q\imp j\bot)\\
\upsilon'\sqss\upsilon&\iff\forall(q:\tQQ)\ldotp\upsilon' q\imp\upsilon q&
\upsilon'\ll\upsilon&\iff j\exists(q:\tQQ)\ldotp\upsilon q\wedge(\upsilon'q'\imp j\bot)
\end{align*}

For $(\delta,\upsilon)$ and $(\delta',\upsilon')$ in $\tII_j$, $\tIIub_j$, $\tIR_j$, or
$\tIRub_j$, we have

\[
\quad\text{and}\quad
\]

Consider the $\delta$ case; the rest are similar. The statement for $\sqss$ is basically just the definition of these domains, and comes directly from
<ref>. The statement about $\ll$ will also follow from <ref>.
Indeed, it says

\[
\delta'\ll\delta \iff
j\exists(q:\tQQ)\ldotp\delta q\wedge\forall(q':\tQQ)\ldotp\delta'q'\imp j(q'<q),
\]

and the right-hand side is equivalent to $j\exists(q:\tQQ)\ldotp\delta q\wedge(\delta'q\imp
j\bot)$ by trichotomy for rationals, $(q<q')\vee(q=q')\vee(q>q')$.trichotomy

Rather than define Dedekind $j$-numeric types as predicates on $\tQQ$, as we did in
<ref>, one could also define them as predicates on $\asSh_j\tQQ$, the
$j$-sheafification of rationals. However, it turns out that doing so makes no difference:
semantically, it defines the same topos of sheaves.

Indeed, it is enough by <ref> to check semantically that
$j$-separification agrees with $j$-sheafification,
$\mathrm{sep}_j\mathcal{Q}\cong\asSh_j\mathcal{Q}$, for the constant type $\mathcal{Q}$ on any set
$Q$. So suppose given a $j$-covering family $\{V_i\to V\}_{i\in I}$ and sections
$q_i\in\mathcal{Q}(V_i)$ such that $j(q_i=q_{i'})$ for $i,i'\in I$. For each $i$, we may assume
each $q_i\in Q$, so it has an extension $\ol{q_i}\in\mathcal{Q}(V)$. We want to show
$j(\ol{q_i}=\ol{q_{i'}})$. We have $(\ol{q_i}=\ol{q_{i'}})\vee\neg(\ol{q_i}=\ol{q_{i'}})$, so we
may assume $\neg(\ol{q_i}=\ol{q_{i'}})$ from which we obtain $\neg(q_i=q_{i'})$ and hence $j\bot$,
which proves the result.

Before concluding this section, we record a lemma that will become useful in <ref>, when we discuss differentiability.

Let $x,y:\tII_j$ be $j$-improper intervals such that $x\sqss y$. If $x$ is $j$-located and $y$ is
$j$-disjoint, then $x=y$.

Write $x=(\delta_x,\upsilon_x)$ and $y=(\delta_y,\upsilon_y)$. For all $q:\tQQ$ we have $\delta_x
q\imp\delta_yq$ and $\upsilon_xq\imp\upsilon_yq$, so it suffices to show $\delta_y q\imp\delta_xq$
for any $q:\tQQ$ (the $\upsilon$ case is similar). Since $\delta_x$ is $j$-closed, we may drop $j$
from the front of all hypotheses by <ref>.

Assuming $\delta_yq$, we have $\exists q'\ldotp q<q'\wedge\delta_yq'$ by $j$-roundedness. Since
$x$ is $j$-located we have $\delta_xq\vee\upsilon_xq'$. In the first case we are done; in the
second case we have $\upsilon_yq'$ which is a contradiction because $y$ is $j$-disjoint.

§.§ Inequalities

In this section we will discuss inequalities for Dedekind $j$-numeric objects, and in <ref> we discuss their arithmetic. We learned some of this from <cit.> and <cit.>, which in particular discuss the order-theoretic and algebraic properties of the extended interval domain $\tII$.

The proofs in the remainder of this chapter,  <ref>,
will depend heavily on the work on predomainspredomain discussed
in <ref>, however the results can usually be stated without it. We write $\tQQ$ to
denote the type of rational numbers, together with the usual $<$ ordering, and we write $\tQQ\op$
for the opposite ordering. Both of these are predomains, and we will often consider the predomain

We defined inequalities for reals in <ref>. We can easily generalize the definition to $j$-local improper intervals. Given two
$j$-local unbounded improper intervals $x_1,x_2:\tIIub_j$, we define $x_1<_jx_2$ by

\begin{equation}\label{eqn:j_less_than}
x_1<_jx_2\iff j\exists(q:\tQQ)\ldotp (x_1<q)\wedge(q<x_2),
\end{equation}

where as usual $x_1<q$ and $q<x_2$ respectively mean $\upsilon_1 q$ and $\delta_2 q$, for
[In <ref> we gave the warning that one should be a bit careful with the $<$ relation on other numeric types. As an example of what can violate standard intuition, let $x=(\delta,\upsilon):\tII$ be given by $\delta q\iff q<1$ and $\upsilon q\iff -1<q$. Then $x<x$ holds.

For the one-sided numeric types, e.g. $\tLR$, there is a good notion of $\leq$, namely $\forall(q:\tQQ)\ldotp\delta q\imp\delta'q$. To obtain $<$ one might try $(\delta\leq\delta')\wedge(\delta\neq\delta')$, but this is semantically too strong in a general topos.]
The same definition also works for the other two-sided $j$-numeric
types $\tIRub_j$, $\tRRub_j$, $\tII_j$, $\tIR_j$, and $\tRR_j$.

inequality!as open subset
For any modality $j$, the set $\{(x_1,x_2)\mid x_1<_j x_2\}\ss\tIIub_j\times\tIIub_j$ is an open
subset. The same is true when $\tIIub_j$ is replaced by any of the other two-sided $j$-numeric

The other two-sided $j$-numeric types are subspaces of $\tIIub_j$, so it suffices to check that
one. Begin by defining an open of the predomain $\tIIubpre\times\tIIubpre$ by

\[
U_<\coloneqq\{(d_1,u_1),(d_2,u_2)\mid u_1<d_2\}\in\Opens(\tIIubpre\times\tIIubpre).
\]

This is easily seen to be an open in the sense of <ref>: it is
up-closed (decreasing $u_1$ and increasing $d_2$ stays in the set) and rounded (if $u_1<d_2$, then
we can easily find $d'_1,u'_2,d'_2,u'_2$ with $d'_1<d_1$, $u_1<u'_1$, $d'_2<d_2$, $u_2<u'_2$, and
still $u'_1<d'_2$).

By <ref>, this determines a Scott open subset of
$\RId_j(\tIIubpre\times\tIIubpre)$ given by $\U_{U_<}=\{I\mid\exists(d_1,u_1,d_2,u_2)\in I\ldotp
u_1<d_2\}$. Under the isomorphism $\tIIub_j\times\tIIub_j\cong\RId_j(\tIIubpre\times\tIIubpre)$
from <ref>, this is equivalent to

\[
\Bigl\{\bigl((\delta_1,\upsilon_1),(\delta_2,\upsilon_2)\bigr) \Bigm|
j\exists(d_1,u_1,d_2,u_2)\ldotp \delta_1 d_1 \wedge
\upsilon_1 u_1 \wedge \delta_2 d_2 \wedge \upsilon_2 u_2 \wedge u_1 < d_2\Bigr\},
\]

or more simply $\{(\delta_1,\upsilon_1),(\delta_2,\upsilon_2)\mid j\exists q\ldotp \upsilon_1 q
\wedge \delta_2 q\}$, for which <ref> is shorthand. In the language of
<ref>, $(x_1<_jx_2)$ iff $(x_1,x_2)\models_jU_<$.

We now move on to discussing the non-strict inequality, $\leq_j$.

The following are equivalent for all $a,b:\tRR_j$:

* $(b <_j a)\imp j\bot$

* $\forall(q:\tQQ)\ldotp q<a\imp q<b$

* $\forall(q:\tQQ)\ldotp b<q\imp a<q$

This is proven for an arbitrary topos in <cit.>, so it easily
applies to the $j$-subtopos. However it is also straightforward, so we we show the proof for
$1\imp 2$; the other implications are similarly easy.

Write $a=(\delta_a,\upsilon_a)$ and $b=(\delta_b,\upsilon_b)$. To prove $1\imp 2$, assume $(b <_j
a)\imp j\bot$, and choose $q$ such that $\delta_aq$. It suffices to prove $j\delta_b q$ because
$\delta_bq$ is $j$-closed; thus we may drop $j$ from the front of all hypotheses. By
$j$-roundedness, we have $j\exists q'\ldotp q<q'\wedge\delta_aq'$, so (dropping $j$) we choose
such a $q'$ and, by $j$-locatedness, we have $\upsilon_b q'\vee\delta_b q$. In one case we are
done; in the other we have $\delta_aq'\wedge\upsilon_bq'$, meaning $b<_ja$, and we obtain $j\bot$
by assumption.

Suppose $a,b:\tRR_j$ are $j$-local reals. We write

\begin{equation}\label{eqn:def_leq}\index{inequality!non-strict}
\end{equation}

iff any of the equivalent conditions of <ref>, e.g. $(b<_ja)\imp
j\bot$, is satisfied.

It is easy to check that the relation $\leq_j$ on $\tRR_j$ is reflexive, transitive, and
anti-symmetric, $(a\leq_jb)\wedge(b\leq_ja)\imp a=b$. It is also easy to check that
$(a<_jb)\imp(a\leq_jb)$, as well as the following facts:

\begin{gather*}
(a<_jb)\wedge(b\leq_jc)\imp (a<_jc)\qquad\text{and}\qquad
(a\leq_jb)\wedge(b<_jc)\imp (a<_jc).
\end{gather*}

As mentioned above, <ref> is about $j$-local reals, not $j$-local
improper intervals.

The above story also works for unbounded reals and one-sided numeric types. For $a,b:\tRRub_j$ one
can define $a\leq_j b$ to be any of the following equivalent conditions

* $(b <_j a)\imp j\bot$

* $\forall(q:\tQQ\cup\{-\infty\})\ldotp q<_ja\imp q<_jb$

* $\forall(q:\tQQ\cup\{\infty\})\ldotp b<_jq\imp a<_jq$

For $a,b:\tLR$ or $a,b:\tLRub$, only condition 2 is defined, and so we define $a\leq_j b$ as
condition 2; this agrees with the domain order on $\tLR$ and $\tLRub$. For $a,b:\tUR$ or
$a,b:\tURub$, only condition 3 is defined, and so we define $b\geq_ja$ as condition 3; this agrees
with the domain order on $\tUR$ and $\tURub$.

§.§ $j$-constant numeric types
numeric type!$j$-constant

The present section (<ref>) is non-standard material, regarding what we call constant numeric types. The technical underpinnings of these ideas is given in <ref>.

Let $j$ be a modality. Say that $\phi:\tQQ\to\Prop$ is $j$-decidable if it satisfies

\[
\forall(q:\tQQ)\ldotp\phi q\vee (\phi q\imp j\bot).
\]

Let $\ctLR_j$ denote the subtype of $\tLR_j$ consisting of those $\delta$ that are $j$-decidable,
and similarly define $\ctUR_j$, $\ctIR_j$, $\ctII_j$, $\ctRR_j$ $\ctLRub_j$, $\ctURub_j$,
$\ctIRub_j$, $\ctIIub_j$, and $\ctRRub_j$. We refer to these as the $j$-constant numeric

Note that $\ctII_j=\ctLR_j\times\ctUR_j$ and $\ctIIub_j=\ctLRub_j\times\ctURub_j$.

domain!basis of
For each of the eight $j$-numeric domains (see <ref>), the constant types form a basis in the sense of
<ref>; indeed, this follows from
<ref>. This fact implies, for example, that for any

\[
(x\ll y)\iff\exists(c:\ctII_j)\ldotp x\ll c\ll y
\quad\text{and}\quad
x\sqss y\iff\forall(c:\ctII_j)\ldotp(c\ll x)\imp(c\sqss y)
\]

and similarly when $\tII$ is replaced with any of the other $j$-numeric domains.

For any $j$ there are internal bijections

\[
\ctLRub_j\cong\ctRRub_j\cong\ctURub_j.
\]

For the first claim, consider the functions $\ctRRub_j\to\ctLRub_j$ and $\ctRRub_j\to\ctURub_j$
given by sending $(\delta,\upsilon)$ to $\delta$ and $\upsilon$ respectively. In the first case,
the inverse sends $\delta$ to $(\delta,\upsilon)$ where for any $q:\tQQ$,

\begin{equation}\label{eqn:upsilon_from_delta}
\upsilon q\iff j\exists(q':\tQQ)\ldotp(q'<q)\wedge(\delta q\imp j\bot)
\end{equation}

It is easy to check that $\upsilon$ is $j$-closed, up-closed, and $j$-rounded, and that the pair
$(\delta,\upsilon)$ is $j$-disjoint and $j$-located. To see that $\upsilon$ is $j$-decidable, we
proceed as in <ref>. Take $q:\tQQ$ and consider the constant
type $\tQQ_{<q}=\{q':\tQQ\mid q'<q\}$. We have $\forall(q':\tQQ_{<q})\ldotp(\delta q'\imp
j\bot)\vee\delta q'$, so $\forall(q':\tQQ_{<q})\ldotp\exists(q'':\tQQ_{<q})\ldotp(\delta q''\imp
j\bot)\vee\delta q'$, and thus $\upsilon q\vee\forall(q':\tQQ_{<q})\ldotp\delta q'$ by
<ref>. It is easy to show that $\forall(q':\tQQ_{<q})\ldotp\delta q'$ implies
$\upsilon q\imp j\bot$, so $\upsilon$ is indeed $j$-constant. Finally, to see that the two
functions are mutually inverse, one takes $(\delta,\upsilon):\ctRRub_j$ and shows using
$j$-locatedness that <ref> holds for any $q:\tQQ$.

There are internal bijections

\[
\ctIIub_j\cong\ctRRub_j\times\ctRRub_j
\qquad\text{and}\qquad
\ctIRub_j\cong\{(d,u)\in\ctRRub_j\times\ctRRub_j\mid d\leq_j u\}
\]

We obtain the left-hand isomorphism from <ref> and the isomorphisms
$\ctIIub_j\cong\ctLRub_j\times\ctURub_j$ and $\ctII_j\cong\ctLR_j\times\ctUR_j$. Using the
left-hand isomorphism, we will also have the right-hand isomorphism if we can show that for any
$d,u:\tRRub$ we have $[\forall q\ldotp ((q<d\wedge u<q)\imp j\bot)]\iff d\leq_j u$. The left-hand
side is constructively equivalent to $(\exists q\ldotp q<d\wedge u<q)\imp j\bot$ and the
right-hand side is by definition $(u<_jd)\imp j\bot$, so it suffices to show $u<_jd\iff
j\exists(q:\tQQ)\ldotp q<d\wedge u<q$, but that is the definition (<ref>).

For $d,u:\ctRRub_j$, we may write $[d,u]:\ctIIub_j$ to denote the constant interval
$(\delta,\upsilon):\ctIIub_j$ given by

\[
\delta q\iff j(q<d)
\qquad\text{and}\qquad
\upsilon q\iff j(u<q)
\]

Thus we have $[-,-]:\ctRRub_j\times\ctRRub_j\to\ctIIub_j$.

Recall from <ref> that $\tIIubpre=\tQQ\times\tQQ$ with $(q_1,q_2)\prec
(q_1',q_2')\iff (q_1<q_1')\wedge(q_2'<q_2)$. Composing $[-,-]$ with the square of the map
$i:\tQQ\to\tRRub_j$, one obtains $[i,i]:\tIIubpre\to\tIIub_j$ which sends $(q,q')$ to $[q,q']$; it
is the usual inclusion $\downclose$ of the predomain into its associated domain (see

Let $f:X\to Y$ be a function. One might say it is $j$-injective if it satisfies
$\forall(x,x':X)\ldotp f(x)=f(x')\imp j(x=x')$, but for <ref> we want a
stronger notion. So say that $f$ is a strongly $j$-injective if it satisfies

\begin{equation}\label{eqn:strongly_j_injective}
\forall(x,x':X)\ldotp f(x)=f(x')\imp (x=x')\vee j\bot.
\end{equation}

There are functions

\[
\ctRR_j\sqcup\{\infty\}\to\ctLR_j
\qquad\text{and}\qquad
\tRR_j\sqcup\{-\infty\}\to\ctUR_j.
\]

which are internally surjective and strongly $j$-injective.

The map $\ctRR_j\sqcup\{\infty\}\to\ctLR_j$ sends $(\delta,\upsilon):\ctRR_j$ to $\delta$, and
sends $\infty$ to the unique predicate $\delta$ satisfying $\forall q\ldotp\delta q$. We will show
it is an internal surjection and a $j$-injection, the claim for $\ctUR_j$ being similar. Take
$\delta:\ctLR_j$ and define $\upsilon$ as in <ref>, and the pair
$(\delta,\upsilon)$ is in $\ctRR_j$ iff $\upsilon$ is $j$-bounded. We already have shown that
$\forall q\ldotp\upsilon q\vee (\upsilon q\imp j\bot)$ and again follows from
<ref> that $(\exists q\ldotp\upsilon q)\vee\forall
q\ldotp(\upsilon q\imp j\bot)$. One can prove that the second case is equivalent to $\forall
q\ldotp\delta q$, and so our function is indeed surjective.

To see that the map is strongly $j$-injective, take $x,x':\ctRR_j\sqcup\{\infty\}$. We need only
consider two of the four cases, namely when $x,x':\ctRR_j$, and when $x:\ctRR_j$ and $x'=\infty$.
For the former we need to show that if both $x=(\delta,\upsilon)$ and $x'=(\delta,\upsilon')$ are
in $\ctRR_j$ then $(\upsilon=\upsilon')\vee j\bot$. So take $q:\tQQ$; we want to show $\upsilon
q\iff\upsilon'q$. Because $\upsilon$ and $\upsilon'$ are constant, it suffices to consider the
case $\upsilon q\wedge(\upsilon'q\imp j\bot)$. We obtain $j\bot$ by $j$-roundedness of $\upsilon$,
$j$-disjointness of $(\delta,\upsilon)$ and $j$-locatedness of $(\delta,\upsilon')$.

Finally, suppose $x=(\delta,\upsilon):\ctRR_j$ and $x'=\infty$. It suffices to show that if
$\delta q$ holds for all $q$ then $j\bot$. We get this because $\upsilon$ is $j$-bounded and
$(\delta,\upsilon)$ is $j$-disjoint.

numeric type!domain
For any $j$, the subtype of $j$-constant elements of any $j$-numeric domain is again a domain, namely
the domain of constant rounded ideals on the associated predomain:

\begin{align*}
\ctLR_j  &\cong\cRId_j(\tLRpre)  &
\ctUR_j  &\cong\cRId_j(\tURpre)  &
\ctII_j  &\cong\cRId_j(\tIIpre)  &
\ctIR_j  &\cong\cRId_j(\tIRpre[j])  \\
\ctLRub_j&\cong\cRId_j(\tLRubpre)&
\ctURub_j&\cong\cRId_j(\tURubpre)&
\ctIIub_j&\cong\cRId_j(\tIIubpre)&
\ctIRub_j&\cong\cRId_j(\tIRubpre[j])
\end{align*}

This is just a matter of seeing that
<ref> are equivalent.

§.§ Arithmetic

The usual arithmetic operations on the usual set $\II$ of extended intervals are well-known (see
<cit.> and <cit.>, who calls them “modal intervals”). For example
addition is straightforward, $(a_1,b_1)+(a_2,b_2)=(a_1+a_2,b_1+b_2)$, whereas multiplication
involves multiple cases depending on signs. It turns out that disjoint intervals and located
disjoint intervals—i.e. real numbers—are each closed under these

Here we discuss the internal $j$-local arithmetic for an arbitrary modality $j$. Our main task is to
understand when 2-variable functions in $\tIIpre\coloneqq(\tQQ\times\tQQ\op)$ give rise to
continuous 2-variable functions on $\tII$. For elements $b_1=(q_1,q_1')$ and $b_2=(q_2,q_2')$ in
$\tQQ\times\tQQ\op$ we write $b_1\prec b_2$ to mean $q_1<q_2$ and $q_2'<q_1'$. We write $b_1\specord b_2$
to mean $q_1\leq q_2$ and $q_2'\leq q_1'$. This notation is aligned with that in

<Ref> is a bit technical, but it paves the way for the $j$-arithmetic, from <ref> through the end of the chapter.

arithmetic!via approximable mappingapproximable mapping
Let $f\colon \tIIpre\times \tIIpre\to \tIIpre$ be a function satisfying the following four

\begin{equation}\label{eqn:four_conditions_approximable}
\begin{aligned}
(b_1'\prec b_1)\imp f(b_1',b_2)\specord f(b_1,b_2)&\quad&
(c\prec f(b_1,b_2))\imp\exists b_1'\ldotp(b_1'\prec b_1)\wedge(c\prec f(b_1',b_2))\\
(b_2'\prec b_2)\imp f(b_1,b_2')\specord f(b_1,b_2)&\quad&
(c\prec f(b_1,b_2))\imp\exists b_2'\ldotp(b_2'\prec b_2)\wedge(c\prec f(b_1,b_2'))
\end{aligned}
\end{equation}

Then $f$ determines an approximable mapping $f^*\colon \tIIpre\times \tIIpre\to \tIIpre$, given by
$f^*(b_1,b_2,b')\iff f(b_1,b_2)<b'$. In turn, $f^*$ determines a continuous morphism of domains

\[
\]

for any modality $j$, and this morphism preserves constants.

Exactly the same statements are true for the other $j$-numeric domains, i.e. when the predomain
$\tIIpre$ is replaced by $\tLRpre$, $\tURpre$, $\tIRpre[j]$, $\tLRubpre$, $\tURubpre$,
$\tIIubpre$, or $\tIRubpre[j]$, and the domain $\tII_j$ is replaced by the corresponding domain of
$j$-rounded ideals, $\tLR_j$, $\tUR_j$, $\tIR_j$, $\tLRub_j$, $\tURub_j$, $\tIIub_j$, or

Both $\tQQ$ and $\tQQ\op$ are linear and unbounded, so the predomain $\tQQ\times\tQQ\op$ is
rounded and has binary joins given by $(\max,\min)$. The four conditions are exactly those
required by <ref>, so have an approximable mapping $f^*\colon
\tIIpre\times \tIIpre\to \tIIpre$. It is decidable (in the sense of
<ref>) because the $<$-relation on $\tQQ$ is decidable.

By <ref>, we obtain a morphism of
domainsdomain!morphism of

\[
\RId_j(f^*)\colon\RId_j(\tIIpre)\times\RId_j(\tIIpre)\to\RId_j(\tIIpre),
\]

or simply $\tII_j\times\tII_j\to\tII_j$, since by definition $\RId_j(\tIIpre)=\tII_j$. This map
preserves constants by <ref>.

For any $f\colon\tIIpre\times\tIIpre\to\tIIpre$, we write $\ubar{f}$ and $\bar{f}$ for its first and
second projections via the isomorphism $\tIIpre\to\tLRpre\times\tURpre$. Then the continuous map
$F_j$ from <ref> is given by the formula
$F_j\big((\delta_1,\upsilon_1),(\delta_2,\upsilon_2)\big)\coloneqq(\delta',\upsilon')$ where

\begin{equation}
\label{dia:two_var}
\begin{aligned}
\delta'd' &\Leftrightarrow j\exists(d_1,d_2,u_1,u_2:\tQQ)\ldotp
\Big[ \delta_1d_1 \wedge \delta_2d_2 \wedge \upsilon_1u_1 \wedge \upsilon_2u_2
\wedge \Big(d' < \ubar{f}\big( (d_1,u_1), (d_2,u_2) \big) \Big) \Big] \\
\upsilon'u' &\Leftrightarrow j\exists(d_1,d_2,u_1,u_2:\tQQ)\ldotp
\Big[ \delta_1d_1 \wedge \delta_2d_2 \wedge \upsilon_1u_1 \wedge \upsilon_2u_2
\wedge \Big( \bar{f}\big( (d_1,u_1), (d_2,u_2) \big) < u' \Big) \Big]
\end{aligned}
\end{equation}

Indeed, this follows directly from <ref>.

We include one more technical lemma here, even though it will not be used again until <ref>. The reader can feel free to skip to <ref>.

Let $\phi_1,\phi_2,\phi_3:\Prop$ be such that $(\phi_1\vee\phi_2)\imp\phi_3$, and let $j_1$,
$j_2$, and $j_3$ be the corresponding closed modalities. Let
$f:\tIIpre\times\tIIpre\to\tIIpre$ be a function satisfying the four conditions <ref> and the following “density” condition:

\[\forall(c:\tIIpre)\ldotp\exists(b_1,b_2:\tIIpre)\ldotp c\prec f(b_1,b_2).\]

Then there is an induced continuous function
$F_{j_1,j_2,j_3}:\tII_{j_1}\times\tII_{j_2}\to\tII_{j_3}$ and it preserves constants.

This follows from <ref>.

§.§.§ Addition
As mentioned above, the usual addition of improper intervals is defined coordinate-wise,
$(d_1,u_1)+(d_2,u_2)=(d_1+d_2,u_1+u_2)$, where $d_1,u_1,d_2,u_2:\tQQ$ are rational numbers.

arithmetic!as continuous
For any modality $j$, addition defines a continuous function
$+_j\colon\tII_j\times\tII_j\to\tII_j$, which preserves constants. The formula for addition
reduces to $(\delta_1,\upsilon_1)+(\delta_2,\upsilon_2)=(\delta',\upsilon')$, where

\begin{equation}\label{eqn:addition}
\begin{aligned}
\delta'q &\Leftrightarrow j\exists(q_1,q_2:\tQQ)\ldotp
\delta_1q_1 \wedge \delta_2q_2 \wedge (q<q_1+q_2) \\
\upsilon'q &\Leftrightarrow j\exists(q_1,q_2:\tQQ)\ldotp
\upsilon_1q_1 \wedge \upsilon_2q_2 \wedge (q_1+q_2<q)
\end{aligned}
\end{equation}

A similar statement holds when $\tII_j$ is replaced with any of the other Dedekind $j$-numeric

Working in the predomain $\tLRpre=(\tQQ,<)$, it is clear that if $q_1<q_2$ then $q_1+q'\leq
q_2+q'$ and $q'+q_1\leq q'+q_2$ for any $q'$. It is also clear that if $q'<q_1+q_2$ then there
exists some $q_1'<q_1$ such that $q'<q_1'+q_2$ and similarly for $q_2$. Thus the conditions of
<ref> are satisfied, and this defines an addition operation for
eight of the ten Dedekind $j$-numeric types. It is easy to see that <ref> agrees
with <ref>.

It remains to check that if $x_1$ and $x_2$ are $j$-located, then so is their sum. So choose
rationals $d<u$; we want to show $j((d<x_1+x_2)\vee(x_1+x_2<u))$. By the arithmetic locatedness of
$x_1$ (<ref>), we have

\[
\]

Then $d-d_1<u-u_1$ so there exists $d_2, u_2$ such that $d-d_1<d_2<u_2<u-u_1$, and hence
$d<d_1+d_2$ and $u_1+u_2<u$. By locatedness of $x_2$, we have $j(d_2<x_2\vee x_2<u_2)$, hence

\begin{multline*}
j[(\exists(d_1,d_2:\tQQ)\ldotp (d_1<x_1) \wedge (d_2<x_2) \wedge (d<d_1+d_2)) \vee {} \\
(\exists(u_1,u_2:\tQQ)\ldotp (x_1<u_1) \wedge (x_2<u_2) \wedge (u_1+u_2<u))]
\qedhere
\end{multline*}

§.§.§ Subtraction

In <ref> we defined approximable mappings for the difference, the max,
and the product of two improper intervals. The formula for subtraction reduces to
$(\delta_1,\upsilon_1)-_j(\delta_2,\upsilon_2)=(\delta',\upsilon')$, where

\begin{equation}\label{eqn:subtraction}\index{arithmetic!subtraction}
\begin{aligned}
\delta'q&\iff j\exists(d,u:\tQQ)\ldotp\delta_1d\wedge\upsilon_2u\wedge(q<d-u)\\
\upsilon'q&\iff j\exists(d,u:\tQQ)\ldotp\upsilon_1u\wedge\delta_1d\wedge(u-d<q).
\end{aligned}
\end{equation}

Note that this notion of subtraction extends the classical one for the set $\IR$ of proper
intervals, where one thinks of $[d,u]$ as representing the set $\{x\mid d\leq x\leq u\}$. Then the
difference is given by

\[
\]

which is the set of all pairwise differences. However, note that $\IR$ does not form a
group, and neither does $\tIR$! Subtraction is defined but is not inverse to addition.

Often the classical extended interval domain $\II$ is used to correct this problem, embedding
$\IR$ into something that does form a group, where for example additive inverse of $[d,u]$ is
$[-d,-u]$, sending proper intervals to improper intervals. However this operation is not
constructively well-behaved; there does not seem to be an analogous operation on $\tII$ in a
topos. Thus we use the definition given in <ref>, as it is the most convenient
for us, and simply supply the above warning. Note that subtraction is inverse to addition for
real numbers: $(\tRR_j,+_j,0)$ forms an abelian group for any $j$, as shown in

§.§.§ Maximum

The formula for the max function given in <ref> reduces to
$\max\!_j((\delta_1,\upsilon_1),(\delta_2,\upsilon_2))=(\delta',\upsilon')$, where

\begin{equation}\label{eqn:maximization}\index{arithmetic!max function}
\begin{aligned}
\delta'q &\iff j\exists(q_1,q_2:\tQQ)\ldotp
\delta_1q_1 \wedge \delta_2q_2 \wedge (q<\max(q_1,q_2)) \\
\upsilon'q &\iff j\exists(q_1,q_2:\tQQ)\ldotp
\upsilon_1q_1 \wedge \upsilon_2q_2 \wedge (\max(q_1,q_2)<q).
\end{aligned}
\end{equation}

However, we can do better.

We have the following equivalences:

\[
q<\max\!_j(x_1,x_2)\iff j(q<x_1\vee q<x_2)
\qquad\text{and}\qquad
\max\!_j(x_1,x_2)<q\iff x_1<q\wedge x_2<q
\]

Begin with the first statement. For the converse direction, suppose $q<x_1$, the case $q<x_2$
being similar. Then by roundedness $j\exists q_1\ldotp q<q_1<x_1$, so for any $q_2<x_2$ we have
$q<\max(q_1,q_2)$. For the forwards direction, suppose $q<\max\!_j(x_1,x_2)$ in the sense of
<ref>. Then there exists $q_1,q_2$ with $q_1<x_1$ and $q_2<x_2$ and
$q<\max(q_1,q_2)$. Then either $q<q_1$ or $q<q_2$, and we are done. The second statement is
similarly straightforward, but uses that $j(P\wedge Q)=jP\wedge jQ$.

§.§.§ Multiplication

The formula for multiplication is more involved, but again it comes directly from
<ref>. It is given by
$(\delta_1,\upsilon_1)*_j(\delta_2,\upsilon_2)=(\delta',\upsilon')$, where

\begin{equation}\label{eqn:multiplication}\index{arithmetic!multiplication}
\begin{aligned}
\begin{split}
\delta'q \iff j\exists(d_1,d_2,u_1,u_2:\tQQ)\ldotp
\delta_1d_1 \wedge \delta_2d_2 \wedge \upsilon_1u_1 \wedge \upsilon_2u_2 \wedge \hspace{1.2in}\\
q<\max(d_1^+ d_2^+,u_1^- u_2^-)-\max(u_1^+ d_2^-, u_2^+ d_1^-) \\
\end{split}\\
\begin{split}
\upsilon'q \iff j\exists(d_1,d_2,u_1,u_2:\tQQ)\ldotp
\delta_1d_1 \wedge \delta_2d_2 \wedge \upsilon_1u_1 \wedge \upsilon_2u_2 \wedge \hspace{1.2in}\\
\max(u_1^+ u_2^+,d_1^- d_2^-)-\max(d_1^+ u_2^-, u_1^-d_2^+)<q
\end{split}
\end{aligned}
\end{equation}

where $q^+=\max(q,0)$ and $q^-=\max(-q,0)$ for any $q:\tQQ$. It may be helpful to note that $q=q^+

The following lemma—which simplifies the above multiplication formula in the case of positive
proper intervals—is straightforward to prove.

Suppose $(\delta_1,\upsilon_1)$ and $(\delta_2,\upsilon_2)$ are each $j$-disjoint. If they are also positive, i.e.  $\delta_10$ and $\delta_20$, then their product is $(\delta_1,\upsilon_1)*_j(\delta_2,\upsilon_2)
= (\delta',\upsilon')$ where

\begin{align*}
\delta'q &\iff j\exists(d_1,d_2:\tQQ)\ldotp
\delta_1d_1 \wedge \delta_2d_2 \wedge (q<d_1*d_2) \wedge (0<d_1)\wedge (0<d_2) \\
\upsilon'q &\iff j\exists(u_1,u_2:\tQQ)\ldotp \upsilon_1u_1\wedge\upsilon_2u_2\wedge (u_1*u_2<q)
\end{align*}

arithmetic!as continuous
For any modality $j$, multiplication defines a continuous function
$*_j\colon\tII_j\times\tII_j\to\tII_j$, which preserves constants. A similar statement holds when
$\tII_j$ is replaced with any of the other two-sided $j$-numeric types, $\tIR_j$, $\tRR_j$,
$\tIIub_j$, $\tIRub_j$, or $\tRRub_j$.

The first statement follows from <ref> and from
<ref>, where it is shown that all of the functions whose composite is
<ref> are approximable mappings between predomains, e.g. $(q\mapsto
q^+):\tIIpre\to\tIIpre$. The statements for $\tIR_j$, $\tIIub_j$, and $\tIRub_j$ follow similarly,
replacing $\tIIpre$ with $\tIRpre[j]$, $\tIIubpre$, and $\tIRubpre[j]$ respectively. It remains to
prove the result for $\tRR_j$ and $\tRRub_j$. For this it suffices to show that if
$x_1,x_2:\tRRub_j$ are located then so is $y\coloneqq x_1*_jx_2$. Take any rationals $d<u$.

As a first step, we prove $j(d<y\vee y<u)$ under two preliminary assumptions: that $0<x_1$ and
that $0<d$. By the multiplicative locatedness of $x_1$ (<ref>)

\[
j\exists(d_1,u_1:\tQQ)\ldotp 0<d_1<x_1<u_1\wedge\left(\frac{u_1}{d_1}<\frac{u}{d}\right).
\]

Choose $q, q':\tQQ$ such that $u_1d<q<q'<ud_1$ and define $d_2\coloneqq\frac{q}{d_1u_1}$ and
$u_2\coloneqq\frac{q'}{d_1u_1}$. So $d<d_1d_2$, $d_2<u_2$, and $u_1u_2<u$, and by locatedness of
$x_2$, we have $j(d_2<x_2\vee x_2<u_2)$. Hence,

\begin{multline*}
\end{multline*}

giving $j(d<y\vee y<u)$ as desired.

As a second step we retain the assumption $0<x_1$, but we drop the second assumption and consider
general $d<u$. Either $d<0$ or $0<u$. If $0<u$ then there exists $d'$ with $\max(0,d)<d'<u$, so
$j(d'<y\vee y<u)$ by the first step, and hence $j(d<y\vee y<u)$. If $d<0$ then $-u<-d$ and, just
as before, there exists $d'$ with $\max(0,-u)<d'<-d$, so $j(d'<-y\vee -y<-d)$ by the first step,
so $j(d<y\vee y<u)$.

Finally, dropping all preliminary assumptions, take any located $x_1$ and $x_2$; we will show
$d<y\vee y<u$ for $y\coloneqq x_1*_jx_2$. Let $m\coloneqq\max(-d,u)$, so since $d<0\vee 0<u$ we
have $0<m$, and hence by locatedness we have

\[
(-1<x_1\vee x_1<0)\wedge(0<x_1\vee x_1<1)\wedge(-m<x_2\vee x_2<0)\wedge(0<x_2\vee x_2<m).
\]

This implies $(x_1<0)\vee(0<x_1)\vee(x_2<0)\vee (0<x_2)\vee(|x_1|<1\wedge|x_2|<m)$. The first four
cases are covered by the second step, above. In the last case $-1<x_1<1$ implies $-|x_2|<y<|x_2|$,
and $|x_2|<m$ implies $|x_2|<-d\vee |x_2|<u$, hence $(d<-|x_2|<y)\vee(y<|x_2|<u)$.

§.§.§ Division

Division is just multiplication by a reciprocal. We next define a reciprocal function $r\mapsto 1/r$ for positive $j$-local reals $r>0$. It is easily extended to a reciprocal for negative $j$-reals $r<0$ by $r\mapsto -(1/(-r))$.

Consider the
predomain $(\tQQ^{>0},<)$, its opposite $(\tQQ^{>0},>)$, and the product $(\tII^{>0})_{\tn{pre}}$.
There is a function $\tIIpre^{>0}\to\tIIpre^{>0}$ sending $(d,u)$ to $(1/u,1/d)$, and it induces an
approximable mapping by <ref>. Thus for any
$(\delta,\upsilon):\tII^{>0}_j$, define the reciprocal to be $(\delta',\upsilon'):\tII^{>0}_j$,
where for a positive rational $q>0$ we put

\begin{equation}\label{eqn:reciprocal}\index{arithmetic!reciprocal}
\delta'q\iff j\exists(u:\tQQ)\ldotp \upsilon u\wedge(q*u<1)
\qquad\text{and}\qquad
\upsilon'q\iff j\exists(d:\tQQ)\ldotp\delta d\wedge(1<q*d)
\end{equation}

$(0<q<1/x)\iff x<1/q$, for any $x:\tII_j$ and $q:\tQQ$.

Since $x$ is $j$-closed, it suffices to show $j(x<1/q)$. By definition, $(0<q<1/x)\iff
j\exists(u:\tQQ)\ldotp(x<u)\wedge (q*u<1)$, and we finish with a chain of equivalences

\[
j\exists(u:\tQQ)\ldotp(x<u)\wedge (q*u<1)
\quad\iff\quad
j\exists(u:\tQQ)\ldotp(x<u)\wedge (u<1/q)
\quad\iff\quad
\]

If $x:\tII^{>0}_j$ is $j$-disjoint then $1/x$ is $j$-disjoint; and if $x$ is $j$-located then
$1/x$ is $j$-located. Moreover, for any positive real $r:\tRR_j^{>0}$ we have $r*r'=1$, where
$r'\coloneqq(\delta',\upsilon')$ is as in <ref>.

Let $(\delta',\upsilon')$ be the reciprocal of $x$. For $j$-disjointness, suppose $0<q$ and
$\delta'q\wedge\upsilon' q$. Then $j\exists d,u\ldotp\delta d\wedge\upsilon u\wedge q*u<1<q*d$,
and we obtain $j\bot$. For $j$-locatedness, suppose $q_1<q_2$. Then $1/q_2<1/q_1$, so
$\delta(1/q_2)\vee\upsilon(1/q_1)$, and the result follows by <ref>.

For the final claim, $1:\tRR_j$ is the $j$-local real represented by $1:\tQQ$; see
<ref>. We first show that if $x$ is $j$-disjoint then $q<x*(1/x)\imp q<1$:

\begin{align}
&\iff j\exists q_1,q_2\ldotp(0<q_1<x)\wedge(0<q_2<1/x)\wedge(q<q_1*q_2)\\\label{eqn:equiv_recip}
&\iff j\exists q_1,q_2\ldotp(0<q_1<x)\wedge(x<1/q_2)\wedge (q<q_1*q_2)\\\nonumber
&\imp j\exists q_1,q_2\ldotp(0<q_1<1/q_2)\wedge q<q_1*q_2\\\nonumber
&\iff j(q<1)
\end{align}

The first equivalence is <ref>, the second is
<ref>, the implication is by $j$-disjointness, and the fourth is an
easy calculation. It remains to prove that if $r:\tRR_j$ is real then $q<1\imp q<x*(1/x)$; assume
$q<1$. By <ref>, we have

\[
j\exists q_1,q_2\ldotp(0<q_1<r<q_2)\wedge(q<q_1/q_2),
\]

which is equivalent to (<ref>) when $x\coloneqq r$, so we obtain $q<r*(1/r)$.

One must be careful to note that for numeric types other than $\tRR$, the distributive law does not
hold. For example, if $x=[0,1]$, $y=[1,1]$, and $z=[-1,-1]$, then

\begin{align*}
=[0,1]*([1,1] + [-1, -1])
&= [0,0]\\
&\neq [-1,1]
\end{align*}

However, it is well-known that the real numbers form a commutative ring in any topos.

real numbers!field of
The type $\tRR_j$ of $j$-local real numbers forms a commutative ring satisfying the additional

\begin{equation}\label{eqn:j-field}
\forall(r:\tRR_j)\ldotp \big(j(r<0\vee r>0)\iff j\exists(r':\tRR_j)\ldotp r*_jr'=1\big).
\end{equation}

In any topos, including the subtopos $\cat{E}_j$, the Dedekind real numbers object $R$ forms a
residue field, in particular a commutative ring $(R,0,+,1,*)$ satisfying $\forall(r:R)\ldotp
(r<0\vee r>0)\iff\exists(r':R)\ldotp r*r'=1$. A constructive proof can be found in

For any morphism of modalities $j'\imp j$, there is an induced continuous map

\begin{align*}
\end{align*}

defined by sending $(\delta,\upsilon)$ to $(j\delta,j\upsilon)$, and it preserves constants, arithmetic, and inequalities. The analogous statement holds for each of the other nine Dedekind numeric types.

The continuity of the above-defined $j$ follows from <ref>. More explicitly, one can check that each of the $j'$-axioms for $\delta$ (or $\upsilon$) immediately implies the corresponding $j$-axiom for $j\delta$ (or $j\upsilon$). The map is continuous because it is the restriction of a morphism of domains.

The fact that $j$ preserves constants follows from <ref>. The fact that it preserves arithmetic follows from <ref>, because all arithmetic operations are induced by approximable mappings. For inequalities, suppose $a<_{j'}b$ in the sense of <ref>, i.e. $j'\exists q\ldotp\upsilon_aq\wedge\delta_bq$. This implies $j\exists q\ldotp j\upsilon_aq\wedge j\delta_bq$, as desired.

type theory|(