# Domain theory in univalent foundations II: Continuous and algebraic domains

Tom de Jong  and  Martín Hötzel Escardó  School of Computer Science,
University of Birmingham, Birmingham, UK<EMAIL_ADDRESS><EMAIL_ADDRESS>https://www.tdejong.com
_and_https://www.cs.bham.ac.uk/~mhe

###### Abstract.

We develop the theory of continuous and algebraic domains in constructive and
predicative univalent foundations, building upon our earlier work on basic
domain theory in this setting. That we work predicatively means that we do not
assume Voevodsky’s propositional resizing axioms. Our work is constructive in
the sense that we do not rely on excluded middle or the axiom of (countable)
choice. To deal with size issues and give a predicatively suitable definition
of continuity of a dcpo, we follow Johnstone and Joyal’s work on continuous
categories. Adhering to the univalent perspective, we explicitly distinguish
between data and property. To ensure that being continuous is a property of a
dcpo, we turn to the propositional truncation, although we explain that some
care is needed to avoid needing the axiom of choice. We also adapt the notion
of a domain-theoretic basis to the predicative setting by imposing suitable
smallness conditions, analogous to the categorical concept of an accessible
category. All our running examples of continuous dcpos are then actually
examples of dcpos with small bases which we show to be well behaved
predicatively. In particular, such dcpos are exactly those presented by small
ideals. As an application of the theory, we show that Scott’s $D_{\infty}$
model of the untyped $\lambda$-calculus is an example of an algebraic dcpo
with a small basis. Our work is formalised in the Agda proof assistant and its
ability to infer universe levels has been invaluable for our purposes.

###### Key words and phrases:

constructivity, predicativity, univalent foundations, homotopy type theory,
HoTT/UF, propositional resizing, domain theory, continuous domain, algebraic
domain

##  1\. Introduction

In previous work [dJon21a, dJon24] we developed domain theory in constructive
and predicative univalent foundations and considered basic applications in the
semantics of programming languages, such as the Scott model of PCF [Plo77,
Sco93]. However, we did not discuss a rich and deep topic in domain theory:
_algebraic_ and _continuous_ dcpos [Gie+03]. We present a treatment of the
basic theory and examples in our constructive and predicative approach, where
we deal with size issues by taking direct inspiration from category theory and
the work of Johnstone and Joyal on continuous categories [JJ82] in particular.

Classically, a dcpo $D$ is said to be _continuous_ if for every element $x$ of
$D$ the set of elements _way below_ it is directed and has supremum $x$. The
problem with this definition in our foundational setup is that the type of
elements way below $x$ is not necessarily small. Although this does not stop
us from asking it to be directed and having supremum $x$, this still poses a
problem: for example, there would be no guarantee that its supremum is
preserved by a Scott continuous function, as it is only required to preserve
suprema of directed families indexed by small types.

Our solution is to use the ind-completion to give a predicatively suitable
definition of continuity of a dcpo, following the category theoretic work by
[JJ82] [JJ82]. Some care is needed to ensure that the resulting definition
expresses a property of a dcpo, rather than an equipment with additional
structure. This is of course where the propositional truncation comes in
useful, but there are two natural ways of using the truncation. We show that
one of them yields a well behaved notion that serves as our definition of
continuity, while the other, which we call _pseudocontinuity_ , is problematic
in a constructive context. In a classical setting where the axiom of choice is
assumed, the two notions (continuity and pseudocontinuity) are equivalent.

Another approach is to turn to the notion of a _basis_ [AJ94, Section 2.2.2],
but to include smallness conditions. While we cannot expect the type of
elements way below an element $x$ to be small, in many examples it is the case
that the type of basis elements way below $x$ is small. We show that if a dcpo
has a small basis, then it is continuous. In fact, all our running examples of
continuous dcpos are actually examples of dcpos with small bases. Moreover,
dcpos with small bases are better behaved. For example, they are locally small
and so are their exponentials. Furthermore, we show that having a small basis
is equivalent to being presented by ideals. For algebraic dcpos, bases work
especially well constructively, at least in the presence of set quotients and
univalence, as explained in Section 5.3. In particular, we show that Scott’s
$D_{\infty}$, as originally conceived in [Sco72], and ported to predicative
univalent foundations in [dJon24], is algebraic and that it has a small
compact basis.

Finally, we pause to mention two other domain-theoretic aspects in this work
that require particular attention when working constructively. Firstly, it is
well-known that the are several inequivalent notions of a finite subset in
constructive mathematics and to characterise the compact elements of a
powerset we need to use the _Kuratowski_ finite subsets. Secondly, _single
step function_ are classically defined by a case distinction (using excluded
middle) on the ordering of elements. Constructively, we cannot, in general,
make this case distinction, so we use subsingleton suprema to define single
step functions instead.

###  1.1. Prerequisites

This is the second part of two papers on domain theory in univalent
foundations. Part I [dJon24] develops the concepts of dcpos, lifting, Scott
continuous maps and exponentials, among others. We also rely on some examples,
such as the dcpo of propositions, the powerset as a dcpo, and Scott’s
$D_{\infty}$, all of which we show to be algebraic dcpos in this paper. Part I
further develops the material and notation for univalent foundations needed
here. In particular, we write $\equiv$ for definitional equality, reserving
$=$ for identity types. We will give explicit references to appropriate
sections, definitions, examples and theorems in Part I when we invoke them
here, so it is advisable to have Part I available for reference.

###  1.2. Related work

For a general discussion of related work on (constructive and predicative)
domain theory, we refer to the related work section of Part I.

Our treatment of continuous (and algebraic) dcpos is based on the work of
[JJ82] [JJ82] which is situated in category theory where attention must be
paid to size issues even in an impredicative setting. In the categorical
context, a smallness criterion similar to our notion of having a small basis
appears in [JJ82, Proposition 2.16]. In contrast to Johnstone and Joyal
[JJ82], we use the propositional truncation to ensure that the type of
continuous dcpos is a subtype of the type of dcpos. This, together with the
related notion of pseudocontinuity, is discussed in Section 4.2. The
particular case of a dcpo with a small compact basis is analogous to the
notion of an accessible category [MP89].

In constructive set theory, our approach corresponds to working with partially
ordered classes as opposed to sets [Acz06]. Our notion of a small basis for a
dcpo (Section 5) is similar, but different from [Acz06]’s notion of a set-
generated dcpo [Acz06, Section 6.4]. While Aczel requires the set $\\{b\in
B\mid b\mathrel{\sqsubseteq}x\\}$ to be directed, we instead require the set
of elements in $B$ that are way-below $x$ to be directed in line with the
usual definition of a basis [AJ94, Section 2.2.6].

Finally, abstract bases were introduced by [Smy77] as “R-structures” [Smy77].
Our treatment of them and the rounded ideal completion is closer to that of
[AJ94] in the aforementioned [AJ94, Section 2.2.6], although ours is based on
families and avoids impredicative constructions.

###  1.3. Relation to our previous work

Along with Part I, this paper presents a revised and expanded treatment of the
results in our conference paper [dJE21]. With the notable exception of
Examples 5.21 and 5.3, the results of this paper can also be found in the
first author’s PhD thesis [dJon22]. Compared to the thesis, we also mention
two terminological changes:

  * •

Instead of writing “$\alpha$ is cofinal in $\beta$”, we now say that “$\beta$
exceeds $\alpha$” (see Definition 3.1). The issue with saying “cofinal” was
that this word is ordinarily used for two subsets where one is already
contained in the other. In particular, two cofinal subsets have the same least
upper bound (if it exists) and this was not the case with our usage of the
word “cofinal”.

  * •

We have swapped “continuity structure” for “continuity data” when discussing
continuous dcpos to reflect that the morphisms do not preserve the data (see
also Remark 4.3). Accordingly, we no longer say that a dcpo is “structurally
continuous”; instead writing that a dcpo is “equipped with continuity data”.
Similar terminological changes apply to the algebraic case.

The present treatment of continuous and algebraic dcpos and small (compact)
bases is significantly different from that of our earlier work [dJE21]. There,
the definition of continuous dcpo was an amalgamation of pseudocontinuity and
having a small basis, although it did not imply local smallness. In this work
we have disentangled the two notions and based our definition of continuity on
Johnstone and Joyal’s notion of a continuous category [JJ82] without making
any reference to a basis. The current notion of a small basis is simpler and
slightly stronger than that of our conference paper [dJE21], which allows us
to prove that having a small basis is equivalent to being presented by ideals.

###  1.4. Formalisation

All of our results are formalised in Agda, building on Escardó’s TypeTopology
development [Esc+]. The reference [dJon24a] precisely links each numbered
environment (including definitions, examples and remarks) in this paper to its
implementation. The HTML rendering has clickable links and so is particularly
suitable for exploring the development:
https://www.cs.bham.ac.uk/~mhe/TypeTopology/DomainTheory.Part-II.html.

###  1.5. Organisation

The paper is organised as follows:

Section 2:

Definition and examples of the way-below relation and compact elements.

Section 3:

The ind-completion of a preorder: a tool used to discuss continuity and
pseudocontinuity of dcpos.

Section 4:

Definitions of continuous and algebraic dcpos accompanied by a discussion on
pseudocontinuity and issues concerning the axiom of choice.

Section 5:

The notion of a small (compact) basis: strengthening continuity (resp.
algebraicity) by imposing smallness conditions.

Section 6:

The (rounded) ideal completion of an abstract basis as a continuous dcpo with
a small basis.

Section 7.1:

Bilimits and exponentials of structurally continuous (or algebraic) dcpos
(with small bases), including a proof that Scott’s $D_{\infty}$ is algebraic
with a small compact basis.

##  2\. The way-below relation and compactness

The way-below relation is the fundamental ingredient in the development of
continuous dcpos. Following Scott [Sco70], a computational intuition of $x\ll
y$ says that every computation of $y$ has to print $x$, or something better
than $x$, at some stage. We recall the notions of a directed family, its
supremum (denoted by $\bigsqcup$), and a $\mathcal{V}$-dcpo from Part I
(Definitions 3.4, 3.6 and 3.7, respectively).

######  Definition 2.1 (Way-below relation, $x\ll y$).

An element $x$ of a $\mathcal{V}$-dcpo $D$ is _way below_ an element $y$ of
$D$ if whenever we have a directed family $\alpha:I\to D$ indexed by
$I:\mathcal{V}$ such that $y\mathrel{\sqsubseteq}\bigsqcup\alpha$, then there
exists $i:I$ such that $x\mathrel{\sqsubseteq}\alpha_{i}$ already. We denote
this situation by $x\ll y$.

######  Lemma 2.2.

The way-below relation enjoys the following properties:

  1. (i)

it is proposition-valued;

  2. (ii)

if $x\ll y$, then $x\mathrel{\sqsubseteq}y$;

  3. (iii)

if $x\mathrel{\sqsubseteq}y\ll v\mathrel{\sqsubseteq}w$, then $x\ll w$;

  4. (iv)

it is antisymmetric;

  5. (v)

it is transitive.

###### Proof.

(i) Using that a dependent product of propositions (over an arbitrary type) is
again a proposition together with the fact that we propositionally truncated
the existence of $i:I$ in the definition. (ii) Simply take
$\alpha:\mathbf{1}_{\mathcal{V}}\to D$ to be $u\mapsto y$. (iii) Suppose that
$\alpha:I\to D$ is directed with $w\mathrel{\sqsubseteq}\bigsqcup\alpha$. Then
$v\mathrel{\sqsubseteq}\bigsqcup\alpha$, so by assumption that $y\ll v$ there
exists $i:I$ with $y\mathrel{\sqsubseteq}\alpha_{i}$ already. But then
$x\mathrel{\sqsubseteq}\alpha_{i}$. (iv) Follows from (ii). (v) Follows from
(ii) and (iii). ∎

In general, the way below relation is not reflexive. The elements for which it
is have a special status and are called compact. We illustrate this notion by
a series of examples.

######  Definition 2.3 (Compactness).

An element of a dcpo is _compact_ if it is way below itself.

######  Example 2.4.

The least element of a pointed dcpo is always compact.

We recall the $\mathcal{V}$-dcpo of propositions $\Omega_{\mathcal{V}}$ with
designated elements $\mathbf{0}_{\mathcal{V}}$ (the empty type) and
$\mathbf{1}_{\mathcal{V}}$ (the unit type) from Part I (Example 3.14).

######  Example 2.5 (Compact elements in $\Omega_{\mathcal{V}}$).

The compact elements of $\Omega_{\mathcal{V}}$ are exactly
$\mathbf{0}_{\mathcal{V}}$ and $\mathbf{1}_{\mathcal{V}}$. In other words, the
compact elements of $\Omega_{\mathcal{V}}$ are precisely the decidable
propositions.

###### Proof.

By Example 2.4 we know that $\mathbf{0}_{\mathcal{V}}$ must be compact. For
$\mathbf{1}_{\mathcal{V}}$, suppose that we have
$Q_{(-)}:I\to\Omega_{\mathcal{V}}$ directed such that
$\mathbf{1}_{\mathcal{V}}\mathrel{\sqsubseteq}\exists_{i:I}Q_{i}$. Then there
exists $i:I$ such that $Q_{i}$ holds, and hence,
$\mathbf{1}_{\mathcal{V}}\mathrel{\sqsubseteq}Q_{i}$. Now suppose that
$P:\Omega_{\mathcal{V}}$ is compact. We show that $P$ is decidable. The family
$\alpha:\left(P+\mathbf{1}_{\mathcal{V}}\right)\to\Omega_{\mathcal{V}}$ given
by $\operatorname{inl}(p)\mapsto\mathbf{1}_{\mathcal{V}}$ and
$\operatorname{inr}(\star)\mapsto\mathbf{0}_{\mathcal{V}}$ is directed and
$P\mathrel{\sqsubseteq}\bigsqcup\alpha$. Hence, by compactness, there exists
$i:P+\mathbf{1}_{\mathcal{V}}$ such that $P\mathrel{\sqsubseteq}\alpha_{i}$
already. Since being decidable is a property of a proposition, we actually get
such an $i$ and by case distinction on it we get decidability of $P$. ∎

We recall the lifting $\operatorname{\mathcal{L}}_{\mathcal{V}}(X)$ of a set
$X$ as a $\mathcal{V}$-dcpo from Part I (Section 5), which built on [EK17,
Kna18].

######  Example 2.6 (Compact elements in the lifting).

An element $(P,\varphi)$ of the lifting
$\operatorname{\mathcal{L}}_{\mathcal{V}}(X)$ of a set $X:\mathcal{V}$ is
compact if and only if $P$ is decidable. Hence, the compact elements of
$\operatorname{\mathcal{L}}_{\mathcal{V}}(X)$ are exactly $\bot$ and $\eta(x)$
for $x:X$.

###### Proof.

To see that compactness implies decidability of the domain of the partial
element, we proceed as in the proof of Example 2.5, but for a partial element
$(P,\varphi)$, we consider the family
$\alpha:\left(P+\mathbf{1}_{\mathcal{V}}\right)\to\operatorname{\mathcal{L}}_{\mathcal{V}}(X)$
given by $\operatorname{inl}(p)\mapsto\eta(\varphi(p))$ and
$\operatorname{inr}(\star)\mapsto\bot$. Conversely, if we have a partial
element $(P,\varphi)$ with $P$ decidable, then either $P$ is false in which
case $(P,\varphi)=\bot$ which is compact by Example 2.4, or $P$ holds. So
suppose that $P$ holds and let
$\alpha:I\to\operatorname{\mathcal{L}}_{\mathcal{V}}(X)$ be directed with
$P\mathrel{\sqsubseteq}\bigsqcup\alpha$. Since $P$ holds, the element
$\bigsqcup\alpha$ must be defined, which means that there exists $i:I$ such
that $\alpha_{i}$ is defined. But for this $i:I$ we also have
$\bigsqcup\alpha=\alpha_{i}$ by construction of the supremum, and hence,
$P\mathrel{\sqsubseteq}\alpha_{i}$, proving compactness of $(P,\varphi)$. ∎

For characterising the compact elements of the powerset, we introduce a lemma,
as well as the notion of Kuratowski finiteness and the induction principle for
Kuratowski finite subsets.

######  Lemma 2.7.

The compact elements of a dcpo are closed under (existing) binary joins.

###### Proof.

Suppose that $x$ and $y$ are compact elements of a $\mathcal{V}$-dcpo $D$ with
$z$ as their least upper bound and suppose that we have $\alpha:I\to D$
directed with $z\mathrel{\sqsubseteq}\bigsqcup\alpha$. Then
$x\mathrel{\sqsubseteq}\bigsqcup\alpha$ and
$y\mathrel{\sqsubseteq}\bigsqcup\alpha$, so by compactness there exist $i,j:I$
such that $x\mathrel{\sqsubseteq}\alpha_{i}$ and
$y\mathrel{\sqsubseteq}\alpha_{j}$. By semidirectedness of $\alpha$, there
exists $k:I$ with ${\alpha_{i},\alpha_{j}}\mathrel{\sqsubseteq}\alpha_{k}$, so
that ${x,y}\mathrel{\sqsubseteq}\alpha_{k}$. But $z$ is the join of $x$ and
$y$, so $z\mathrel{\sqsubseteq}\alpha_{k}$, as desired. ∎

We recall the type $\operatorname{\mathcal{P}}_{\mathcal{T}}(X)$ of
$\mathcal{T}$-valued subsets of $X$ and the set-theoretic notation $\in$ and
$\subseteq$ from Part I (Definitions 2.3 and 2.4).

######  Definition 2.8 (Total space of a subset, $\operatorname{\mathbb{T}}$).

The _total space_ of a $\mathcal{T}$-valued subset $S$ of a type $X$ is
defined as
$\operatorname{\mathbb{T}}(S)\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\Sigma_{x:X}(x\in
S)$.

######  Definition 2.9 (Kuratowski finiteness).

  1. (i)

A type $X$ is _Kuratowski finite_ if there exists some natural number
$n:\mathbb{N}$ and a surjection $e:\operatorname{Fin}(n)\twoheadrightarrow X$,
where $\operatorname{Fin}(n)$ is the standard finite type with exactly $n$
elements [Rij22, Section 7.3].

  2. (ii)

A subset is _Kuratowski finite_ if its total space is a Kuratowski finite
type.

Thus, a type $X$ is _Kuratowski finite_ if its elements can be finitely
enumerated, possibly with repetitions, although the repetitions can be removed
when $X$ has decidable equality.

######  Lemma 2.10.

The Kuratowski finite subsets of a set are closed under finite unions and
contain all singletons.

###### Proof.

The empty set and any singleton are clearly Kuratowski finite. Moreover, if
$A$ and $B$ are Kuratowski finite subsets, then we may assume to have natural
numbers $n$ and $m$ and surjections
$\sigma:\operatorname{Fin}(n)\twoheadrightarrow\operatorname{\mathbb{T}}(A)$
and
$\tau:\operatorname{Fin}(m)\twoheadrightarrow\operatorname{\mathbb{T}}(B)$. We
can then patch these together to obtain a surjection
$\operatorname{Fin}(n+m)\twoheadrightarrow\operatorname{\mathbb{T}}(A\cup B)$,
as desired. ∎

######  Lemma 2.11 (Induction for Kuratowski finite subsets).

A property of subsets of a type $X$ holds for all Kuratowski finite subsets of
$X$ as soon as

  1. (i)

it holds for the empty set,

  2. (ii)

it holds for any singleton subset, and

  3. (iii)

it holds for $A\cup B$, whenever it holds for $A$ and $B$.

###### Proof.

Let $Q$ be a such a property and let $A$ be an arbitrary Kuratowski finite
subset of $X$. Since $Q$ is proposition-valued, we may assume to have a
natural number $n$ and a surjection
$\sigma:\operatorname{Fin}(n)\twoheadrightarrow\operatorname{\mathbb{T}}(A)$.
Then the subset $A$ must be equal to the finite join of singletons
$\\{\sigma_{0}\\}\cup\\{\sigma_{1}\\}\cup\dots\cup\\{\sigma_{n-1}\\}$, which
can be shown to satisfy $Q$ by induction on $n$, and hence, so must $A$. ∎

######  Definition 2.12 ($\beta$).

For a set $X:\mathcal{U}$, we write
$\beta:\operatorname{List}(X)\to\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$
for the canonical map which takes a list to its set of elements. (For the
inductive definition of the type $\operatorname{List}(X)$, recall e.g. [Uni13,
Section 5.1].)

######  Lemma 2.13.

A subset $A:\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$ of a set
$X:\mathcal{U}$ is Kuratowski finite if and only if it is in the image of
$\beta$.

###### Proof.

The left to right direction follows from Lemma 2.10, while the converse
follows easily from the induction principle for Kuratowski finite subsets
where we use list concatenation in case (iii). ∎

######  Example 2.14 (Compact elements in
$\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$).

The compact elements of $\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$ for a
set $X:\mathcal{U}$ are exactly the Kuratowski finite subsets of $X$.

###### Proof.

Suppose first that $A:\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$ is a
compact element. The family

$\left(\Sigma_{l:\operatorname{List}(X)}\,\beta(l)\subseteq
A\right)\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$

is directed, as it contains $\emptyset$ and we can concatenate lists to
establish semidirectedness. Moreover,
$\left(\Sigma_{l:\operatorname{List}(X)}\,\beta(l)\subseteq A\right)$ lives in
$\mathcal{U}$ and we clearly have
$A\subseteq\bigsqcup{\beta\circ{\operatorname{pr_{1}}}}$. So by compactness,
there exists $l:\operatorname{List}(X)$ with $\beta(l)\subseteq A$ such that
$A\subseteq\beta(l)$ already. But this says exactly that $A$ is Kuratowski
finite by Lemma 2.13.

For the converse we use the induction principle for Kuratowski finite subsets:
the empty set is compact by Example 2.4, singletons are easily shown to be
compact, and binary unions are compact by Lemma 2.7. ∎

We end this section by presenting a few lemmas connecting the way-below
relation and compactness to Scott continuous sections, which we recall from
Part I (Definition 4.13).

######  Lemma 2.15.

If we have a Scott continuous retraction
${{D}}$${{E}}$$\scriptstyle{s}$$\scriptstyle{r}$, then $y\ll s(x)$ implies
$r(y)\ll x$ for every $x:D$ and $y:E$.

###### Proof.

Suppose that $y\ll s(x)$ and that $x\mathrel{\sqsubseteq}\bigsqcup\alpha$ for
a directed family $\alpha:I\to D$. Then
$s(x)\mathrel{\sqsubseteq}s\left(\bigsqcup\alpha\right)=\bigsqcup\left(s\circ\alpha\right)$
by Scott continuity of $s$, so there exists $i:I$ such that
$y\mathrel{\sqsubseteq}s(\alpha_{i})$ already. Now monotonicity of $r$ implies
$r(y)\mathrel{\sqsubseteq}r(s(\alpha_{i}))=\alpha_{i}$ which completes the
proof that $r(y)\ll x$. ∎

We also recall embedding-projection pairs from Part I (Definition 7.2).

######  Lemma 2.16.

The embedding in an embedding-projection pair
${{D}}$${{E}}$$\scriptstyle{\varepsilon}$$\scriptstyle{\pi}$ preserves and
reflects the way-below relation, i.e. $x\ll
y\iff\varepsilon(x)\ll\varepsilon(y)$. In particular, an element $x$ is
compact if and only if $\varepsilon(x)$ is.

###### Proof.

Suppose that $x\ll y$ in $D$ and let $\alpha:I\to E$ be directed with
$\varepsilon(y)\mathrel{\sqsubseteq}\bigsqcup\alpha$. Then
$y=\pi(\varepsilon(y))\mathrel{\sqsubseteq}\bigsqcup\pi\circ\alpha$ by Scott
continuity of $\pi$. Hence, there exists $i:I$ such that
$x\mathrel{\sqsubseteq}\pi(\alpha_{i})$. But then
$\varepsilon(x)\mathrel{\sqsubseteq}\varepsilon(\pi(\alpha_{i}))\mathrel{\sqsubseteq}\alpha_{i}$
by monotonicity of $\varepsilon$ and the fact that $\varepsilon\circ\pi$ is a
deflation. This proves that $x\ll y$. Conversely, if
$\varepsilon(x)\ll\varepsilon(y)$, then $x=\pi(\varepsilon(x))\ll y$ by Lemma
2.15. ∎

##  3\. The ind-completion

The ind-completion will be a useful tool for phrasing and proving results
about directed complete _posets_ and is itself a directed complete _preorder_
, cf. Lemma 3.3. It was introduced by [GV72] in [GV72, Section 8] in the
context of category theory, but its role in order theory is discussed in
[JJ82, Section 1]. We will also use it in the context of order theory, but our
treatment will involve a careful consideration of the universes involved, very
similar to the original treatment in [GV72].

######  Definition 3.1 ($\mathcal{V}$-ind-completion
$\mathcal{V}\\!\operatorname{-Ind}(X)$, exceed, ${\mathrel{\lesssim}}$).

The _$\mathcal{V}$ -ind-completion_ $\mathcal{V}\\!\operatorname{-Ind}(X)$ of
a preorder $X$ is the type of directed families in $X$ indexed by types in the
universe $\mathcal{V}$. Such a family $\beta:J\to X$ _exceeds_ another family
$\alpha:I\to X$ if for every $i:I$, there exists $j:J$ such that
$\alpha_{i}\mathrel{\sqsubseteq}\beta_{j}$, and we denote this relation by
$\alpha\mathrel{\lesssim}\beta$.

The following is straightforward.

######  Lemma 3.2.

The relation $\mathrel{\lesssim}$ defines a preorder on the ind-completion.

######  Lemma 3.3.

The $\mathcal{V}$-ind-completion $\mathcal{V}\\!\operatorname{-Ind}(X)$ of a
preorder $X$ is $\mathcal{V}$-directed complete.

###### Proof.

Suppose that we have a directed family
$\alpha:I\to\mathcal{V}\\!\operatorname{-Ind}(X)$ with $I:\mathcal{V}$. Then
each $\alpha_{i}$ is a directed family in $X$ indexed by a type
$J_{i}:\mathcal{V}$. We define the family
$\hat{\alpha}:\left(\Sigma_{i:I}J_{i}\right)\to X$ by
$(i,j)\mapsto\alpha_{i}(j)$. It is clear that $\hat{\alpha}$ exceeds each
$\alpha_{i}$, and that $\beta$ exceeds $\hat{\alpha}$ if $\beta$ exceeds every
$\alpha_{i}$. So it remains to show that $\hat{\alpha}$ is in fact an element
of $\mathcal{V}\\!\operatorname{-Ind}(X)$, i.e. that it is directed. Because
$\alpha$ and each $\alpha_{i}$ are directed, $I$ and each $J_{i}$ are
inhabited. Hence, so is the domain of $\hat{\alpha}$. It remains to show that
$\hat{\alpha}$ is semidirected. Suppose we have $(i_{1},j_{1}),(i_{2},j_{2})$
in the domain of $\hat{\alpha}$. By directedness of $\alpha$, there exists
$i:I$ such that $\alpha_{i}$ exceeds both $\alpha_{i_{1}}$ and
$\alpha_{i_{2}}$. Hence, there exist $j_{1}^{\prime},j_{2}^{\prime}:J_{i}$
with $\alpha_{i_{1}}(j_{1})\mathrel{\sqsubseteq}\alpha_{i}(j_{1}^{\prime})$
and $\alpha_{i_{2}}(j_{2})\mathrel{\sqsubseteq}\alpha_{i}(j_{2}^{\prime})$.
Because the family $\alpha_{i}$ is directed in $X$, there exists $j:J_{i}$
such that
$\alpha_{i}(j_{1}^{\prime}),\alpha_{i}(j_{2}^{\prime})\mathrel{\sqsubseteq}\alpha_{i}(j)$.
Hence, we conclude that
$\hat{\alpha}(i_{1},j_{1})\equiv\alpha_{i_{1}}(j_{1})\mathrel{\sqsubseteq}\alpha_{i}(j_{1}^{\prime})\mathrel{\sqsubseteq}\alpha_{i}(j)\equiv\hat{\alpha}(i,j)$,
and similarly for $(i_{2},j_{2})$, which proves semidirectedness of
$\hat{\alpha}$. ∎

######  Lemma 3.4.

Taking directed suprema defines a monotone map from a $\mathcal{V}$-dcpo to
its $\mathcal{V}$-ind-completion, denoted by
${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$.

###### Proof.

We have to show that $\bigsqcup\alpha\mathrel{\sqsubseteq}\bigsqcup\beta$ for
directed families $\alpha$ and $\beta$ such that $\beta$ exceeds $\alpha$.
Note that the inequality holds as soon as
$\alpha_{i}\mathrel{\sqsubseteq}\bigsqcup\beta$ for every $i$ in the domain of
$\alpha$. For this, it suffices that for every such $i$, there exists a $j$ in
the domain of $\beta$ such that $\alpha_{i}\mathrel{\sqsubseteq}\beta_{j}$.
But the latter says exactly that $\beta$ exceeds $\alpha$. ∎

[JJ82] [JJ82] generalise the notion of continuity from posets to categories
and do so by phrasing it in terms of
$\bigsqcup:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ having a left adjoint.
We follow their approach and now work towards this. It turns out to be
convenient to use the following two notions, which are in fact equivalent by
Lemma 3.8:

######  Definition 3.5 (Approximate, left adjunct).

For an element $x$ of a dcpo $D$ and a directed family $\alpha:I\to D$, we say
that

  1. (i)

$\alpha$ _approximates_ $x$ if the supremum of $\alpha$ is $x$ and each
$\alpha_{i}$ is way below $x$, and

  2. (ii)

$\alpha$ is _left adjunct_ to $x$ if $\alpha\mathrel{\lesssim}\beta\iff
x\mathrel{\sqsubseteq}\bigsqcup\beta$ for every directed family $\beta$.

######  Remark 3.6.

For a $\mathcal{V}$-dcpo $D$, a function
$L:D\to\mathcal{V}\\!\operatorname{-Ind}(D)$ is a left adjoint to
${{\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D}$ precisely when
$L(x)$ is left adjunct to $x$ for every $x:D$. Of course, we need to know that
$L$ is monotone and this is shown in the next lemma.

######  Lemma 3.7.

Every function $L:D\to\mathcal{V}\\!\operatorname{-Ind}(D)$ satisfying that
$L(x)$ is left adjunct to $x$ for every $x:D$ is monotone and order-
reflecting.

###### Proof.

Suppose we are given elements $x,y:D$. By assumption, we know that
$L(x)\mathrel{\lesssim}L(y)\iff x\mathrel{\sqsubseteq}\bigsqcup L(y)$, but
$L(y)$ approximates $y$, so $\bigsqcup L(y)=y$ and hence
$L(x)\mathrel{\lesssim}L(y)\iff x\mathrel{\sqsubseteq}y$, so $L$ preserves and
reflects the order. ∎

######  Lemma 3.8.

A directed family $\alpha$ approximates an element $x$ if and only if it is
left adjunct to it.

###### Proof.

Suppose first that $\alpha$ approximates $x$. If
$\alpha\mathrel{\lesssim}\beta$, then
$x=\bigsqcup\alpha\mathrel{\sqsubseteq}\bigsqcup\beta$, by Lemma 3.4.
Conversely, if $x\mathrel{\sqsubseteq}\bigsqcup\beta$, then $\beta$ exceeds
$\alpha$: for if $i$ is in the domain of $\alpha$, then $\alpha_{i}\ll x$, so
there exists $j$ such that $\alpha_{i}\mathrel{\sqsubseteq}\beta_{j}$ already.

In the other direction, suppose that $\alpha$ is left adjunct to $x$. We show
that each $\alpha_{i}$ is way below $x$. If $\beta$ is a directed family with
$x\mathrel{\sqsubseteq}\bigsqcup\beta$, then $\beta$ exceeds $\alpha$ as
$\alpha$ is assumed to be left adjunct to $x$. Hence, for every $i$, there
exists $j$ with $\alpha_{i}\mathrel{\sqsubseteq}\beta_{j}$, proving that
$\alpha_{i}\ll x$. Since $\alpha$ exceeds itself, we get
$x\mathrel{\sqsubseteq}\bigsqcup\alpha$ by assumption. For the other
inequality, we note that $x\mathrel{\sqsubseteq}\bigsqcup\hat{x}$, where
$\hat{x}:\mathbf{1}\to D$ is the directed family that maps to $x$. Hence, as
$\alpha$ is left adjunct to $x$, we must have that $\hat{x}$ exceeds $\alpha$,
which means that each $\alpha_{i}$ is below $x$. Thus,
$\bigsqcup\alpha\mathrel{\sqsubseteq}x$ and $x=\bigsqcup\alpha$ hold, as
desired. ∎

######  Proposition 3.9.

For a $\mathcal{V}$-dcpo $D$, a function
$L:D\to\mathcal{V}\\!\operatorname{-Ind}(D)$ is a left adjoint to
$\bigsqcup:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ if and only if $L(x)$
approximates $x$ for every $x:D$.

###### Proof.

Immediate from Lemma 3.8 and Remark 3.6. ∎

##  4\. Continuous and algebraic dcpos

Using the ind-completion from the previous section, we turn to defining
continuous and algebraic dcpos, paying special attention to size and
constructivity issues regarding the axiom of choice. This second issue is
discussed in Section 4.2 from two perspectives: type-theoretically, via a
discussion on the placement of the propositional truncation, and
categorically, via left adjoints.

###  4.1. Continuous dcpos

We define what it means for a $\mathcal{V}$-dcpo to be continuous and prove
the fundamental interpolation properties for the way-below relation. Examples
are postponed (see Sections 5.2 and 6.2) until we have developed the theory
further.

######  Definition 4.1 (Continuity data, $I_{x}$, $\alpha_{x}$).

_Continuity data_ for a $\mathcal{V}$-dcpo $D$ assigns to every $x:D$ a type
$I_{x}:\mathcal{V}$ and a directed _approximating family_ $\alpha_{x}:I\to D$
such that $\alpha_{x}$ has supremum $x$ and each element $\alpha_{x}(i)$ is
way below $x$.

The notion of continuity data can be understood categorically as follows.

######  Proposition 4.2.

The type of continuity data for a $\mathcal{V}$-dcpo $D$ is equivalent to the
type of left adjoints to ${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to
D$.

###### Proof.

Given continuity data for $D$, we define a function
$D\to\mathcal{V}\\!\operatorname{-Ind}(D)$ by sending $x:D$ to the directed
family $\alpha_{x}$. This is indeed a left adjoint to
${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ because of Proposition
3.9. Conversely, given a left adjoint
$L:{D\to\mathcal{V}\\!\operatorname{-Ind}(D)}$, the assignment $x\mapsto L(x)$
is continuity data for $D$, again by Proposition 3.9. That these two mapping
make up a type equivalence can be checked directly, using that the type
expressing that a map is a left adjoint to
${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ is a proposition. ∎

######  Remark 4.3.

It should be noted that having continuity data is _not_ a property of a dcpo,
i.e., the type of continuity data for a dcpo is not a subsingleton, because an
element $x:D$ can have several different approximating families, e.g. if
$\alpha:I\to D$ approximates $x$, then so does $[\alpha,\alpha]:(I+I)\to D$.
In other words, the left adjoint to
$\bigsqcup:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ is not unique, although
it is unique up to isomorphism (of the preorder
$\mathcal{V}\\!\operatorname{-Ind}(D)$). In category theory this is typically
sufficient (and often the best one can do). [JJ82] follow this philosophy in
[JJ82], but we want the type of continuous $\mathcal{V}$-dcpos to be a subtype
of the $\mathcal{V}$-dcpos. One reason that a property is preferred is that it
is considered good mathematical practice to only consider morphisms that
preserve imposed structure. In the case of continuity data, this would imply
preservation of the way-below relation, but this excludes many Scott
continuous maps, e.g. if the value of a constant map is not compact, then it
does not preserve the way-below relation.

It is natural to ask whether the univalence axiom can be used to identify
these isomorphic objects. However, this is not the case because the ind-
completion $\mathcal{V}\\!\operatorname{-Ind}(D)$ is _not_ a univalent
category in the sense of [AKS15], because it is a preorder and not a poset.
One way to obtain a subtype is to propositionally truncate the notion of
continuity data and this is indeed the approach that we will take. However,
another choice that would yield a property is to identify isomorphic elements
of $\mathcal{V}\\!\operatorname{-Ind}(D)$. This approach is discussed at
length in Section 4.2 and in particular it is explained to be inadequate in a
constructive setting.

######  Definition 4.4 (Continuity of a dcpo).

A $\mathcal{V}$-dcpo is _continuous_ if it has unspecified continuity data,
i.e. if the type of continuity data is inhabited.

Thus, a dcpo is continuous if we have an _unspecified_ function assigning an
approximating family to every element of the dcpo.

######  Proposition 4.5.

Continuity of a $\mathcal{V}$-dcpo $D$ is equivalent to having an unspecified
left adjoint to ${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$.

###### Proof.

By Proposition 4.2 and functoriality of the propositional truncation. ∎

######  Lemma 4.6.

For elements $x$ and $y$ of a dcpo with continuity data, the following are
equivalent:

  1. (i)

$x\mathrel{\sqsubseteq}y$;

  2. (ii)

$\alpha_{x}(i)\mathrel{\sqsubseteq}y$ for every $i:I_{x}$;

  3. (iii)

$\alpha_{x}(i)\ll y$ for every $i:I_{x}$.

###### Proof.

Note that (iii) implies (ii) and (ii) implies (i), because if
$\alpha_{x}(i)\mathrel{\sqsubseteq}y$ for every $i:I_{x}$, then
$x=\bigsqcup\alpha_{x}\mathrel{\sqsubseteq}y$, as desired. So it remains to
prove that (i) implies (iii), but this holds, because $\alpha_{x}(i)\ll x$ for
every $i:I_{x}$. ∎

######  Lemma 4.7.

For elements $x$ and $y$ of a dcpo with continuity data, $x$ is way below $y$
if and only if there exists $i:I_{y}$ such that
$x\mathrel{\sqsubseteq}\alpha_{y}(i)$.

###### Proof.

The left-to-right implication holds, because $\alpha_{y}$ is a directed family
with supremum $y$, while the converse holds because $\alpha_{y}(i)\ll y$ for
every $i:I_{y}$. ∎

We now prove three interpolation lemmas for dcpos with continuity data.
Because the conclusions of the lemmas are propositions, the results will
follow for continuous dcpos immediately.

######  Lemma 4.8 (Nullary interpolation for the way-below relation).

For every $x:D$ of a continuous dcpo $D$, there exists $y:D$ such that $y\ll
x$.

###### Proof.

The approximating family $\alpha_{x}$ is directed, so there exists $i:I_{x}$
and hence we can take
$y\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\alpha_{x}(i)$ since
$\alpha_{x}(i)\ll x$. ∎

Our proof of the following lemma is inspired by [JJ82, Proposition 2.12].

######  Lemma 4.9 (Unary interpolation for the way-below relation).

If $x\ll y$ in a continuous dcpo $D$, then there exists an _interpolant_ $d:D$
such that $x\ll d\ll y$.

###### Proof.

Since we are proving a proposition, we may assume to be given continuity data
for $D$. Thus, we can approximate every approximant $\alpha_{y}(i)$ of $y$ by
an approximating family $\beta_{i}:J_{i}\to D$. This defines a map
$\hat{\beta}$ from $I_{y}$ to $\mathcal{V}\\!\operatorname{-Ind}(D)$, the ind-
completion of the $\mathcal{V}$-dcpo $D$, by sending $i:I_{y}$ to the directed
family $\beta_{i}$. We claim that $\hat{\beta}$ is directed in
$\mathcal{V}\\!\operatorname{-Ind}(D)$. Since $\alpha_{y}$ is directed,
$I_{y}$ is inhabited, so it remains to prove that $\hat{\beta}$ is
semidirected. So suppose we have $i_{1},i_{2}:I_{y}$. Because $\alpha_{y}$ is
semidirected, there exists $i:I_{y}$ such that
$\alpha_{y}(i_{1}),\alpha_{y}(i_{2})\mathrel{\sqsubseteq}\alpha_{y}(i)$. We
claim that $\beta_{i}$ exceeds $\beta_{i_{1}}$ and $\beta_{i_{2}}$, which
would prove semidirectedness of $\hat{\beta}$. We give the argument for
$i_{1}$ only as the case for $i_{2}$ is completely analogous. We have to show
that for every $j:J_{i_{1}}$, there exists $j^{\prime}:J_{i}$ such that
$\beta_{i_{1}}(j)\mathrel{\sqsubseteq}\beta_{i}(j^{\prime})$. But this holds
because $\beta_{i_{1}}(j)\ll\bigsqcup\beta_{i}$ for every such $j$, as we have
$\beta_{i_{1}}(j)\ll\alpha_{y}(i_{1})\mathrel{\sqsubseteq}\alpha_{y}(i)\mathrel{\sqsubseteq}\bigsqcup\beta_{i}$.

Thus, $\hat{\beta}$ is directed in $\mathcal{V}\\!\operatorname{-Ind}(D)$ and
hence we can calculate its supremum in $\mathcal{V}\\!\operatorname{-Ind}(D)$
to obtain the _directed_ family $\gamma:(\Sigma_{i:I}J_{i})\to D$ given by
$(i,j)\mapsto\beta_{i}(j)$.

We now show that $y$ is below the supremum of $\gamma$. By Lemma 4.6, it
suffices to prove that $\alpha_{y}(i)\mathrel{\sqsubseteq}\bigsqcup\gamma$ for
every $i:I_{y}$, and, in turn, to prove this for an $i:I_{y}$ it suffices to
prove that $\beta_{i}(j)\mathrel{\sqsubseteq}\bigsqcup\gamma$ for every
$j:J_{i}$. But this is immediate from the definition of $\gamma$. Thus,
$y\mathrel{\sqsubseteq}\bigsqcup\gamma$. Because $x\ll y$, there exists
$(i,j):\Sigma_{i:I}J_{i}$ such that
$x\mathrel{\sqsubseteq}\gamma(i,j)\equiv\beta_{i}(j)$.

Finally, for our interpolant, we take
$d\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\alpha_{y}(i)$. Then, indeed,
$x\ll d\ll y$, because
$x\mathrel{\sqsubseteq}\beta_{i}(j)\ll\alpha_{y}(i)\equiv d$ and
$d\equiv\alpha_{y}(i)\ll y$, completing the proof. ∎

######  Lemma 4.10 (Binary interpolation for the way-below relation).

If $x\ll z$ and $y\ll z$ in a continuous dcpo $D$, then there exists an
interpolant $d:D$ such that $x,y\ll d$ and $d\ll z$.

The proof is a straightforward application of unary interpolation.

###### Proof.

Using that $x\ll z$ and $y\ll z$, there exist interpolants ${d_{1},d_{2}}:D$
such that $x\ll d_{1}\ll z$ and $y\ll d_{2}\ll z$. Hence, there exist
$i_{1},i_{2}:I_{z}$ such that $d_{1}\mathrel{\sqsubseteq}\alpha_{z}(i_{1})$
and $d_{2}\mathrel{\sqsubseteq}\alpha_{z}(i_{2})$. By semidirectedness of
$\alpha_{z}$, there then exists $i:I_{z}$ for which
$d_{1},d_{2}\mathrel{\sqsubseteq}\alpha_{z}(i)$. Our final interpolant is
defined as $d\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\alpha_{z}(i)$, which
works because $x\ll d_{1}\mathrel{\sqsubseteq}d$, $y\ll
d_{2}\mathrel{\sqsubseteq}d$ and $d\equiv\alpha_{z}(i)\ll z$. ∎

Continuous dcpos are closed under Scott continuous retracts. Keeping track of
universes, it holds in the following generality, where we recall from Part I
(Definition 3.9) that we write
$\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{U},\mathcal{T}}$ for the type of
$\mathcal{V}$-dcpos with carriers in $\mathcal{U}$ and order relations taking
values in $\mathcal{T}$.

######  Theorem 4.11.

If we have dcpos
$D:\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{U},\mathcal{T}}$ and
$E:\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{U^{\prime}},\mathcal{T^{\prime}}}$
such that $D$ is a Scott continuous retract of $E$, then $D$ is continuous if
$E$ is. Moreover, we can give continuity data for $D$ if we have such data for
$E$.

###### Proof.

We prove the result in case we are given continuity data for $E$, as the other
will follow from that and the fact that the propositional truncation is
functorial. So suppose that we have a Scott continuous section $s:D\to E$ and
retraction $r:E\to D$. We claim that for every $x:D$, the family
$r\circ\alpha_{s(x)}$ approximates $x$. Firstly, it is directed, because
$\alpha_{s(x)}$ is and $r$ is Scott continuous. Secondly,

$\displaystyle\textstyle\bigsqcup r\circ\alpha_{s(x)}$
$\displaystyle=r\left(\textstyle\bigsqcup\alpha_{s(x)}\right)$ (by Scott
continuity of $r$) $\displaystyle=r(s(x))$ (as $\alpha_{s(x)}$ is the
approximating family of $s(x)$) $\displaystyle=x$ $\displaystyle\text{(because
$s$ is a section of $r$)},$

so the supremum of $r\circ\alpha_{s(x)}$ is $x$. Finally, we must prove that
$r\left(\alpha_{s(x)}(i)\right)\ll x$ for every $i:I_{x}$. By Lemma 2.15, this
is implied by $\alpha_{s(x)}(i)\ll s(x)$, which holds as $\alpha_{s(x)}$ is
the approximating family of $s(x)$. ∎

Recall from Part I (Definition 3.12) that a $\mathcal{V}$-dcpo is locally
small if $x\mathrel{\sqsubseteq}y$ is equivalent to a type in $\mathcal{V}$
for all elements $x$ and $y$.

######  Proposition 4.12.

A continuous dcpo is locally small if and only if its way-below relation has
small values.

###### Proof.

By Lemmas 4.6 and 4.7, we have

$x\mathrel{\sqsubseteq}y\iff\forall_{i:I_{x}}\left(\alpha_{x}(i)\ll
y\right)\quad\text{and}\quad x\ll
y\iff\exists_{i:I_{y}}\left(x\mathrel{\sqsubseteq}\alpha_{y}(i)\right),$

for every two elements $x$ and $y$ of a dcpo with continuity data. But the
types $I_{x}$ and $I_{y}$ are small, finishing the proof. The result also
holds for continuous dcpos, because what we are proving is a proposition. ∎

Proposition 4.12 is significant because the definition of the way-below
relation for a $\mathcal{V}$-dcpo $D$ quantifies over all families into $D$
indexed by types in $\mathcal{V}$.

###  4.2. Pseudocontinuity

In light of Proposition 4.2, we see that a $\mathcal{V}$-dcpo $D$ can have
continuity data in more than one way: the map
${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ can have two left
adjoints $L_{1},L_{2}$ such that for some $x:D$, the directed families
$L_{1}(x)$ and $L_{2}(x)$ exceed each other, yet are unequal. In order for the
left adjoint to be truly unique (and not just up to isomorphism), the preorder
$\mathcal{\mathcal{V}}\\!\operatorname{-Ind}(D)$ would have to identify
families that exceed each other. Of course, we could enforce this
identification by passing to the poset reflection
$\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}$ of
$\mathcal{V}\\!\operatorname{-Ind}(D)$ and this section studies exactly that.

Another perspective on the situation is the following: The type-theoretic
definition of having continuity data for a $\mathcal{V}$-dcpo $D$ is of the
form $\Pi_{x:D}\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\dots$, while
continuity is defined as its propositional truncation
$\left\|\Pi_{x:D}\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\dots\right\|$.
Yet another way to obtain a property is by putting the propositional
truncation on the _inside_ instead:
$\Pi_{x:D}\left\|\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\dots\right\|$.
We study what this amounts to and how it relates to continuity and the poset
reflection. Our results are summarised in Table 1 below.

######  Definition 4.13 (Pseudocontinuity).

A $\mathcal{V}$-dcpo $D$ is _pseudocontinuous_ if for every $x:D$ there exists
an unspecified directed family that approximates $x$.

Notice that continuity data $\Rightarrow$ continuity $\Rightarrow$
pseudocontinuity, but reversing the first implication is an instance of global
choice [Esc19, Section 3.35.6], while reversing the second amounts to an
instance of the axiom of choice that we do not expect to be provable in our
constructive setting. We further discuss this point in Remark 4.15.

For a $\mathcal{V}$-dcpo $D$, the map
${\bigsqcup}:\mathcal{V}\\!\operatorname{-Ind}(D)\to D$ is monotone, so it
induces a unique monotone map
${\bigsqcup_{\approx}}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}\to D$
such that the diagram

${\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}}$${D}$${\mathcal{V}\\!\operatorname{-Ind}(D)}$$\scriptstyle{\bigsqcup_{\approx}}$$\scriptstyle{[-]}$$\scriptstyle{\bigsqcup}$
(1)

commutes.

######  Proposition 4.14.

A $\mathcal{V}$-dcpo $D$ is pseudocontinuous if and only if the map of posets
${\bigsqcup}_{\approx}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}\to D$
has a necessarily unique left adjoint.

Observe that the type of left adjoints to
${\bigsqcup}_{\approx}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}\to D$ is
a proposition, precisely because
$\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}$ is a poset, cf. [AKS15, Lemma
5.2].

###### Proof.

Suppose that
${\bigsqcup}_{\approx}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}\to D$
has a left adjoint $L$ and let $x:D$ be arbitrary. We have to prove that there
exists a directed family $\alpha:I\to D$ that approximates $x$. By
surjectivity of the universal map $[-]$, there exists a directed family
$\alpha:I\to D$ such that $L(x)=[\alpha]$. Moreover, $\alpha$ approximates $x$
by virtue of Lemma 3.8, since for every
$\beta:\mathcal{V}\\!\operatorname{-Ind}(D)$, we have

$\displaystyle\alpha\mathrel{\lesssim}\beta$ $\displaystyle\iff
L(x)\leq[\beta]$ (since $L(x)=[\alpha]$) $\displaystyle\iff
x\mathrel{\sqsubseteq}\textstyle\bigsqcup_{\approx}{[\beta]}$ (since $L$ is a
left adjoint to $\textstyle{\bigsqcup}_{\approx}$) $\displaystyle\iff
x\mathrel{\sqsubseteq}\textstyle\bigsqcup\beta$ $\displaystyle\text{(by
\lx@cref{creftype~refnum}{supremum-map-quotient-comm})}.$

The converse is more involved and we apply [Kra+17, Theorem 5.4], which says
that every weakly constant map with values in a set factors through the
propositional truncation of its domain. Assume that $D$ is pseudocontinuous.
We start by constructing the left adjoint, so let $x:D$ be arbitrary. Writing
$\mathcal{A}_{x}$ for the type of directed families that approximate $x$, we
have an obvious map
$\varphi_{x}:\mathcal{A}_{x}\to\mathcal{V}\\!\operatorname{-Ind}(D)$ that
forgets that the directed family approximates $x$.

We claim that all elements in the image of $\varphi_{x}$ exceed each other.
For if $\alpha$ and $\beta$ are directed families both approximating $x$, then
for every $i$ in the domain of $\alpha$ we know that $\alpha_{i}\ll
x=\bigsqcup\beta$, so that there exists $j$ with
$\alpha_{i}\mathrel{\sqsubseteq}\beta_{j}$. Hence, passing to the poset
reflection, the composite $[-]\circ\varphi_{x}$ is constant. Thus, by [Kra+17,
Theorem 5.4] we have a (necessarily unique) map $\psi_{x}$ making the diagram

${\mathcal{A}_{x}}$${\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}}$${\left\|\mathcal{A}_{x}\right\|}$$\scriptstyle{[-]\circ\varphi_{x}}$$\scriptstyle{|-|}$$\scriptstyle{\psi_{x}}$

commute. Since $D$ is assumed to be pseudocontinuous, we have that
$\left\|\mathcal{A}_{x}\right\|$ holds for every $x:D$, so together with
$\psi_{x}$ this defines a map
$L:D\to\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}$ by
$L(x)\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\psi_{x}(p)$, where $p$
witnesses pseudocontinuity at $x$.

Lastly, we prove that $L$ is indeed a left adjoint to ${\bigsqcup}_{\approx}$.
So let $x:D$ be arbitrary. Since we’re proving a property, we can use
pseudocontinuity at $x$ to specify a directed family $\alpha$ that
approximates $x$. We now have to prove $[\alpha]\leq\beta^{\prime}\iff
x\mathrel{\sqsubseteq}\bigsqcup_{\approx}\beta^{\prime}$ for every
$\beta^{\prime}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}$. This is a
proposition, so using quotient induction, it suffices to prove
$[\alpha]\leq[\beta]\iff x\mathrel{\sqsubseteq}\bigsqcup_{\approx}[\beta]$ for
every $\beta:\mathcal{V}\\!\operatorname{-Ind}(D)$. Indeed, for such $\beta$
we have

$\displaystyle[\alpha]\leq[\beta]$
$\displaystyle\iff\alpha\mathrel{\lesssim}\beta$ $\displaystyle\iff
x\mathrel{\sqsubseteq}\textstyle\bigsqcup\beta$ (by Lemma 3.8 and the fact
that $\alpha$ approximates $x$) $\displaystyle\iff
x\mathrel{\sqsubseteq}\textstyle\bigsqcup_{\approx}[\beta]$
$\displaystyle\text{(by \lx@cref{creftype~refnum}{supremum-map-quotient-
comm})},$

finishing the proof. ∎

Thus, the explicit type-theoretic formulation and the formulation using left
adjoints in each row of Table 1 (which summarises our findings) are
equivalent.

| Type-theoretic formulation |  Formulation with adjoints | Property
---|---|---|---
Continuity data | $\Pi_{x:D}\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\,\delta(\alpha,x)$ |  Specified left adjoint to ${\bigsqcup:\mathcal{V}\\!\operatorname{-Ind}(D)\to D}$ | ✕
Continuity | $\left\|\Pi_{x:D}\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\,\delta(\alpha,x)\right\|$ |  Unspecified left adjoint to ${\bigsqcup:\mathcal{V}\\!\operatorname{-Ind}(D)\to D}$ | ✓
Pseudocont. | $\Pi_{x:D}\left\|\Sigma_{I:\mathcal{V}}\Sigma_{\alpha:I\to D}\,\delta(\alpha,x)\right\|$ |  Specified left adjoint to ${\bigsqcup_{\approx}:\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}\to D}$ | ✓
Table 1. Continuity (data) and pseudocontinuity of a dcpo $D$, where
$\delta(\alpha,x)$ abbreviates that $\alpha$ is directed and approximates $x$.

######  Remark 4.15.

The issue with pseudocontinuity is that taking the quotient introduces a
dependence on instances of the axiom of choice when it comes to proving
properties of pseudocontinuous dcpos. An illustrative example is the proof of
unary interpolation (Lemma 4.9), where we used the continuity data to first
approximate an element $y$ by $\alpha_{y}$ and then, in turn, approximate
every approximant $\alpha_{y}(i)$. With pseudocontinuity this argument would
require _choosing_ an approximating family for every $i$. Another example is
that while the preorder $\mathcal{V}\\!\operatorname{-Ind}(D)$ is
$\mathcal{V}$-directed complete, a direct lifting of the proof of this fact to
the poset reflection $\mathcal{V}\\!\operatorname{-Ind}(D)/{\approx}$ requires
the axiom of choice. The same issues concerning the axiom of choice occur in
[JJ82, pp. 260–261] and the notion of continuity data follows their solution
precisely. We then truncate this to get a property of dcpos (recall Remark
4.3), resulting in our definition of a continuity.

###  4.3. Algebraic dcpos

Many of our examples of dcpos are not just continuous, but satisfy the
stronger condition of being algebraic, meaning their elements can be
approximated by compact elements only.

######  Definition 4.16 (Algebraicity data, $I_{x}$, $\kappa_{x}$).

_Algebraicity data_ for a $\mathcal{V}$-dcpo $D$ assigns to every $x:D$ a type
$I_{x}:\mathcal{V}$ and a directed family $\kappa_{x}:I\to D$ of _compact_
elements such that $\kappa_{x}$ has supremum $x$.

######  Definition 4.17 (Algebraicity).

A $\mathcal{V}$-dcpo is _algebraic_ if it has some unspecified algebraicity
data, i.e. if the type of algebraicity data is inhabited.

######  Lemma 4.18.

Every algebraic dcpo is continuous.

###### Proof.

We prove that algebraicity data for a dcpo yields continuity data. The claim
for algebraic and continuous then follows by functoriality of the
propositional truncation. It suffices to prove that $\kappa_{x}(i)\ll x$ for
every $i:I_{x}$. By assumption, $\kappa_{x}(i)$ is compact and has supremum
$x$. Hence,
$\kappa_{x}(i)\ll\kappa_{x}(i)\mathrel{\sqsubseteq}\bigsqcup\kappa_{x}=x$, so
$\kappa_{x}(i)\ll x$. ∎

##  5\. Small bases

Recall that the traditional, set-theoretic definition of a dcpo $D$ being
continuous says that for every element $x\in D$, the subset $\\{y\in D\mid
y\ll x\\}$ is directed with supremum $x$. As explained in the introduction,
the problem with this definition in a predicative context is that the subset
$\\{y\in D\mid y\ll x\\}$ is not small in general. But, as is well-known in
domain theory, it is sufficient (and in fact equivalent) to instead ask that
$D$ has a subset $B$, known as a _basis_ , such that the subset $\\{b\in B\mid
b\ll x\\}\subseteq B$ is directed with supremum $x$, see [AJ94, Section 2.2.2]
and [Gie+03, Definition III-4.1]. The idea developed in this section is that
in many examples we can find a _small_ basis giving us a predicative handle on
the situation.

If a dcpo has a small basis, then it is continuous. In fact, all our running
examples of continuous dcpos are actually examples of dcpos with small bases.
Moreover, dcpos with small bases are better behaved. For example, they are all
locally small and so are their exponentials, which also have small bases
(Section 7.2). In Section 6.3 we also show that having a small basis is
equivalent to being presented by ideals.

Following the flow of Section 4, we first consider small bases for continuous
dcpos, before turning to small compact bases for algebraic dcpos (Section
5.1). After presenting examples of dcpos with small compact bases in Section
5.2, we describe the canonical small compact basis for an algebraic dcpo and
the role that the univalence axiom and a set replacement principle play in
Section 5.3.

######  Definition 5.1 (Small basis).

For a $\mathcal{V}$-dcpo $D$, a map $\beta:B\to D$ with $B:\mathcal{V}$ is a
_small basis_ for $D$ if the following conditions hold:

  1. (i)

for every $x:D$, the family $\left(\Sigma_{b:B}\left(\beta(b)\ll
x\right)\right)\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$ is directed
and has supremum $x$;

  2. (ii)

for every $x:D$ and $b:B$, the proposition $\beta(b)\ll x$ is
$\mathcal{V}$-small.

We will write
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ for
the type $\Sigma_{b:B}\left(\beta(b)\ll x\right)$ and conflate this type with
the canonical map
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$.

Item (ii) ensures not only that the type $\Sigma_{b:B}\left(\beta(b)\ll
x\right)$ is $\mathcal{V}$-small, but also that a dcpo with a small basis is
locally small (Proposition 5.5).

######  Remark 5.2.

If $\beta:B\to D$ is a small basis for a $\mathcal{V}$-dcpo $D$, then the type
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is
small. Hence, we have a type $I:\mathcal{V}$ and an equivalence
$\varphi:I\simeq\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$
and we see that the family
$I\xrightarrow{\varphi}\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$
is directed and has the same supremum as
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\to D$.
We will use this tacitly and write as if the type
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is
actually a type in $\mathcal{V}$.

######  Lemma 5.3.

If a dcpo comes equipped with a small basis, then it can be equipped with
continuity data. Hence, if a dcpo has an unspecified small basis, then it is
continuous.

###### Proof.

For every element $x$ of a dcpo $D$, the family
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\to D$
approximates $x$, so the assignment
$x\mapsto\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$
is continuity data for $D$. ∎

######  Lemma 5.4.

In a dcpo $D$ with a small basis $\beta:B\to D$, we have
$x\mathrel{\sqsubseteq}y$ if and only if $\forall_{b:B}\left(\beta(b)\ll
x\to\beta(b)\ll y\right)$ for every $x,y:D$.

###### Proof.

If $x\mathrel{\sqsubseteq}y$ and $\beta(b)\ll x$, then $\beta(b)\ll y$, so the
left-to-right implication is clear. For the converse, suppose that the
condition of the lemma holds. Because
$x=\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$,
the inequality $x\mathrel{\sqsubseteq}y$ holds as soon as
$\beta(b)\mathrel{\sqsubseteq}y$ for every $b:B$ with $\beta(b)\ll x$, but
this is implied by the condition. ∎

######  Proposition 5.5.

A dcpo with a small basis is locally small. Moreover, the way-below relation
on all of the dcpo has small values.

###### Proof.

The first claim follows from Lemma 5.4 and the second follows from the first
and Proposition 4.12. ∎

A notable feature of dcpos with a small basis is that interpolants for the
way-below relation, cf. Lemmas 4.8, 4.9 and 4.10, can be found in the basis,
as we show now.

######  Lemma 5.6 (Nullary interpolation in the basis for the way-below
relation).

In a dcpo $D$ with a small basis $\beta:B\to D$, there exists $b:B$ with
$\beta(b)\ll x$ for every $x:D$.

###### Proof.

For every $x:D$, the approximating family
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}x$ is directed,
so there exists $b:B$ with $\beta(b)\ll x$. ∎

######  Lemma 5.7 (Unary interpolation in the basis for the way-below
relation).

If $x\ll y$ in a dcpo $D$ with a small basis $\beta:B\to D$, then there exists
an interpolant $b:B$ such that $x\ll\beta(b)\ll y$.

###### Proof.

The small basis ensures that we have continuity data for $D$ by Lemma 5.3.
Hence, if $x\ll y$, then there exists an interpolant $d:D$ with $x\ll d\ll y$.
Now $d\ll
y\mathrel{\sqsubseteq}\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}y$,
so there exists $b:B$ such that $d\mathrel{\sqsubseteq}\beta(b)\ll y$.
Moreover, $x\ll d\mathrel{\sqsubseteq}\beta(b)$, completing the proof. ∎

######  Lemma 5.8 (Binary interpolation in the basis for the way-below
relation).

If $x\ll z$ and $y\ll z$ in a dcpo $D$ with a small basis $\beta:B\to D$, then
there exists an interpolant $b:B$ such that $x,y\ll\beta(b)$ and $\beta(b)\ll
z$.

###### Proof.

Again, the small basis ensures that we have continuity data for $D$ by Lemma
5.3. Hence, if $x\ll y$ and $y\ll z$, then there exists an interpolant $d:D$
with $x,y\ll d\ll z$. Now $d\ll
z\mathrel{\sqsubseteq}\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}z$,
so there exists $b:B$ such that $d\mathrel{\sqsubseteq}\beta(b)\ll z$.
Moreover, $x,y\ll d\mathrel{\sqsubseteq}\beta(b)$, completing the proof. ∎

Before proving the analogue of Theorem 4.11 (closure under Scott continuous
retracts) for small bases, we need a type-theoretic analogue of [AJ94,
Proposition 2.2.4] and [Gie+03, Proposition III-4.2], which essentially says
that it is sufficient for a “subset” of
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ (given
by $\sigma$ in the lemma) to be directed and have supremum $x$.

######  Lemma 5.9.

Suppose that we have an element $x$ of a $\mathcal{V}$-dcpo $D$ together with
two maps $\beta:B\to D$ and $\sigma:I\to\Sigma_{b:B}\left(\beta(b)\ll
x\right)$ with $I:\mathcal{V}$. If
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\circ\sigma$
is directed and has supremum $x$, then
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is
directed with supremum $x$ too.

###### Proof.

Suppose that
${\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x}\circ{\sigma}$
is directed and has supremum $x$. Obviously, $x$ is an upper bound for
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$, so we
are to prove that it is the least. If $y$ is an upper bound for
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$, then
it is also an upper bound for
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\circ\sigma$
which has supremum $x$, so that $x\mathrel{\sqsubseteq}y$ follows. So the
point is directedness of
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$. Its
domain is inhabited, because $\sigma$ is directed. Now suppose that we have
$b_{1},b_{2}:B$ with $\beta(b_{1}),\beta(b_{2})\ll x$. Since
$x=\bigsqcup\left(\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\circ\sigma\right)$,
there exist $i_{1},i_{2}:I$ such that
$\beta(b_{1})\mathrel{\sqsubseteq}\beta({\operatorname{pr_{1}}}(\sigma(i_{1})))$
and
$\beta(b_{2})\mathrel{\sqsubseteq}\beta({\operatorname{pr_{1}}}(\sigma(i_{2})))$.
Since
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\circ\sigma$
is directed, there exists $i:I$ with
$\beta({\operatorname{pr_{1}}}(\sigma(i_{1}))),\beta({\operatorname{pr_{1}}}(\sigma(i_{2})))\mathrel{\sqsubseteq}\beta({\operatorname{pr_{1}}}(\sigma(i)))$.
Hence, writing
$b\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}{\operatorname{pr_{1}}}(\sigma(i))$,
we have $\beta(b)\ll x$ and
$\beta(b_{1}),\beta(b_{2})\mathrel{\sqsubseteq}\beta(b)$. Thus,
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is
directed, as desired. ∎

######  Theorem 5.10.

If we have a Scott continuous retract
${{D}}$${{E}}$$\scriptstyle{s}$$\scriptstyle{r}$ and $\beta:B\to E$ is a small
basis for $E$, then $r\circ\beta$ is a small basis for $D$.

###### Proof.

First of all, note that $E$ is locally small by Proposition 5.5. But being
locally small is closed under Scott continuous retracts by Lemma 4.14 of Part
I, so $D$ is locally small too. Moreover, we have continuity data for $D$ by
virtue of Theorem 4.11 and Lemma 5.3. Hence, the way-below relation is small-
valued by Proposition 4.12. In particular, the proposition $r(\beta(b))\ll x$
is small for every $b:B$ and $x:D$.

We are going to use Lemma 5.9 to show that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{r\circ\beta}x$
is directed and has supremum $x$ for every $x:D$. By Lemma 2.15, the identity
on $B$ induces a well-defined map $\sigma:\left(\Sigma_{b:B}\left(\beta(b)\ll
s(x)\right)\right)\to\left(\Sigma_{b:B}\left(r(\beta(b))\ll y\right)\right)$.
Now Lemma 5.9 tells us that it suffices to prove that
$r\circ\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}s(x)$
is directed with supremum $x$. But
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}s(x)$ is
directed with supremum $x$, so by Scott continuity of $r$, the family
$r\circ\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}s(x)$
is directed with supremum $r(s(x))=x$, as desired. ∎

Finally, a nice use of dcpos with small bases is that they yield locally small
exponentials, as we can restrict the quantification in the pointwise order to
elements of the small basis.

######  Proposition 5.11.

If $D$ is a dcpo with an unspecified small basis and $E$ is a locally small
dcpo, then the exponential $E^{D}$ is locally small too.

###### Proof.

Being locally small is a proposition, so in proving the result we may assume
that $D$ comes equipped with a small basis $\beta:B\to D$. For arbitrary Scott
continuous functions $f,g:D\to E$, we claim that $f\mathrel{\sqsubseteq}g$
precisely when
$\forall_{b:B}\left(f(\beta(b))\mathrel{\sqsubseteq}g(\beta(b))\right)$, which
is a small type using that $E$ is locally small. The left-to-right implication
is obvious, so suppose that $f(\beta(b))\mathrel{\sqsubseteq}g(\beta(b))$ for
every $b:B$ and let $x:D$ be arbitrary. We are to show that
$f(x)\mathrel{\sqsubseteq}g(x)$. Since
$x=\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$,
it suffices to prove
$f\left(\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\right)\mathrel{\sqsubseteq}g\left(\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\right)$
and in turn, that
$f(\beta(b))\mathrel{\sqsubseteq}g\left(\bigsqcup\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\right)$
for every $b:B$. But is easily seen to hold, because
$f(\beta(b))\mathrel{\sqsubseteq}g(\beta(b))$ for every $b:B$ by assumption. ∎

###  5.1. Small compact bases

Similarly to the progression from continuous dcpos (Section 4.1) to algebraic
ones (Section 4.3), we now turn to small _compact_ bases.

######  Definition 5.12 (Small compact basis).

For a $\mathcal{V}$-dcpo $D$, a map $\beta:B\to D$ with $B:\mathcal{V}$ is a
_small compact basis_ for $D$ if the following conditions hold:

  1. (i)

for every $b:B$, the element $\beta(b)$ is compact in $D$;

  2. (ii)

for every $x:D$, the family
$\left(\Sigma_{b:B}\left(\beta(b)\mathrel{\sqsubseteq}x\right)\right)\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$
is directed and has supremum $x$;

  3. (iii)

for every $x:D$ and $b:B$, the proposition $\beta(b)\mathrel{\sqsubseteq}x$ is
$\mathcal{V}$-small.

We will write $\mathop{\downarrow}_{\beta}x$ for the type
$\Sigma_{b:B}\left(\beta(b)\mathrel{\sqsubseteq}x\right)$ and conflate this
type with the canonical map
$\mathop{\downarrow}_{\beta}x\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$.

######  Remark 5.13.

If $\beta:B\to D$ is a small compact basis for a $\mathcal{V}$-dcpo $D$, then
the type $\mathop{\downarrow}_{\beta}x$ is small. Similarly to Remark 5.2, we
will use this tacitly and write as if the type $\mathop{\downarrow}_{\beta}x$
is actually a type in $\mathcal{V}$.

######  Lemma 5.14.

If a dcpo comes equipped with a small compact basis, then it can be equipped
with algebraicity data. Hence, if a dcpo has an unspecified small compact
basis, then it is algebraic.

###### Proof.

For every element $x$ of a dcpo $D$ with a small compact basis $\beta:B\to D$,
the family $\mathop{\downarrow}_{\beta}x\to D$ consists of compact elements
and approximates $x$, so the assignment $x\mapsto\mathop{\downarrow}_{\beta}x$
is algebraicity data for $D$. ∎

Actually, with suitable assumptions, we can get canonical algebraicity data
from an unspecified small compact basis, as discussed in detail in Section
5.3. This observation relies on Proposition 5.16 below and we prefer to
present examples of dcpos with small compact bases first (Section 5.2).

######  Lemma 5.15.

A map $\beta:B\to D$ is a small compact basis for a dcpo $D$ if and only if
$\beta$ is a small basis for $D$ and $\beta(b)$ is compact for every $b:B$.

###### Proof.

If $\beta(b)$ is compact for every $b:B$, then
$\beta(b)\mathrel{\sqsubseteq}x$ if and only if $\beta(b)\ll x$ for every
$b:B$ and $x:D$, so that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x\simeq\mathop{\downarrow}_{\beta}x$
for every $x:D$. In particular,
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$
approximates $x$ if and only if $\mathop{\downarrow}_{\beta}x$ does, which
completes the proof. ∎

######  Proposition 5.16.

A small compact basis contains every compact element. That is, if $\beta:B\to
D$ is a small compact basis for a dcpo $D$ and $x:D$ is compact, then there
exists $b:B$ such that $\beta(b)=x$.

###### Proof.

Suppose we have a compact element $x:D$. By compactness of $x$ and the fact
that $x=\mathop{\downarrow}_{\beta}x$, there exists $b:B$ with $\beta(b)\ll x$
such that $x\mathrel{\sqsubseteq}\beta(b)$. But then $\beta(b)=x$ by
antisymmetry. ∎

###  5.2. Examples of dcpos with small compact bases

Armed with the theory of small bases we turn to examples illustrating small
bases in practice. Our examples will involve small _compact_ bases and an
example of a dcpo with a small basis that is not compact will have to wait
until Section 6.2 when we have developed the ideal completion.

######  Example 5.17.

The map $\beta:\mathbf{2}\to\Omega_{\mathcal{U}}$ defined by
$0\mapsto\mathbf{0}_{\mathcal{U}}$ and $1\mapsto\mathbf{1}_{\mathcal{U}}$ is a
small compact basis for $\Omega_{\mathcal{U}}$. In particular,
$\Omega_{\mathcal{U}}$ is algebraic.

The basis $\beta:\mathbf{2}\to\Omega_{\mathcal{U}}$ defined above has the
special property that it is _dense_ in the sense of [Esc+,
TypeTopology.Density]: its image has empty complement, i.e. the type
$\Sigma_{P:\Omega_{\mathcal{U}}}\lnot\left(\Sigma_{b:\mathbf{2}}\,\beta(b)=P\right)$
is empty.

###### Proof of Example 5.17.

By Example 2.5, every element in the image of $\beta$ is compact. Moreover,
$\Omega_{\mathcal{U}}$ is locally small, so we only need to prove that for
every $P:\Omega_{\mathcal{U}}$ the family $\mathop{\downarrow}_{\beta}P$ is
directed with supremum $P$. The domain of the family is inhabited, because
$\beta(0)$ is the least element. Semidirectedness also follows easily, since
$\mathbf{2}$ has only two elements for which we have
$\beta(0)\mathrel{\sqsubseteq}\beta(1)$. Finally, the supremum of
$\mathop{\downarrow}_{\beta}P$ is obviously below $P$. Conversely, if $P$
holds, then $\bigsqcup{\mathop{\downarrow}_{\beta}P}=\mathbf{1}=P$. The final
claim follows from Lemma 5.14. ∎

######  Example 5.18.

For a set $X:\mathcal{U}$, the map
$\beta:\left(\mathbf{1}+X\right)\to\operatorname{\mathcal{L}}_{\mathcal{U}}(X)$
given by $\operatorname{inl}(\star)\mapsto\bot$ and
$\operatorname{inr}(x)\mapsto\eta(x)$ is a small compact basis for
$\operatorname{\mathcal{L}}_{\mathcal{U}}(X)$. In particular,
$\operatorname{\mathcal{L}}_{\mathcal{U}}(X)$ is algebraic.

Similar to Example 5.17, the basis
$\beta:(\mathbf{1}+X)\to\operatorname{\mathcal{L}}_{\mathcal{U}}(X)$ defined
above is also dense.

###### Proof of Example 5.18.

By Example 2.6, every element in the image of $\beta$ is compact. Moreover,
the lifting is locally small, so we only need to prove that for every partial
element $l$, the family $\mathop{\downarrow}_{\beta}l$ is directed with
supremum $l$. The domain of the family is inhabited, because
$\beta(\operatorname{inl}(\star))$ is the least element. Semidirectedness also
follows easily: First of all, $\beta(\operatorname{inl}(\star))$ is the least
element. Secondly, if we have $x,x^{\prime}:X$ such that
$\beta(\operatorname{inr}(x)),\beta(\operatorname{inr}(x^{\prime}))\mathrel{\sqsubseteq}l$,
then because $\beta(\operatorname{inr}(x))\equiv\eta(x)$ is defined, we must
have $\beta(\operatorname{inr}(x))=l=\beta(\operatorname{inr}(x^{\prime}))$ by
definition of the order. Finally, the supremum of
$\mathop{\downarrow}_{\beta}l$ is obviously a partial element below $l$.
Conversely, if $l$ is defined, then $l=\eta(x)$ for some $x:X$, and hence,
$l=\eta(x)\mathrel{\sqsubseteq}\bigsqcup\mathop{\downarrow}_{\beta}l$. The
final claim follows from Lemma 5.14. ∎

######  Example 5.19.

For a set $X:\mathcal{U}$, the map
$\beta:\operatorname{List}(X)\to\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$
from Definition 2.12 (whose image is the type of Kuratowski finite subsets of
$X$) is a small compact basis for
$\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$. In particular,
$\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$ is algebraic.

###### Proof of Example 5.19.

By Lemmas 2.13 and 2.14, all elements in the image of $\beta$ are compact.
Moreover, $\operatorname{\mathcal{P}}_{\mathcal{U}}(X)$ is locally small, so
we only need to prove that for every $A:\operatorname{\mathcal{P}}(X)$ the
family $\mathop{\downarrow}_{\beta}A$ is directed with supremum $A$, but this
was also proven in Example 2.14. The final claim follows from Lemma 5.14. ∎

At this point the reader may ask whether we have any examples of dcpos which
can be equipped with algebraicity data but that do not have a small compact
basis. The following example shows that this can happen in our predicative
setting:

######  Example 5.20.

The lifting $\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$ of a proposition
$P:\mathcal{U}$ can be given algebraicity data, but has a small compact basis
if and only if $P$ is $\mathcal{V}$-small.

Thus, requiring that $\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$ has a small
basis for every proposition $P:\mathcal{U}$ is equivalent to the propositional
resizing principle that every proposition in $\mathcal{U}$ is equivalent to
one in $\mathcal{V}$.

###### Proof of Example 5.20.

Note that $\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$ is simply the type of
propositions in $\mathcal{V}$ that imply $P$. It has algebraicity data,
because given such a proposition $Q$, the family

$\displaystyle Q+\mathbf{1}_{\mathcal{V}}$
$\displaystyle\to\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$
$\displaystyle\operatorname{inl}(q)$
$\displaystyle\mapsto\mathbf{1}_{\mathcal{V}}$
$\displaystyle\operatorname{inr}(\star)$
$\displaystyle\mapsto\mathbf{0}_{\mathcal{V}}$

is directed, has supremum $Q$ and consists of compact elements. But if
$\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$ had a small compact basis
$\beta:B\to\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$, then we would have
$P\simeq\exists_{b:B}\left(\beta(b)\simeq\mathbf{1}_{\mathcal{V}}\right)$ and
the latter is $\mathcal{V}$-small. Conversely, if $P$ is equivalent to
$P_{0}:\mathcal{V}$, then $\operatorname{\mathcal{L}}_{\mathcal{V}}(P)$ is
isomorphic to $\operatorname{\mathcal{L}}_{\mathcal{V}}(P_{0})$, which has a
small compact basis by Example 5.18. ∎

######  Example 5.21.

The ordinals in univalent foundations, as introduced in [Uni13, Section 10.3]
and further developed by the second author in [Esc+18], give an example of a
large (even impredicatively) algebraic sup-lattice without a small basis. In
[dJE23, Theorem 5.8] we showed that the large poset of small ordinals has
small suprema, so indeed the ordinals form a sup-lattice111This result needs
small set quotients, or equivalently, set replacement; see Section 5.3 for a
discussion of set replacement.. Moreover, they cannot have a small basis, as
otherwise we could take the supremum of all ordinals in the basis which would
yield a greatest ordinal which does not exist (as a consequence of [Uni13,
Lemma 10.3.21]).

It remains to show that the sup-lattice of ordinals is algebraic. This follows
from the following two facts.

  1. (i)

Every successor ordinal, i.e. one of the form $\alpha+\mathbf{1}$, is compact.

  2. (ii)

Every ordinal $\alpha$ is the supremum of the family
$x:\alpha\mapsto\alpha\mathbin{\downarrow}x+\mathbf{1}$, where
$\alpha\mathbin{\downarrow}x$ denotes the ordinal of elements of $\alpha$ that
are strictly less than $x$.

While the family in (ii) is not necessarily directed, this does not pose a
problem, since we can take its directification (see Definition 7.10 later) by
considering finite joins of elements in the family which are necessarily
compact again by Lemma 2.7.

For proving these facts, we recall from [Esc+18, Ordinals.OrdinalOfOrdinals]
that the order $\preceq$ on ordinals can be characterised as follows:

$\alpha\preceq\beta\quad\iff\quad\forall_{x:\alpha}\exists_{y:\beta}\,\alpha\mathbin{\downarrow}x=\beta\mathbin{\downarrow}y.$

We now prove (i): Suppose that
$\alpha+\mathbf{1}\preceq\bigsqcup_{i:I}\beta_{i}$. Since
$\alpha=(\alpha+\mathbf{1})\mathbin{\downarrow}\operatorname{inr}(\star)$,
there exists $s:\bigsqcup_{i:I}\beta_{i}$ with
$\alpha=\bigsqcup_{i:I}\beta_{i}\mathbin{\downarrow}s$. By [dJon+23, Lemma 15]
there exist $j:I$ and $b:\beta_{j}$ with
${\bigsqcup_{i:I}\beta_{i}}\mathbin{\downarrow}s=\beta_{j}\mathbin{\downarrow}b$.
Hence, $\alpha=\beta_{j}\mathbin{\downarrow}b$, but then it follows that
$\alpha+\mathbf{1}\preceq\beta_{j}$.

To see that (ii) is true, we first notice that
${\alpha\mathbin{\downarrow}x+\mathbf{1}}\preceq\alpha$ holds (using the
characterisation of the partial order) so that $\alpha$ is an upper bound for
the family. Now suppose that $\beta$ is another upper bound. We need to show
that $\alpha\preceq\beta$. So let $x:\alpha$ be arbitrary. Since $\beta$ is an
upper bound of the family, there is $b:\beta$ with
$\alpha\mathbin{\downarrow}x=(\alpha\mathbin{\downarrow}x+\mathbf{1})\mathbin{\downarrow}\operatorname{inr}\star=\beta\mathbin{\downarrow}b$,
so we are done.

###  5.3. The basis of compact elements

So far, our development of algebraic dcpos (with small compact bases) has
resulted from specialising the treatment of continuous dcpos with small bases.
In this section we take a closer look at the algebraic case.

Classically, the subset $K$ of compact elements of an algebraic dcpo $D$ forms
a basis for $D$. In our predicative context, we only consider small bases, and
a priori there is no reason for $K$ to be a small type. However, if $D$ comes
equipped with a small compact basis, then set replacement implies that $K$ is
in fact small.

We recall the _set replacement_ principle from [dJE23, Definition 3.27]: it
asserts that the image of a map $f:X\to Y$ is
${\mathcal{U}\sqcup\mathcal{V}}$-small if $X$ is $\mathcal{U}$-small and $Y$
is a locally $\mathcal{V}$-small set, where local smallness refers to
smallness of the identity types. We also recall [dJE23, Theorem 3.29] that set
replacement is logically equivalent to the existence of small set quotients.

If we additionally assume univalence, then the relevant smallness condition is
a property [dJE23, Section 2.3], which means that having an unspecified small
compact basis is sufficient.

In particular, with set replacement and univalence, we can show:

$\displaystyle\|$ $\displaystyle D\text{ has a specified small compact
basis}\|\to$ $\displaystyle D\text{ has a specified small compact basis}$

Using the terminology of [Kra+17, Definition 3.9], we may thus say that the
type expressing that $D$ has a specified small compact basis has split
support. This observation is due to Ayberk Tosun (private communication) who
also formalised the result for spectrality in the context of locale theory in
predicative univalent foundations [AET24, Theorem 4.17].

######  Lemma 5.22.

Every element $x$ of an algebraic dcpo is the directed supremum of all compact
elements below $x$.

###### Proof.

Writing $D$ for the algebraic dcpo, and letting $x:D$ be arbitrary, we have to
show that the inclusion family

$\iota_{x}:\left(\Sigma_{c:D}\left(c\text{ is
compact}\right)\times\left(c\mathrel{\sqsubseteq}x\right)\right)\to D$

is directed with supremum $x$. Since this is a proposition, we may assume to
be given algebraicity data for $D$. Thus, we have a directed family
$\kappa_{x}:I_{x}\to D$ of compact elements with supremum $x$. By
directedness, $I_{x}$ is inhabited, so we see that the domain of $\iota_{x}$
is inhabited too. For semidirectedness, assume we have compact elements
$c_{1},c_{2}:D$ below $x$. Since $x$ is the directed supremum of $\kappa_{x}$,
there exist elements $i_{1},i_{2}:I_{x}$ with
$c_{1}\mathrel{\sqsubseteq}\kappa_{x}(i_{1})$ and
$c_{2}\mathrel{\sqsubseteq}\kappa_{x}(i_{2})$. By directedness of
$\kappa_{x}$, there then exists $i:I_{x}$ such that $c_{1}$ and $c_{2}$ are
both below $\kappa_{x}(i)$. But $\kappa_{x}(i)$ is a compact element below $x$
so we are done. Finally, we show that $\iota_{x}$ has supremum $x$. Clearly,
$x$ is an upper bound for $\iota_{x}$. Now suppose that $y$ is any other upper
bound. It then suffices to show that $\kappa_{x}(i)\mathrel{\sqsubseteq}y$ for
all $i:I_{x}$. But each $\kappa_{x}(i)$ is a compact element below $x$, so
this holds since $y$ is an upper bound for $\iota_{x}$. ∎

######  Lemma 5.23.

Assuming set replacement, if a $\mathcal{V}$-dcpo is equipped with a small
compact basis, then the subtype of compact elements is $\mathcal{V}$-small.

If we additionally assume univalence, then having an unspecified small compact
basis suffices.

###### Proof.

Let $\beta:B\to D$ be the small compact basis of the $\mathcal{V}$-dcpo $D$.
Notice that $\beta$ factors through the subtype $K$ of compact elements of
$D$. Moreover, by Proposition 5.16 the map $\beta:B\to K$ is surjective.
Hence, $K$ is equivalent to the image of $\beta:B\to D$. Now an application of
set replacement finishes the proof, since $B$ is small and $K$ is locally
small because it is a subtype of $D$ which is locally small by antisymmetry,
Propositions 5.5 and 5.15.

Assuming univalence, being small is a property [dJE23, Proposition 2.8], so
that the result follows from the above and the universal property of the
truncation. ∎

######  Proposition 5.24.

Assuming univalence and set replacement, the types expressing that a dcpo has
a specified, resp. unspecified, small compact basis are logically equivalent.

###### Proof.

In one direction, we simply apply the propositional truncation. In the other
direction, we apply Lemmas 5.22 and 5.23 to see that

${K_{s}}\simeq K\hookrightarrow D$

is a small compact basis for the $\mathcal{V}$-dcpo $D$, where $K$ denotes the
subtype of compact elements and $K_{s}$ is the $\mathcal{V}$-small copy of
$K$. ∎

We note that the above cannot be promoted to an equivalence of types, because
the type of specified small compact bases is not a proposition. This may seem
puzzling to a domain theorist because there is a unique basis— _as a subset_
—which consists of compact elements. If we had asked for the map $\beta:B\to
D$ in the definition of a small compact basis to be an embedding, then
(ignoring size issues for a moment) the resulting type is a proposition: it
has a unique element in case the dcpo is algebraic, given by the _subset_ of
compact elements. (This is true because any basis must contain all compact
elements.)

We illustrate why we do not impose this requirement by revisiting Example
5.19. This example showed that the canonical map from lists into the powerset
of a set $X$ is a small compact basis for the algebraic dcpo
$\operatorname{\mathcal{P}}(X)$. This map is not an embedding, as any
permutation of a list will give rise to the same subset. If we insisted on
having an embedding, we would instead have to use the inclusion of the
Kuratowski finite subsets $\mathcal{K}(X)$ into
$\operatorname{\mathcal{P}}(X)$. However, $\mathcal{K}(X)$ is not a small type
without additional assumptions, such as HITs or more specifically, set
replacement (as $\mathcal{K}(X)$ is precisely the image of the inclusion of
lists).

Returning to the main line of thought, we conclude that, in the presence of
set replacement and univalence, if there is some unspecified small compact
basis, then the subset of compact elements is small.

##  6\. The rounded ideal completion

We have seen that in continuous dcpos, the basis essentially “generates” the
whole dcpo, because the basis suffices to approximate any of its elements. It
is natural to ask whether one can start from a more abstract notion of basis
and “complete” it to a continuous dcpo. Following [AJ94] [AJ94, Section
2.2.6], but keeping track of size, this is exactly what we do here using the
notion of an _abstract basis_ and the _rounded ideal completion_.

######  Definition 6.1 (Abstract basis).

An _abstract $\mathcal{V}$-basis_ is a type $B:\mathcal{V}$ with a binary
relation ${\prec}:B\to B\to\mathcal{V}$ that is proposition-valued, transitive
and satisfies _nullary_ and _binary interpolation_ :

  1. (i)

for every $a:B$, there exists $b:B$ with $b\prec a$, and

  2. (ii)

for every $a_{1},a_{2}\prec b$, there exists $a:B$ with ${a_{1},a_{2}}\prec
a\prec b$.

######  Definition 6.2 (Ideal, (rounded) ideal completion,
$\mathcal{V}\\!\operatorname{-Idl}(B,\prec)$).

  1. (i)

A subset $I:\operatorname{\mathcal{P}}_{\mathcal{V}}(B)$ of an abstract
$\mathcal{V}$-basis $(B,{\prec})$ is a _$\mathcal{V}$ -ideal_ if it is a
directed lower set with respect to ${\prec}$. That it is a lower set means: if
$b\in I$ and $a\prec b$, then $a\in I$ too.

  2. (ii)

We write $\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ for the type of
$\mathcal{V}$-ideals of an abstract $\mathcal{V}$-basis $(B,{\prec})$ and call
$\mathcal{V}\\!\operatorname{-Idl}({B,\prec})$ the _(rounded) ideal
completion_ of $(B,\prec)$.

For the remainder of this section, we will fix an abstract $\mathcal{V}$-basis
$(B,{\prec})$ and consider its $\mathcal{V}$-ideals. The name rounded ideal
completion is justified by Lemmas 6.5 and 6.6 below.

######  Definition 6.3 (Union of ideals, $\bigcup\mathcal{I}$).

Given a family $\mathcal{I}:S\to\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$
of ideals, indexed by $S:\mathcal{V}$, we write

$\textstyle\bigcup\mathcal{I}\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\\{b\in
B\mid\exists_{s:S}\left(b\in\mathcal{I}_{s}\right)\\}.$

######  Lemma 6.4.

If $\mathcal{I}:S\to\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ is directed,
then $\bigcup\mathcal{I}$ is an ideal.

###### Proof.

The subset $\bigcup\mathcal{I}$ is easily seen to be a lower set, for if
$a\prec b\in\bigcup\mathcal{I}$, then there exists $s:S$ such that $a\prec
b\in\mathcal{I}_{s}$, so $a\in\mathcal{I}_{s}$ as $\mathcal{I}_{s}$ is a lower
set, but then $a\in\bigcup\mathcal{I}$. Moreover, $\bigcup\mathcal{I}$ is
inhabited: Since $\mathcal{I}$ is directed, there exists $s:S$, but
$\mathcal{I}_{s}$ is an ideal and therefore inhabited, so there exists
$b\in\mathcal{I}_{s}$ which implies $b\in\bigcup\mathcal{I}$. Finally, suppose
we have $b_{1},b_{2}\in\bigcup\mathcal{I}$. By definition, there exist
$s_{1},s_{2}:S$ such that $b_{1}\in\mathcal{I}_{s_{1}}$ and
$b_{2}\in\mathcal{I}_{s_{2}}$. By directedness of $S$, there exists $s:S$ such
that $\mathcal{I}_{s_{1}},\mathcal{I}_{s_{2}}\subseteq\mathcal{I}_{s}$. Hence,
$b_{1},b_{2}\in\mathcal{I}_{s}$, which is an ideal, so there exists
$b\in\mathcal{I}_{s}$ with $b_{1},b_{2}\prec b$. But then also
$b\in\bigcup\mathcal{I}$, which proves that $\bigcup\mathcal{I}$ is directed
and hence an ideal, completing the proof. ∎

######  Lemma 6.5.

The rounded ideal completion is a $\mathcal{V}$-dcpo when ordered by subset
inclusion.

###### Proof.

Since taking unions yields the least upper bound in the powerset, we only have
to prove that the union of ideals is again an ideal, but this is Lemma 6.4. ∎

Paying attention to the universe levels, the ideals form a large but locally
small $\mathcal{V}$-dcpo because
$\mathcal{V}\\!\operatorname{-Idl}(B,{\prec}):\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{V^{+}},\mathcal{V}}$.

######  Lemma 6.6 (Roundedness).

The ideals of an abstract basis are _rounded_ : for every element $a$ of an
ideal $I$, there exists $b\in I$ such that $a\prec b$.

###### Proof.

Because ideals are semidirected. ∎

Roundedness makes up for the fact that we have not required an abstract basis
to be reflexive. If it is, then (Section 6.1) the ideal completion is
algebraic.

######  Definition 6.7 (Principal ideal, $\mathop{\downarrow}b$).

The _principal ideal_ of an element $b:B$ is defined as the subset
$\mathop{\downarrow}b\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\\{a\in B\mid
a\prec b\\}$. Observe that the principal ideal is indeed an ideal: it is a
lower set by transitivity of ${\prec}$, and inhabited and semidirected
precisely by nullary and binary interpolation, respectively.

######  Lemma 6.8.

The assignment $b\mapsto\mathop{\downarrow}b$ is monotone, i.e. if $a\prec b$,
then $\mathop{\downarrow}a\subseteq\mathop{\downarrow}b$.

###### Proof.

By transitivity of ${\prec}$. ∎

######  Lemma 6.9.

Every ideal is the directed supremum of its principal ideals. That is, for an
ideal $I$, the family $\left(\Sigma_{b:B}\left(b\in
I\right)\right)\xrightarrow{b\mapsto\mathop{\downarrow}b}\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$
is directed and has supremum $I$.

###### Proof.

Since ideals are lower sets, we have $\mathop{\downarrow}b\subseteq I$ for
every $b\in I$. Hence, the union $\bigcup_{b\in I}\mathop{\downarrow}b$ is a
subset of $I$. Conversely, if $a\in I$, then by roundedness of $I$ there
exists $a^{\prime}\in I$ with $a\prec a^{\prime}$, so that $a\in\bigcup_{b\in
I}\mathop{\downarrow}b$. So it remains to show that the family is directed.
Notice that it is inhabited, because $I$ is an ideal. Now suppose that
$b_{1},b_{2}\in I$. Since $I$ is directed, there exists $b\in I$ such that
${b_{1},b_{2}}\prec b$. But this implies
${\mathop{\downarrow}b_{1},\mathop{\downarrow}b_{2}}\subseteq\mathop{\downarrow}b$
by Lemma 6.8, so the family is semidirected, as desired. ∎

######  Lemma 6.10.

The following are equivalent for every two ideals $I$ and $J$:

  1. (i)

$I\ll J$;

  2. (ii)

there exists $b\in J$ such that $I\subseteq\mathop{\downarrow}b$;

  3. (iii)

there exist $a\prec b$ such that
$I\subseteq\mathop{\downarrow}a\subseteq\mathop{\downarrow}b\subseteq J$.

In particular, if $b$ is an element of an ideal $I$, then
$\mathop{\downarrow}b\ll I$.

###### Proof.

We show that (i) $\Rightarrow$ (ii) $\Rightarrow$ (iii) $\Rightarrow$ (i). So
suppose that $I\ll J$. Then $J$ is the directed supremum of its principal
ideals by Lemma 6.9. Hence, there exists $b\in J$ such that
$I\subseteq\mathop{\downarrow}b$ already, which is exactly (ii). Now suppose
that we have $a\in J$ with $I\subseteq\mathop{\downarrow}a$. By roundedness of
$J$, there exists $b\in J$ with $a\prec b$. But then
$I\subseteq\mathop{\downarrow}a\subseteq\mathop{\downarrow}b\subseteq J$ by
Lemma 6.8 and the fact that $J$ is a lower set, establishing (iii). Now
suppose that condition (iii) holds and that $J$ is a subset of some directed
join of ideals $\mathcal{J}$ indexed by a type $S:\mathcal{V}$. Since
$a\in\mathop{\downarrow}b\subseteq J$, there exists $s:S$ such that
$a\in\mathcal{J}_{s}$. In particular,
$\mathop{\downarrow}a\subseteq\mathcal{J}_{s}$ because ideals are lower sets.
Hence, if $a^{\prime}\in I\subseteq\mathop{\downarrow}a$, then
$a^{\prime}\in\mathcal{J}_{s}$, so $I\subseteq\mathcal{J}_{s}$, which proves
that $I\ll J$.

Finally, if $b$ is an element of an ideal $I$, then $\mathop{\downarrow}b\ll
I$, because (ii) implies (i) and
$\mathop{\downarrow}b\subseteq\mathop{\downarrow}b$ obviously holds. ∎

######  Theorem 6.11.

The principal ideals
$\mathop{\downarrow}{(-)}:B\to\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$
yield a small basis for $\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$. In
particular, $\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ is continuous.

###### Proof.

First of all, note that the way-below relation on
$\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ is small-valued because of
Lemma 6.10. So it remains to show that for every ideal $I$, the family
$\left(\Sigma_{b:B}\left(\mathop{\downarrow}b\ll
I\right)\right)\xrightarrow{b\mapsto\mathop{\downarrow}b}\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$
is directed with supremum $I$. That the domain of this family is inhabited
follows from Lemma 6.10 and the fact that $I$ is inhabited. For
semidirectedness, suppose we have $b_{1},b_{2}:B$ with
${\mathop{\downarrow}b_{1},\mathop{\downarrow}b_{2}}\ll I$. By Lemma 6.10
there exist ${c_{1},c_{2}}\in I$ such that
$\mathop{\downarrow}b_{1}\subseteq\mathop{\downarrow}c_{1}$ and
$\mathop{\downarrow}b_{2}\subseteq\mathop{\downarrow}c_{2}$. Since $I$ is
directed, there exists $b\in I$ with ${c_{1},c_{2}}\prec b$. But now
$\mathop{\downarrow}b_{1}\subseteq\mathop{\downarrow}c_{1}\subseteq\mathop{\downarrow}b\ll
I$ by Lemmas 6.8 and 6.10 and similarly,
$\mathop{\downarrow}b_{2}\subseteq\mathop{\downarrow}b\ll I$. Hence, the
family is semidirected, as we wished to show. Finally, we show that $I$ is the
supremum of the family. If $b\in I$, then, since $I$ is rounded, there exists
$c\in I$ with $b\prec c$. Moreover, $\mathop{\downarrow}c\ll I$ by Lemma 6.10.
Hence, $b$ is included in the join of the family. Conversely, if we have $b:B$
with $\mathop{\downarrow}b\ll I$, then $\mathop{\downarrow}b\subseteq I$, so
$I$ is also an upper bound for the family. ∎

###  6.1. The rounded ideal completion of a reflexive abstract basis

If the relation of an abstract basis is reflexive, then we obtain an algebraic
dcpo, as we show now.

######  Lemma 6.12.

If ${\prec}:B\to B\to\mathcal{V}$ is proposition-valued, transitive and
reflexive, then $(B,{\prec})$ is an abstract basis.

###### Proof.

The interpolation properties for ${\prec}$ are easily proved when it is
reflexive. ∎

######  Lemma 6.13.

If an element $b:B$ is reflexive, i.e. $b\prec b$ holds, then $b\in I$ if and
only if $\mathop{\downarrow}b\subseteq I$ for every ideal $I$.

###### Proof.

The left-to-right implication holds because $I$ is a lower set and the
converse holds because $b\in\mathop{\downarrow}b$ as $b$ is assumed to be
reflexive. ∎

######  Lemma 6.14.

If $b:B$ is reflexive, then its principal ideal $\mathop{\downarrow}b$ is
compact.

###### Proof.

Suppose that we have $b:B$ such that $b\prec b$ holds and that
$\mathop{\downarrow}b\subseteq\bigcup\mathcal{I}$ for some directed family
$\mathcal{I}$ of ideals. By Lemma 6.13, we have $b\in\bigcup\mathcal{I}$,
which means that there exists $s$ in the domain of $\mathcal{I}$ such that
$b\in\mathcal{I}_{s}$. Using Lemma 6.13 once more, we see that
$\mathop{\downarrow}b\subseteq\mathcal{I}_{s}$, proving that
$\mathop{\downarrow}b$ is compact. ∎

######  Theorem 6.15.

If ${\prec}$ is reflexive, then the principal ideals
$\mathop{\downarrow}{(-)}:B\to\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$
yield a small _compact_ basis for
$\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$. In particular,
$\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ is algebraic.

###### Proof.

This follows from Theorems 6.11, 6.14 and 5.15. ∎

######  Theorem 6.16.

If $f:B\to D$ is a monotone map to a $\mathcal{V}$-dcpo $D$, then the map
$\bar{f}:\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})\to D$ defined by taking
an ideal $I$ to the supremum of the directed family
${f\circ{\operatorname{pr_{1}}}}:\left(\Sigma_{b:B}\left(b\in
I\right)\right)\to D$ is Scott continuous. Moreover, if ${\prec}$ is
reflexive, then $\bar{f}$ is the unique Scott continuous map making the
diagram

${B}$${D}$${\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})}$$\scriptstyle{f}$$\scriptstyle{\mathop{\downarrow}{(-)}}$$\scriptstyle{\bar{f}}$

commute.

###### Proof.

Note that ${f\circ{\operatorname{pr_{1}}}}:\left(\Sigma_{b:B}\left(b\in
I\right)\right)\to D$ is indeed a directed family, because $I$ is a directed
subset of $B$ and $f$ is monotone. For Scott continuity of $\bar{f}$, assume
that we have a directed family $\mathcal{I}$ of ideals indexed by
$S:\mathcal{V}$. We first show that $\bar{f}\left(\bigcup\mathcal{I}\right)$
is an upper bound of $\bar{f}\circ\mathcal{I}$. So let $s:S$ be arbitrary and
note that
$\bar{f}\left(\bigcup\mathcal{I}\right)\supseteq\bar{f}\left(\mathcal{I}_{s}\right)$
as soon as $\bar{f}\left(\bigcup\mathcal{I}\right)\mathrel{\sqsupseteq}f(b)$
for every $b\in\mathcal{I}_{s}$. But for such $b$ we have
$b\in\bigcup\mathcal{I}$, so this holds. Now suppose that $y$ is an upper
bound of $\bar{f}\circ\mathcal{I}$. To show that
$\bar{f}\left(\bigcup\mathcal{I}\right)\mathrel{\sqsubseteq}y$, it is enough
to prove that $f(b)\mathrel{\sqsubseteq}y$ for every $b\in\mathcal{I}$. But
for such $b$, there exists $s:S$ such that $b\in\mathcal{I}_{s}$ and hence,
$f(b)\mathrel{\sqsubseteq}\bar{f}\left(\mathcal{I}_{s}\right)\mathrel{\sqsubseteq}y$.

Finally, if ${\prec}$ is reflexive, then we prove that
$\bar{f}\left(\mathop{\downarrow}b\right)=f(b)$ for every $b:B$ by
antisymmetry. Since ${\prec}$ is assumed to be reflexive, we have
$b\in\mathop{\downarrow}b$ and therefore,
$f(b)\mathrel{\sqsubseteq}\bar{f}\left(\mathop{\downarrow}b\right)$.
Conversely, for every $c\prec b$ we have $f(c)\mathrel{\sqsubseteq}f(b)$ by
monotonicity of $f$ and hence,
$\bar{f}(\mathop{\downarrow}b)\mathrel{\sqsubseteq}f(b)$, as desired.
Uniqueness is proved easily, because if
$g:{\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})\to D}$ is Scott continuous
with $g(\mathop{\downarrow}b)=f(b)$, then for an arbitrary ideal $I$ we have
$g(I)=g(\bigcup_{b\in I}\mathop{\downarrow}b)=\bigcup_{b\in
I}g(\mathop{\downarrow}b)=\bigcup_{b\in I}f(b)\equiv\bar{f}(I)$ by Lemma 6.9
and Scott continuity of $g$. ∎

###  6.2. Example: the ideal completion of dyadics

We describe an example of a continuous dcpo, built using the ideal completion,
that is not algebraic. In fact, this dcpo has no compact elements at all.

We inductively define a type and an order representing dyadic rationals
$m/2^{n}$ in the interval $(-1,1)$ for integers $m,n$. This type is isomorphic
to the lower Dedekind reals extended with $\infty$. We could work with lower
Dedekind reals but we prefer the type of dyadics for its simplicity.

The intuition for the upcoming definitions is the following: Start with the
point $0$ in the middle of the interval (represented by _middle_ below). Then
consider the two functions (respectively represented by _left_ and _right_
below)

$\displaystyle l,r$ $\displaystyle:(-1,1)\to(-1,1)$ $\displaystyle l(x)$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}(x-1)/2$
$\displaystyle r(x)$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}(x+1)/2$

that generate the dyadic rationals. Observe that $l(x)<0<r(x)$ for every
$x:(-1,1)$. Accordingly, we inductively define the following types:

######  Definition 6.17 (Dyadics, $\mathbb{D}$, $\prec$).

The type of _dyadics_ $\mathbb{D}:\mathcal{U}_{0}$ is the inductive type with
these three constructors

$\operatorname{middle}:\mathbb{D}\quad\operatorname{left}:{\mathbb{D}\to\mathbb{D}}\quad\operatorname{right}:{\mathbb{D}\to\mathbb{D}}.$

We also inductively define
${\prec}:{\mathbb{D}\to\mathbb{D}\to\mathcal{U}_{0}}$ as

$\displaystyle\operatorname{middle}$ $\displaystyle\prec\operatorname{middle}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{0}$
$\displaystyle\quad{\operatorname{left}(x)}$
$\displaystyle\prec{\operatorname{middle}}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{1}$
$\displaystyle\quad{\operatorname{right}(x)}$
$\displaystyle\prec{\operatorname{middle}}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{0}$
$\displaystyle\operatorname{middle}$
$\displaystyle\prec{\operatorname{left}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{0}$
$\displaystyle{\operatorname{left}(x)}$
$\displaystyle\prec{\operatorname{left}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}{x\prec y}$
$\displaystyle{\operatorname{right}(x)}$
$\displaystyle\prec{\operatorname{left}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{0}$
$\displaystyle\operatorname{middle}$
$\displaystyle\prec{\operatorname{right}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{1}$
$\displaystyle{\operatorname{left}(x)}$
$\displaystyle\prec{\operatorname{right}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\mathbf{1}$
$\displaystyle{\operatorname{right}(x)}$
$\displaystyle\prec{\operatorname{right}(y)}$
$\displaystyle\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}{x\prec
y}.\\!\\!\\!\\!$

######  Lemma 6.18.

The type of dyadics is a set with decidable equality.

###### Proof.

Sethood follows from having decidable equality by Hedberg’s Theorem. To see
that $\mathbb{D}$ has decidable equality, one can use a standard inductive
proof. ∎

######  Definition 6.19 (Trichotomy, density, having no endpoints).

We say that a binary relation ${<}$ on a type $X$ is

  * •

_trichotomous_ if exactly one of $x<y$, $x=y$ or $y<x$ holds.

  * •

_dense_ if for every $x,y:X$, there exists some $z:X$ such that $x\prec z\prec
y$.

  * •

_without endpoints_ if for every $x:X$, there exist some $y,z:X$ with $y\prec
x\prec z$.

######  Lemma 6.20.

The relation ${\prec}$ on the dyadics is proposition-valued, transitive,
irreflexive, trichotomous, dense and without endpoints.

###### Proof.

That ${\prec}$ is proposition-valued, transitive, irreflexive and trichotomous
is all proven by a straightforward induction on the definition on
$\mathbb{D}$. That it has no endpoints is witnessed by the fact that for every
$x:\mathbb{D}$, we have

${\operatorname{left}x}\prec x\prec{\operatorname{right}x}$ ($\dagger$)

which is proven by induction on $\mathbb{D}$ as well. We spell out the
inductive proof that it is dense, making use of ($\dagger$ ‣ 6.2). Suppose
that $x\prec y$. Looking at the definition of the order, we see that we need
to consider five cases.

  * •

If $x=\operatorname{middle}$ and $y=\operatorname{right}y^{\prime}$, then we
have $x\prec\operatorname{right}(\operatorname{left}(y^{\prime}))\prec y$.

  * •

If $x=\operatorname{left}(x^{\prime})$ and $y=\operatorname{middle}$, then we
have $x\prec\operatorname{left}(\operatorname{right}(x^{\prime}))\prec y$.

  * •

If $x=\operatorname{left}(x^{\prime})$ and $y=\operatorname{right}y^{\prime}$,
then we have $x\prec\operatorname{middle}\prec y$.

  * •

If $x=\operatorname{right}(x^{\prime})$ and
$y=\operatorname{right}y^{\prime}$, then we have $x^{\prime}\prec y^{\prime}$
and therefore, by induction hypothesis, there exists $z^{\prime}:\mathbb{D}$
such that $x^{\prime}\prec z^{\prime}\prec y^{\prime}$. Hence,
$x\prec\operatorname{right}(z^{\prime})\prec y$.

  * •

If $x=\operatorname{left}(x^{\prime})$ and
$y=\operatorname{left}(y^{\prime})$, then $x^{\prime}\prec y^{\prime}$ and so,
by induction hypothesis, there exists $z^{\prime}:\mathbb{D}$ such that
$x^{\prime}\prec z^{\prime}\prec y^{\prime}$. Thus,
${x\prec\operatorname{left}(z^{\prime})\prec y}$. ∎

######  Proposition 6.21.

The pair $(\mathbb{D},{\prec})$ is an abstract $\mathcal{U}_{0}$-basis.

###### Proof.

By Lemma 6.20 the relation ${\prec}$ is proposition-valued and transitive.
Moreover, that it has no endpoints implies unary interpolation. For binary
interpolation, suppose that we have $x\prec z$ and $y\prec z$. Then by
trichotomy there are three cases.

  * •

If $x=y$, then using density and our assumption that $x\prec z$, there exists
$d:\mathbb{D}$ with $y=x\prec d\prec z$, as desired.

  * •

If $x\prec y$, then using density and our assumption that $y\prec z$, there
exists $d:\mathbb{D}$ with $y\prec d\prec z$, but then also $x\prec d$ since
$x\prec y$, so we are done.

  * •

If $x\prec y$, then the proof is similar to that of the second case. ∎

######  Proposition 6.22.

The ideal completion
$\mathcal{U}_{0}\\!\operatorname{-Idl}(\mathbb{D},{\prec}):{\mathcal{U}_{0}}\\!\operatorname{-DCPO}_{\mathcal{U}_{1},\mathcal{U}_{0}}$
is continuous with small basis
$\mathop{\downarrow}(-):\mathbb{D}\to\mathcal{U}_{0}\\!\operatorname{-Idl}(\mathbb{D},{\prec})$.
Moreover, it cannot be algebraic, because none of its elements are compact.

###### Proof.

The first claim follows from Theorem 6.11. Now suppose for a contradiction
that we have a compact ideal $I$. By Lemma 6.10, there exists $x\in I$ with
$I\subseteq\mathop{\downarrow}x$. But this implies $x\prec x$, which is
impossible as ${\prec}$ is irreflexive. ∎

###  6.3. Ideal completions of small bases

Given a $\mathcal{V}$-dcpo $D$ with a small basis $\beta:B\to D$, we show that
there are two natural ways of turning $B$ into an abstract basis. Either
define $b\prec c$ by $\beta(b)\ll\beta(c)$, or by
$\beta(b)\mathrel{\sqsubseteq}\beta(c)$. Taking their $\mathcal{V}$-ideal
completions we show that the former yields a continuous dcpo isomorphic to
$D$, while the latter yields an algebraic dcpo (with a small compact basis) in
which $D$ can be embedded. The latter fact will find application in Section
7.2, while the former gives us a presentation theorem: every dcpo with a small
basis is isomorphic to a dcpo of ideals. In particular, if
$D:\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{U},\mathcal{T}}$ has a small
basis, then it is isomorphic to a dcpo with simpler universe parameters,
namely
$\mathcal{V}\\!\operatorname{-Idl}\left(B,{\ll_{\beta}}\right):\mathcal{V}\\!\operatorname{-DCPO}_{\mathcal{V^{+}},\mathcal{V}}$.
Of course a similar result holds for dcpos with a small compact basis. In
studying these variations, it is helpful to first develop some machinery that
all of them have in common.

Fix a $\mathcal{V}$-dcpo $D$ with a small basis $\beta:B\to D$. In what
follows we conflate the family
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x:\left(\Sigma_{b:B}\left(\beta(b)\ll
x\right)\right)\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D$ with its
associated subset ${\\{b\in B\mid\beta(b)\ll x\\}}$, formally given by the map
$B\to\Omega_{\mathcal{V}}$ defined as $b\mapsto\exists_{b:B}\left(\beta(b)\ll
x\right)$.

######  Lemma 6.23.

The assignment
$x:D\mapsto\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x:\operatorname{\mathcal{P}}(B)$
is Scott continuous.

###### Proof.

Note that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}(-)$ is
monotone: if $x\mathrel{\sqsubseteq}y$ and $b:B$ is such that $\beta(b)\ll x$,
then also $\beta(b)\ll y$. So it suffices to prove that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\left(\bigsqcup\alpha\right)\subseteq\bigcup_{i:I}\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{\alpha_{i}}$.
So suppose that $b:B$ is such that $\beta(b)\ll\bigsqcup\alpha$. By Lemma 5.7,
there exists $c:B$ with $\beta(b)\ll\beta(c)\ll\bigsqcup\alpha$. Hence, there
exists $i:I$ such that $\beta(b)\ll\beta(c)\mathrel{\sqsubseteq}\alpha_{i}$
already, and therefore,
$b\in\bigcup_{j:J}\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{\alpha_{j}}$,
as desired. ∎

By virtue of the fact that $\beta$ is a small basis for $D$, we know that
taking the directed supremum of
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ equals
$x$ for every $x:D$. In other words,
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{(-)}$ is
a section of $\bigsqcup{(-)}$. The following lemma gives conditions for the
other composite to be an inflation or a deflation.

######  Lemma 6.24.

Let $I:\operatorname{\mathcal{P}}_{\mathcal{V}}(B)$ be a subset of $B$ such
that its associated family ${\bar{I}:\left(\Sigma_{b:B}\left(b\in
I\right)\right)\xrightarrow{\beta\circ{\operatorname{pr_{1}}}}D}$ is directed.

  1. (i)

If the conjunction of $\beta(b)\mathrel{\sqsubseteq}\beta(c)$ and $c\in I$
implies $b\in I$, then
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\bigsqcup\bar{I}\subseteq
I$.

  2. (ii)

If for every $b\in I$ there exists $c\in I$ such that $\beta(b)\ll\beta(c)$,
then
$I\subseteq\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\bigsqcup\bar{I}$.

In particular, if both conditions hold, then
$I=\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\bigsqcup\bar{I}$.

Note that the first condition says that $I$ is a lower set with respect to the
order of $D$, while the second says that $I$ is rounded with respect to the
way-below relation.

###### Proof.

(i) Suppose that $I$ is a lower set and let $b:B$ be such that
$\beta(b)\ll\bigsqcup\bar{I}$. Then there exists $c\in I$ with
$\beta(b)\mathrel{\sqsubseteq}\beta(c)$, which implies $b\in I$ as desired,
because $I$ is assumed to be a lower set. (ii) Assume that $I$ is rounded and
let $b\in I$ be arbitrary. By roundedness of $I$, there exists $c\in I$ such
that $\beta(b)\ll\beta(c)$. But then
$\beta(b)\ll\beta(c)\mathrel{\sqsubseteq}\bigsqcup\bar{I}$, so that
$b\in\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\bigsqcup\bar{I}$,
as we wished to show. ∎

######  Lemma 6.25.

Suppose that we have ${\prec}:B\to B\to\mathcal{V}$ and let $x:D$ be
arbitrary.

  1. (i)

If $b\prec c$ implies $\beta(b)\mathrel{\sqsubseteq}\beta(c)$ for every
$b,c:B$, then
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is a
lower set w.r.t. ${\prec}$.

  2. (ii)

If $\beta(b)\ll\beta(c)$ implies $b\prec c$ for every $b,c:B$, then
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is
semidirected w.r.t. $\prec$.

###### Proof.

(i) This is immediate, because
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}{\beta}x$ is a
lower set with respect to the order relation on $D$. (ii) Suppose that the
condition holds and that we have ${b_{1},b_{2}}:B$ such that
$\beta(b_{1}),\beta(b_{2})\ll x$. Using binary interpolation in the basis,
there exist ${c_{1},c_{2}}:B$ with $\beta(b_{1})\ll\beta(c_{1})\ll x$ and
$\beta(b_{2})\ll\beta(c_{2})\ll x$. Hence,
$c_{1},c_{2}\in\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta
x}$ and moreover, by assumption we have $b_{1}\prec c_{1}$ and $b_{2}\prec
c_{2}$, as desired. ∎

####  6.3.1. Ideal completion with respect to the way-below relation

######  Lemma 6.26.

If $\beta:B\to D$ is a small basis for a $\mathcal{V}$-dcpo $D$, then
$\left(B,\ll_{\beta}\right)$ is an abstract $\mathcal{V}$-basis where
$b\ll_{\beta}c$ is defined as $\beta(b)\ll\beta(c)$.

######  Remark 6.27.

The definition of an abstract $\mathcal{V}$-basis requires the relation on it
to be $\mathcal{V}$-valued. Hence, for the lemma to make sense we appeal to
the fact that $\beta$ is a _small_ basis which tells us that we can substitute
$\beta(b)\ll\beta(c)$ by an equivalent type in $\mathcal{V}$.

###### Proof of Lemma 6.26.

The way-below relation is proposition-valued and transitive. Moreover,
${\ll_{\beta}}$ satisfies nullary and binary interpolation precisely because
we have nullary and binary interpolation in the basis for the way-below
relation by Lemmas 5.6 and 5.8. ∎

The following theorem is a presentation result for dcpos with a small basis:
every such dcpo can be presented as the rounded ideal completion of its small
basis.

######  Theorem 6.28.

The map
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{(-)}:D\to\mathcal{V}\\!\operatorname{-Idl}\left(B,{\ll_{\beta}}\right)$
is an isomorphism of $\mathcal{V}$-dcpos.

###### Proof.

First of all, we should check that the map is well-defined, i.e. that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is an
$\left(B,{\ll_{\beta}}\right)$-ideal. It is an inhabited subset by nullary
interpolation in the basis and a semidirected lower set because the criteria
of Lemma 6.25 are satisfied when taking ${\prec}$ to be ${\ll_{\beta}}$.
Secondly, the map
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{(-)}$ is
Scott continuous by Lemma 6.23.

Now notice that the map $\beta:\left(B,{\ll_{\beta}}\right)\to D$ is monotone
and that the Scott continuous map it induces by Theorem 6.16 is exactly the
map
$\bigsqcup:\mathcal{V}\\!\operatorname{-Idl}\left(B,{\ll_{\beta}}\right)\to D$
that takes an ideal $I$ to the supremum of its associated directed family
$\beta\circ{\operatorname{pr_{1}}}:\left(\Sigma_{b:B}\left(b\in
I\right)\right)\to D$.

Since $\beta$ is a basis for $D$, we know that
$\bigsqcup{\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x}=x$
for every $x:D$. So it only remains to show that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\circ\bigsqcup$
is the identity on
$\mathcal{V}\\!\operatorname{-Idl}\left(B,{\ll_{\beta}}\right)$, for which we
will use Lemma 6.24. So suppose that
$I:\mathcal{V}\\!\operatorname{-Idl}\left(B,{\ll_{\beta}}\right)$ is
arbitrary. Then we only need to prove that

  1. (i)

the conjunction of $\beta(b)\mathrel{\sqsubseteq}\beta(c)$ and $c\in I$
implies $b\in I$ for every $b,c:B$;

  2. (ii)

for every $b\in I$, there exists $c\in I$ such that $\beta(b)\ll\beta(c)$.

Note that (ii) is just saying that $I$ is a rounded ideal w.r.t.
${\ll_{\beta}}$, so this holds. For (i), suppose that
$\beta(b)\mathrel{\sqsubseteq}\beta(c)$ and $c\in I$. By roundedness of $I$,
there exists $c^{\prime}\in I$ such that $c\ll_{\beta}c^{\prime}$. But then
$\beta(b)\mathrel{\sqsubseteq}\beta(c)\ll\beta(c^{\prime})$, so that
$b\ll_{\beta}c^{\prime}$ which implies that $b\in I$, because ideals are lower
sets. ∎

####  6.3.2. Ideal completion with respect to the order relation

######  Lemma 6.29.

If $\beta:B\to D$ is a small basis for a $\mathcal{V}$-dcpo $D$, then
$\left(B,\mathrel{\sqsubseteq}_{\beta}\right)$ is an abstract
$\mathcal{V}$-basis where $b\mathrel{\sqsubseteq}_{\beta}c$ is defined as
$\beta(b)\mathrel{\sqsubseteq}\beta(c)$.

###### Proof.

The relation ${\mathrel{\sqsubseteq}_{\beta}}$ is reflexive, so this follows
from Lemma 6.12. ∎

######  Remark 6.30.

The definition of an abstract $\mathcal{V}$-basis requires the relation on it
to be $\mathcal{V}$-valued. Hence, for the lemma to make sense we appeal to
Proposition 5.5 to know that $D$ is locally small which tells us that we can
substitute $\beta(b)\mathrel{\sqsubseteq}\beta(c)$ by an equivalent type in
$\mathcal{V}$.

######  Theorem 6.31.

The map
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{(-)}:D\to\mathcal{V}\\!\operatorname{-Idl}\left(B,{\mathrel{\sqsubseteq}_{\beta}}\right)$
is the embedding in an embedding-projection pair. In particular, $D$ is a
Scott continuous retract of the algebraic dcpo
$\mathcal{V}\\!\operatorname{-Idl}\left(B,\mathrel{\sqsubseteq}_{\beta}\right)$
that has a small compact basis. Moreover, if $\beta$ is a small _compact_
basis, then the map is an isomorphism.

###### Proof.

First of all, we should check that the map is well-defined, i.e. that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x$ is an
$\left(B,{\mathrel{\sqsubseteq}_{\beta}}\right)$-ideal. It is an inhabited
subset by nullary interpolation in the basis and a semidirected lower set
because the criteria of Lemma 6.25 are satisfied when taking ${\prec}$ to be
${\mathrel{\sqsubseteq}_{\beta}}$. Secondly, the map
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}{(-)}$ is
Scott continuous by Lemma 6.23.

Now notice that the map
$\beta:\left(B,{\mathrel{\sqsubseteq}_{\beta}}\right)\to D$ is monotone and
that the continuous map it induces by Theorem 6.16 is exactly the map
$\bigsqcup:\mathcal{V}\\!\operatorname{-Idl}\left(B,{\mathrel{\sqsubseteq}_{\beta}}\right)\to
D$ that takes an ideal $I$ to the supremum of the directed family
${\beta\circ{\operatorname{pr_{1}}}:{\left(\Sigma_{b:B}\left(b\in
I\right)\right)\to D}}$.

Since $\beta$ is a basis for $D$, we know that
$\bigsqcup{\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}x}=x$
for every $x:D$. So it only remains to show that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\circ\bigsqcup$
is a deflation, for which we will use Lemma 6.24. So suppose that
$I:\mathcal{V}\\!\operatorname{-Idl}\left(B,{\mathrel{\sqsubseteq}_{\beta}}\right)$
is arbitrary. Then we only need to prove that the conjunction of
$\beta(b)\mathrel{\sqsubseteq}\beta(c)$ and $c\in I$ implies $b\in I$, but
this holds, because $I$ is a lower set with respect to
${\mathrel{\sqsubseteq}_{\beta}}$.

Finally, assume that $\beta$ is a small compact basis. We show that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta}\circ\bigsqcup$
is also inflationary in this case. So let $I$ be an arbitrary ideal. By Lemma
6.24 it is enough to show that for every $b\in I$, there exists $c\in I$ such
that $\beta(b)\ll\beta(c)$. But by assumption, $\beta(b)$ is compact, so we
can simply take $c$ to be $b$. ∎

Combining Theorem 5.10, Theorems 6.11 and 6.28, and Theorems 6.31 and 6.15, we
obtain the following result:

######  Corollary 6.32.

  1. (i)

A $\mathcal{V}$-dcpo has a small basis if and only if it is isomorphic to
$\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ for an abstract basis
$(B,{\prec})$.

  2. (ii)

A $\mathcal{V}$-dcpo has a small compact basis if and only if it is isomorphic
to $\mathcal{V}\\!\operatorname{-Idl}(B,{\prec})$ for an abstract basis
$(B,{\prec})$ where ${\prec}$ is reflexive.

  3. (iii)

A $\mathcal{V}$-dcpo has a small basis if and only if it is a Scott continuous
retract of a $\mathcal{V}$-dcpo with a small compact basis.

In particular, every $\mathcal{V}$-dcpo with a small basis is isomorphic to
one whose order takes values in $\mathcal{V}$ and whose carrier lives in
$\mathcal{V}^{+}$.

##  7\. Bilimits and exponentials

###  7.1. Structurally continuous and algebraic bilimits

We show that bilimits are closed under equipment with continuity/algebraicity
data. For the reminder of this section, fix a directed diagram of
$\mathcal{V}$-dcpos $(D_{i})_{i:I}$ with embedding-projection pairs
$\left(\varepsilon_{i,j},\pi_{i,j}\right)_{i\mathrel{\sqsubseteq}j\text{ in
}I}$ between them, as in Section 7 of Part I. We stress that, throughout this
section, the word “embedding” is only used in the domain-theoretic sense, i.e.
it is reserved for one half of an embedding-projection pair, rather than in
the homotopy type theory sense of having subsingleton fibers.

Now suppose that for every $i:I$, we have $\alpha_{i}:J_{i}\to D_{i}$ with
each $J_{i}:\mathcal{V}$. Then we define
$J_{\infty}\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\Sigma_{i:I}J_{i}$ and
$\alpha_{\infty}:J_{\infty}\to D_{\infty}$ by
$(i,j)\mapsto\varepsilon_{i,\infty}(\alpha_{i}(j))$, where
$\varepsilon_{i,\infty}$ is as in Definition 7.12 of Part I.

######  Lemma 7.1.

If every $\alpha_{i}$ is directed and we have $\sigma:D_{\infty}$ such that
$\alpha_{i}$ approximates $\sigma_{i}$, then $\alpha_{\infty}$ is directed and
approximates $\sigma$.

###### Proof.

Observe that $\alpha_{\infty}$ is equal to the supremum, if it exists, of the
directed families $\left(\varepsilon_{i,\infty}\circ\alpha_{i}\right)_{i:I}$
in the ind-completion of $D_{\infty}$, cf. the proof of Lemma 3.3. Hence, for
directedness of $\alpha_{\infty}$, it suffices to prove that the family
$i\mapsto\varepsilon_{i,\infty}\circ\alpha_{i}$ is directed with respect to
the exceeds-relation. The index type $I$ is inhabited, because we are working
with a directed diagram of dcpos. For semidirectedness, we will first prove
that if $i\mathrel{\sqsubseteq}i^{\prime}$, then
$\varepsilon_{i^{\prime},\infty}\circ\alpha_{i^{\prime}}$ exceeds
$\varepsilon_{i,\infty}\circ\alpha_{i}$.

So suppose that $i\mathrel{\sqsubseteq}i^{\prime}$ and $j:J_{i}$. As
$\alpha_{i}$ approximates $\sigma_{i}$, we have $\alpha_{i}(j)\ll\sigma_{i}$.
Because $\varepsilon_{i,i^{\prime}}$ is an embedding, it preserves the way-
below relation (Lemma 2.16), so that we get
$\varepsilon_{i,i^{\prime}}(\alpha_{i}(j))\ll\varepsilon_{i,i^{\prime}}(\sigma_{i})\mathrel{\sqsubseteq}\sigma_{i^{\prime}}=\bigsqcup\alpha_{i^{\prime}}$.
Hence, there exists $j^{\prime}:J_{i^{\prime}}$ with
$\varepsilon_{i,i^{\prime}}(\alpha_{i}(j))\mathrel{\sqsubseteq}\alpha_{i^{\prime}}(j^{\prime})$
which yields
$\varepsilon_{i,\infty}(\alpha_{i}(j))=\varepsilon_{i^{\prime},\infty}\left(\varepsilon_{i,i^{\prime}}(\alpha_{i}(j))\right)\mathrel{\sqsubseteq}\varepsilon_{i^{\prime},\infty}(\alpha_{i^{\prime}}(j^{\prime}))$,
completing the proof that
$\varepsilon_{i^{\prime},\infty}\circ\alpha_{i^{\prime}}$ exceeds
$\varepsilon_{i,\infty}\circ\alpha_{i}$.

Now to prove that the family $i\mapsto\varepsilon_{i,\infty}\circ\alpha_{i}$
is semidirected with respect to the exceeds-relation, suppose we have
$i_{1},i_{2}:I$. Since $I$ is a directed preorder, there exists $i:I$ such
that $i_{1},i_{2}\mathrel{\sqsubseteq}i$. But then
$\varepsilon_{i,\infty}\circ\alpha_{i}$ exceeds both
$\varepsilon_{i_{1},\infty}\circ\alpha_{i_{1}}$ and
$\varepsilon_{i_{2},\infty}\circ\alpha_{i_{2}}$ by the above.

Thus, $\alpha_{\infty}$ is directed. To see that its supremum is $\sigma$,
observe that

$\displaystyle\sigma$
$\displaystyle=\textstyle\bigsqcup_{i:I}\varepsilon_{i,\infty}(\sigma_{i})$
(by Lemma 7.19 of Part I)
$\displaystyle=\textstyle\bigsqcup_{i:I}\varepsilon_{i,\infty}\left(\textstyle\bigsqcup\alpha_{i}\right)$
(since $\alpha_{i}$ approximates $\sigma_{i}$)
$\displaystyle=\textstyle\bigsqcup_{i:I}\bigsqcup\varepsilon_{i,\infty}\circ\alpha_{i}$
(by Scott continuity of $\varepsilon_{i,\infty}$)
$\displaystyle=\textstyle\bigsqcup_{(i,j):J_{\infty}}\alpha_{\infty}(i,j),$

as desired.

Finally, we wish to show that $\alpha_{\infty}(i,j)\ll\sigma$ for every
$(i,j):J_{\infty}$. But $\varepsilon_{i,\infty}$ is an embedding and therefore
preserves the way-below relation while $\alpha_{i}(j)$ approximates
$\sigma_{i}$, so we get
$\alpha_{\infty}(i,j)\equiv\varepsilon_{i,\infty}(\alpha_{i}(j))\ll\varepsilon_{i,\infty}(\sigma_{i})\mathrel{\sqsubseteq}\sigma$
where the final inequality holds because
$\varepsilon_{i,\infty}\circ\pi_{i,\infty}$ is a deflation. ∎

######  Lemma 7.2.

If $\alpha_{i}(j)$ is compact for every $i:I$ and $j:J_{i}$, then all the
values of $\alpha_{\infty}$ are compact too.

###### Proof.

Let $(i,j):J_{\infty}$ be arbitrary. Since $\varepsilon_{i,\infty}$ is an
embedding it preserves compact elements, so
$\alpha_{\infty}(i,j)\equiv\varepsilon_{i,\infty}(\alpha_{i}(j))$ is compact.
∎

######  Theorem 7.3.

If each $D_{i}$ comes equipped with continuity (resp. algebraicity) data, then
we can give continuity (resp. algebraicity) data for $D_{\infty}$.

###### Proof.

Let $\sigma:D_{\infty}$ be arbitrary. By assumption on each $D_{i}$, we have a
directed family $\alpha_{i}:J_{i}\to D_{i}$ approximating $\sigma_{i}$. Hence,
by Lemma 7.1, the family $\alpha_{\infty}$ is directed and approximates
$\sigma$, giving continuity data for $D_{\infty}$. For the algebraic case, we
apply the above and Lemma 7.2. ∎

Note that we do not expect to be able to prove that $D_{\infty}$ is continuous
if each $D_{i}$ is, because it would require an instance of the axiom of
choice to get continuity data on each $D_{i}$, and without those we have
nothing to operate on.

######  Theorem 7.4.

If each $D_{i}$ has a small basis $\beta_{i}:B_{i}\to D_{i}$, then the map

$\displaystyle\beta_{\infty}:\left(B_{\infty}\mathrel{\vcentcolon\mspace{-1.2mu}\equiv}\Sigma_{i:I}B_{i}\right)$
$\displaystyle\to$ $\displaystyle D_{\infty}$ $\displaystyle(i,b)$
$\displaystyle\mapsto$ $\displaystyle\varepsilon_{i,\infty}(\beta_{i}(b))$

is a small basis for $D_{\infty}$. Furthermore, if each $\beta_{i}$ is a small
compact basis, then $\beta_{\infty}$ is a small compact basis too.

###### Proof.

First of all, we must show that the proposition $\beta_{\infty}(i,b)\ll\sigma$
is small for every $i:I$, $b:B_{i}$ and $\sigma:D_{\infty}$. We claim that
this is the case as the way-below relation on $D_{\infty}$ has small values.
By Proposition 4.12 and Theorem 7.3, it suffices to prove that $D_{\infty}$ is
locally small. But this holds by Proposition 7.22 of Part I as each $D_{i}$ is
locally small by Proposition 5.5.

It remains to prove that, for an arbitrary element $\sigma:D_{\infty}$, the
family
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta_{\infty}}\sigma$
given by
$\left(\Sigma_{(i,b):B_{\infty}}\beta_{\infty}(i,b)\ll\sigma\right)\xrightarrow{\beta_{\infty}\circ{\operatorname{pr_{1}}}}D_{\infty}$
is directed with supremum $\sigma$. Note that for every $i:I$ and $b:B_{i}$,
we have that $\beta_{i}(b)\ll\sigma_{i}$ implies

$\beta_{\infty}(i,b)\equiv\varepsilon_{i,\infty}(\beta_{i}(b))\ll\varepsilon_{i,\infty}(\sigma_{i})\mathrel{\sqsubseteq}\sigma,$

since Lemma 2.16 tells us that the embedding $\varepsilon_{i,\infty}$
preserves the way-below relation. Hence, the identity map induces a well-
defined map

$\iota:\left(\Sigma_{i:I}\Sigma_{b:B_{i}}\beta_{i}(b)\ll\sigma_{i}\right)\to\left(\Sigma_{(i,b):B_{\infty}}\beta_{\infty}(i,b)\ll\sigma\right).$

Lemma 5.9 now tells us that we only need to show that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta_{\infty}}\sigma\circ\iota$
is directed and has supremum $\sigma$. But if we write
$\alpha_{i}:\left(\Sigma_{b:B_{i}}\beta_{i}(b)\ll\sigma_{i}\right)\to D_{i}$
for the map $b\mapsto\beta_{i}(b)$, then we see that
$\mathop{\rotatebox[origin={c}]{270.0}{$\twoheadrightarrow$}}_{\beta_{\infty}}\sigma\circ\iota$
is given by $\alpha_{\infty}$ defined from $\alpha_{i}$ as in the start of
this section. But then $\alpha_{\infty}$ is indeed seen to be directed with
supremum $\sigma$ by virtue of Lemma 7.1 and the fact that $\alpha_{i}$
approximates $\sigma_{i}$.

Finally, if every $\beta_{i}$ is a small compact basis, then $\beta_{\infty}$
is also a small compact basis because by Lemma 5.15 all we need to know is
that $\beta_{\infty}(i,b)\equiv\varepsilon_{i,\infty}(\beta_{i}(b))$ is
compact for every $i:I$ and $b:B_{i}$. But this follows from the fact that
embeddings preserve compactness and that each $\beta_{i}(b)$ is compact. ∎

###  7.2. Exponentials with small (compact) bases

Just as in the classical, impredicative setting, the exponential of two
continuous dcpos need not be continuous [Jun89]. However, with some work, we
are able to show that $E^{D}$ has a small basis provided that both $D$ and $E$
do and that $E$ has all (not necessarily directed) $\mathcal{V}$-suprema, that
is, $E$ is a continuous lattice. We first establish this for small compact
bases using _step functions_ and then derive the result for compact bases
using Theorem 6.31.

####  7.2.1. Single step functions

Suppose that we have a dcpo $D$ and a pointed dcpo $E$. Classically [Gie+03,
Exercise II-2.31], the single step function given by $d:D$ and $e:E$ is
defined as

$\displaystyle\llparenthesis d\Rightarrow e\rrparenthesis:D$ $\displaystyle\to
E$ $\displaystyle x$ $\displaystyle\mapsto\begin{cases}e&\text{if
$d\mathrel{\sqsubseteq}x$;}\\\ \bot&\text{otherwise}.\end{cases}$

Constructively, we can’t expect to make this case distinction in general, so
we define single step functions using subsingleton suprema instead.

######  Definition 7.5 (Single step function, $\llparenthesis d\Rightarrow
e\rrparenthesis$).

The _single step function_ given by two elements $d:D$ and $e:E$, where $D$ is
a locally small $\mathcal{V}$-dcpo and $E$ is a pointed $\mathcal{V}$-dcpo, is
the function $\llparenthesis d\Rightarrow e\rrparenthesis:D\to E$ that maps a
given $x:D$ to the supremum of the family indexed by the subsingleton
$d\mathrel{\sqsubseteq}x$ that is constantly $e$.

Note that we need the domain $D$ to be locally small, because we need the type
$d\mathrel{\sqsubseteq}x$ to be a subsingleton in $\mathcal{V}$ to use the
$\mathcal{V}$-directed-completeness of $E$. For the definition of
$\llparenthesis d\Rightarrow e\rrparenthesis$ to make sense, we need to know
that the supremum of the constant family exists. This is the case by Lemma 4.9
of Part I, which says that the supremum of a subsingleton-indexed family
$\alpha:{P\to E}$ is given by the supremum of the directed family
$\mathbf{1}+P\to E$ defined by $\operatorname{inl}(\star)\mapsto\bot$ and
$\operatorname{inr}(p)\mapsto\alpha(p)$.

######  Lemma 7.6.

If $d:D$ is compact, then $\llparenthesis d\Rightarrow e\rrparenthesis$ is
Scott continuous for every $e:E$.

###### Proof.

Suppose that $d:D$ is compact and that $\alpha:I\to D$ is a directed family.
We first show that $\llparenthesis d\Rightarrow
e\rrparenthesis\left(\bigsqcup\alpha\right)$ is an upper bound of
$\llparenthesis d\Rightarrow e\rrparenthesis\circ\alpha$. So let $i:I$ be
arbitrary. Then we have to prove
$\bigsqcup_{d\mathrel{\sqsubseteq}\alpha_{i}}e\mathrel{\sqsubseteq}\bigsqcup{\llparenthesis
d\Rightarrow e\rrparenthesis\circ\alpha}$. Since the supremum gives a lower
bound of the upper bounds, it suffices to prove that
$e\mathrel{\sqsubseteq}\bigsqcup{\llparenthesis d\Rightarrow
e\rrparenthesis\circ\alpha}$ whenever $d\mathrel{\sqsubseteq}\alpha_{i}$. But
in this case we have $e=\llparenthesis d\Rightarrow
e\rrparenthesis(\alpha_{i})\mathrel{\sqsubseteq}\bigsqcup{\llparenthesis
d\Rightarrow e\rrparenthesis\circ\alpha}$, so we are done.

To see that $\llparenthesis d\Rightarrow
e\rrparenthesis\left(\bigsqcup\alpha\right)$ is a lower bound of the upper
bounds, suppose that we are given $y:E$ such that $y$ is an upper bound of
$\llparenthesis d\Rightarrow e\rrparenthesis\circ\alpha$. We are to prove that
$\left(\bigsqcup_{d\mathrel{\sqsubseteq}\bigsqcup\alpha}e\right)\mathrel{\sqsubseteq}y$.
Note that it suffices for $d\mathrel{\sqsubseteq}\bigsqcup\alpha$ to imply
$e\mathrel{\sqsubseteq}y$. So assume that
$d\mathrel{\sqsubseteq}\bigsqcup\alpha$. By compactness of $d$ there exists