# Constructing Initial Algebras Using Inflationary Iteration

Andrew M. Pitts S. C. Steenkamp Department of Computer Science and Technology
University of Cambridge, UK<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

An old theorem of Adámek constructs initial algebras for sufficiently
cocontinuous endofunctors via transfinite iteration over ordinals in classical
set theory. We prove a new version that works in constructive logic, using
“inflationary” iteration over a notion of _size_ that abstracts from limit
ordinals just their transitive, directed and well-founded properties.
Borrowing from Taylor’s constructive treatment of ordinals, we show that sizes
exist with upper bounds for any given signature of indexes. From this it
follows that there is a rich class of endofunctors to which the new theorem
applies, provided one admits a weak form of choice (WISC) due to Streicher,
Moerdijk, van den Berg and Palmgren, and which is known to hold in the
internal constructive logic of many kinds of elementary topos.

##  1 Introduction

Initial algebras for endofunctors are a simple category-theoretic concept that
has proved very useful in logic and computer science. Recall that an _initial
algebra_ $(\mu F,\iota)$ for an endofunctor
$F:\mathcal{C}\rightarrow\mathcal{C}$ on a category $\mathcal{C}$, is a
morphism $\iota:F(\mu F)\rightarrow\mu F$ in $\mathcal{C}$ with the property
that for any morphism $a:F(A)\rightarrow A$, there is a unique $\hat{a}:\mu
F\rightarrow A$ that is an $F$-algebra morphism, that is, satisfies
$\hat{a}\circ\iota=a\circ F(\hat{a})$. In functional programming, $\hat{a}$ is
sometimes called the _catamorphism_ associated with the algebra $(A,a)$ [24].
By varying the choice of $\mathcal{C}$ and $F$, such initial algebras give
semantics for various kinds of inductive (or dually, coinductive) structures
and, via their catamorphisms, associated (co)recursion schemes. We refer the
reader to the draft book by Adámek, Milius, and Moss [7] for an account of
this within classical logic.

Here we make a contribution to the existence of initial algebras within
_constructive_ logics. Our motivation for doing so is not philosophical, nor
motivated by the computational insights that a constructive approach can
bring, important though both those thing are. Rather, we are interested in the
semantics of dependent type theories with inductive constructions, such as
types that are inductive [23], inductive-recursive [12], inductive-inductive
[16], quotient (inductive-)inductive [10, 20] and more generally higher-
inductive [38]. Toposes are often used when constructing models of such type
theories and sometimes the easiest way of doing so is to use their “internal
logic” [19, Part D] to express the constructions; see [28, 22], for example.
Although there are different candidates for what is the internal logic of
toposes, in general they are not classical. So we are led to ask for what
categories $\mathcal{C}$ and functors $F:\mathcal{C}\rightarrow\mathcal{C}$
that are describable in such an internal logic is it the case that an initial
$F$-algebra can be constructed?

We pursue this question by developing a constructive version of Adámek’s
classical theorem about existence of initial algebras via transfinite
iteration over ordinals [5] (we discuss a different constructive approach [6]
in Section 5). Recall, or see Adámek et al. [7, section 6.1] for example, that
if $F:\mathcal{C}\rightarrow\mathcal{C}$ is an endofunctor on a category
$\mathcal{C}$ with all small colimits (colimits of small chains is enough),
then we get a large chain in $\mathcal{C}$,
$(F^{\alpha}0)_{\\_}{\alpha\in\mathsf{Ord}}$ indexed by the totally ordered
class of ordinals $\mathsf{Ord}$, defined by recursion over the ordinals:

$F^{\alpha}0=\begin{cases}0\quad\text{(initial object in
$\mathcal{C}$)}&\text{if $\alpha=0$, the ordinal zero}\\\
F(F^{\beta}0)&\text{if $\alpha=\beta^{+}$ is a successor ordinal}\\\
\operatorname{\mathrm{colim}}_{\\_}{\beta<\lambda}F^{\beta}0&\text{if
$\alpha=\lambda$ is a limit ordinal}\end{cases}$ (1)

The links in the chain are $\mathcal{C}$-morphisms
$i_{\\_}\alpha:F^{\alpha}0\rightarrow F^{\alpha^{+}}0$ also defined by ordinal
recursion:

$i_{\\_}\alpha=\begin{cases}\text{unique morphism given by initiality of
$0$}&\text{if $\alpha=0$, the ordinal zero}\\\ F(i_{\\_}\beta)&\text{if
$\alpha=\beta^{+}$ is a successor ordinal}\\\ \text{induced by the universal
property of colimits}&\text{if $\alpha=\lambda$ is a limit
ordinal}\end{cases}$ (2)

######  Theorem 1.1 ([classical] (Adámek [5])).

If $i_{\\_}\alpha$ is an isomorphism for some $\alpha\in\mathsf{Ord}$, then
$(F^{\alpha}0,i_{\\_}\alpha^{-1})$ is an initial algebra for
$F:\mathcal{C}\rightarrow\mathcal{C}$. So in particular, if $F$ preserves
colimits of shape $\lambda$ for some limit ordinal $\lambda$, then (by
definition of “preserves colimits”) $i_{\\_}\lambda$ is an isomorphism and
$F^{\lambda}0$ is an initial $F$-algebra.

This theorem is labelled [classical] because its proof uses classical logic:
the properties of ordinal numbers that it relies upon require the Law of
Excluded Middle ($\forall p.\;p\vee\neg p$). In Section 3 we show that by
replacing the use of ordinals with a weaker notion of “size” and modifying the
way $F$ is iterated, one can obtain a constructive version of Adámek’s theorem
(see Theorem 3.8).

Not only the proof, but also the application of Adámek’s theorem can require
classical logic: the Axiom of Choice [ac] is often invoked to find a suitably
large limit ordinal $\lambda$ for which a particular functor of interest
preserves $\lambda$-colimits. Such uses of [ac] are not always necessary. In
particular, existence of initial algebras for polynominal functors
$F_{\\_}{A,B}(\\_)=\sum_{\\_}{a\in
A}(\\_)^{B(a)}:\mathbf{Set}\rightarrow\mathbf{Set}$ (where $A\in\mathbf{Set}$
and $B\in\mathbf{Set}^{A}$) can be proved constructively; see [25, Proposition
3.6]. These initial algebras are the categorical analogue of W-types [2, 17]
and we will make use of the fact that they exist in toposes with natural
number object in what follows. However, for non-polynomial functors,
especially ones whose specification involves both exponentiation by infinite
sets and taking quotients by equivalence relations (such as Example 4.14
below), it is not immediately clear that [ac] can be avoided. In fact, we show
in Section 4 that a much weaker choice principle than [ac], the “Weakly
Initial Sets of Covers” [wisc] axiom [33, 25, 39] is enough to ensure that our
constructive version of Adámek’s theorem applies to a rich class of
endofunctors. [wisc] has been called “constructively acceptable” because it is
valid in a wide range of elementary toposes [39]. In particular it holds in
presheaf and realizability toposes that have been used to construct models of
dependent type theory that mix quotients and inductive constructions, which,
as we mentioned above, motivates our desire for a constructive treatment of
initial algebras.

##  2 Constructive meta-theory

The results in this paper are presented in the usual informal language of
mathematics, but only making use of intuitionistically valid logical
principles (and, to obtain the results of Section 4, extended by the WISC
axiom). In particular we avoid use of the Law of Excluded Middle, or more
generally the Axiom of Choice.

More specifically, our results can be soundly interpreted in any elementary
topos with natural number object and universes [34] (satisfying [wisc], for
the last part of the paper). Thus when we refer to the category $\mathbf{Set}$
of small sets and functions, we mean the generalised elements of some such
universe, which we always assume contains the subobject classifier. In fact,
in order to interpret quantification over such small sets in a straightforward
way, we tacitly assume there is a countable nested sequence of such universes,
$\mathbf{Set}=\mathbf{Set}_{\\_}0\in\mathbf{Set}_{\\_}1\in\cdots$. A suitable
version of Martin-Löf’s Extensional Type Theory [23] extended with an
impredicative universe of propositions can be used as the internal language of
such toposes.

In fact the use of impredicative quantification is not necessary: we have
developed a formalisation of the results of this paper using the Agda [9]
proof assistant, which can provide a dependent type theory with a predicative
universe of (proof irrelevant) propositions and convenient mechanisms (such as
pattern-matching) for using inductively defined types. We then have to
postulate as axioms some things which are derivable in the logic of toposes,
namely axioms for propositional extensionality, quotient sets and unique
choice (and [wisc], when we need it). Our Agda development is available at
[29].

##  3 Size-indexed inflationary iteration

Throughout this section we fix a large, locally small category111The
collection of objects is in $\mathbf{Set}_{\\_}1$ and the collection of
morphisms between any pair of objects is in $\mathbf{Set}$. $\mathcal{C}$ and
an endofunctor $F:\mathcal{C}\rightarrow\mathcal{C}$. We will consider
sequences of objects in $\mathcal{C}$ built up by iterating $F$ while taking
certain colimits. For simplicity we assume that $\mathcal{C}$ is cocomplete,
that is, has colimits of all small diagrams.222This means that we are given a
function assigning a choice of colimit for each small diagram, since we work
in a constructive setting and in particular have to avoid use of the Axiom of
Choice.

From a constructive point of view, the problem with the sequence (1) is that
it makes use of ordinals, which rely on the Law of Excluded Middle [lem] for
their good properties; in particular, the definition in (1) is by cases
according to whether an ordinal is zero, or a successor, _or not_. In the case
that $\mathcal{C}$ is a complete partially ordered set (with joins denoted by
$\bigvee$), Abel and Pientka [4, section 4.5] point out that one can avoid
this case distinction, while still achieving within constructive logic the
same result in the (co)limit, by instead taking the approach of Sprenger and
Dam [32] and using what they term an _inflationary iteration_ :

$\mu_{\\_}iF=\textstyle\bigvee_{\\_}{j<i}F(\mu_{\\_}jF)$ (3)

We only need $i$ to range over the elements of a set equipped with a binary
relation $<$ that is well-founded for this definition to make sense. Here we
generalise from complete posets to cocomplete categories, replacing joins by
colimits. Definition 3.2 sums up what we need of the indexes $i$ and the
relation $<$ between them in order to ensure that the inflationary sequence
can be defined and yields an initial algebra for $F$ if it becomes stationary
up to isomorphism.

######  Definition 3.1.

Recall that a _semi-category_ is like a category, but lacks identity
morphisms. A semi-category is _thin_ if there is at most one morphism between
any pair of objects. Thus a small thin semi-category is the same thing as a
set $\kappa$ (the set of objects) equipped with a transitive relation
$\\_<\\_\subseteq\kappa\times\kappa$ (the existence-of-a-morphism relation).
Given such a $(\kappa,{<})$, a _diagram_ $D:\kappa\rightarrow\mathcal{C}$ in a
category $\mathcal{C}$ is by definition a semi-functor from $\kappa$ to
$\mathcal{C}$: thus $D$ maps each $i\in\kappa$ to a $\mathcal{C}$-object
$D_{\\_}i$, each pair $(j,i)$ with $j<i$ to a $\mathcal{C}$-morphism
$D_{\\_}{j,i}:D_{\\_}j\rightarrow D_{\\_}i$, and these morphisms satisfy
$D_{\\_}{j,i}\circ D_{\\_}{k,j}=D_{\\_}{k,i}$ for all $k<j<i$ in $\kappa$.

######  Definition 3.2.

A _size_ is a small thin semi-category $(\kappa,{<})$ that is

  * •

_directed_ : every finite subset of $\kappa$ has an upper bound with respect
to $<$; specifically, we assume we are given a distinguished element
$0^{s}\in\kappa$ and a binary operation
$\\_\mathbin{\sqcup^{s}}\\_:\kappa\times\kappa\rightarrow\kappa$ satisfying
$\forall
i,j\in\kappa.\;i<{i\mathbin{\sqcup^{s}}j}\;\wedge\;j<{i\mathbin{\sqcup^{s}}j}$

  * •

_well-founded_ : for all $K\subseteq\kappa$, if $\forall i\in\kappa.(\forall
j<i.\;j\in K)\Rightarrow i\in K$, then $K=\kappa$.

Note that the directedness property in particular gives a successor operation
$\mathop{\uparrow^{s}}:\kappa\rightarrow\kappa$ on the elements of a size,
defined by $\mathop{\uparrow^{s}}i\triangleq i\mathbin{\sqcup^{s}}i$ and
satisfying $\forall i\in\kappa.\;i<\mathop{\uparrow^{s}}i$. (We do not need a
successor that also preserves $<$, although the sizes constructed in the next
section have one that does so.)

######  Example 3.3.

In the next section we will define a rich class of sizes derived from
algebraic signatures (see Proposition 4.2). For now, we note that the natural
numbers $\mathbb{N}$ with their usual strict order is a size.333$\mathbb{N}$
will be the smallest size once one has developed a comparison relation between
sizes. To do that one probably has to restrict to sizes that are _extensional_
, that is, satisfy $\forall i,j\in\kappa.\;\\{k\in\kappa\mid
k<i\\}=\\{k\in\kappa\mid k<j\\}\Rightarrow i=j$. However, we have no need of
that property for the results in this paper. In classical logic, an ordinal is
a size iff its usual strict total order is directed, which happens iff it is a
limit ordinal.

######  Remark 3.4.

Since we are working constructively, the well-foundedness property of a size
is stated in a suitably positive form; classically, it is equivalent to the
non-existence of infinite descending chains for $<$. Well-foundedness of $<$
allows one to define size-indexed families by _well-founded recursion_ [37,
section 6.3]: given a size $\kappa$ and a $\kappa$-indexed family of sets
$(A_{\\_}i)_{\\_}{i\in\kappa}$, from each family of functions
$(f_{\\_}i:(\prod_{\\_}{j<i}A_{\\_}j)\rightarrow A_{\\_}i)_{\\_}{i\in\kappa}$
we get a family of elements $(a_{\\_}i\in A_{\\_}i)_{\\_}{i\in\kappa}$,
uniquely defined by the requirement $\forall
i\in\kappa.\;a_{\\_}i=f_{\\_}i((a_{\\_}j)_{\\_}{j<i})$.

Given a size $\kappa$, for each element $i\in\kappa$ we get a small thin semi-
category444Well-foundedness is preserved, but directedness is not, so
${\downarrow}(i)$ is not necessarily a size. ${\downarrow}(i)$ whose vertices
are the elements $j\in\kappa$ with $j<i$ and whose morphisms are the instances
of the $<$ relation. Thus a diagram $D:{\downarrow}(i)\rightarrow\mathcal{C}$
maps each $j<i$ to a $\mathcal{C}$-object $D_{\\_}j$ and each pair $(k,j)$
with $k<j<i$ to a $\mathcal{C}$-morphism $D_{\\_}{k,j}:D_{\\_}k\rightarrow
D_{\\_}j$, satisfying $D_{\\_}{k,j}\circ D_{\\_}{l,k}=D_{\\_}{l,j}$ for all
$l<k<j<i$. We write

$(\mathrm{inc}^{D}_{\\_}j:D_{\\_}j\rightarrow\operatorname{\mathrm{colim}}_{\\_}{j<i}D_{\\_}j)_{\\_}{j<i}$
(4)

for the colimit of this diagram (recall that we are assuming $\mathcal{C}$ is
cocomplete). Thus for all $k<j<i$ it is the case that
$\mathrm{inc}^{D}_{\\_}k=\mathrm{inc}^{D}_{\\_}j\circ D_{\\_}{k,j}$; and given
any cocone in $\mathcal{C}$

$(f_{\\_}j:D_{\\_}j\rightarrow X)_{\\_}{j<i}\qquad\forall
k<j<i.\;f_{\\_}k=f_{\\_}j\circ D_{\\_}{k,j}$

there is a unique $\mathcal{C}$-morphism
$\hat{f}:\operatorname{\mathrm{colim}}_{\\_}{j<i}D_{\\_}j\rightarrow X$
satisfying $\forall j<i.\;\hat{f}\circ\mathrm{inc}^{D}_{\\_}j=f_{\\_}j$.

Since $<$ is transitive, if $j<i$ in $\kappa$, then ${\downarrow}(j)$ is a
sub-semi-category of ${\downarrow}(i)$ and each diagram
$D:{\downarrow}(i)\rightarrow\mathcal{C}$ restricts to a diagram
$D|_{\\_}j:{\downarrow}(j)\rightarrow\mathcal{C}$. We write

$\mathrm{c}^{D}_{\\_}{j,i}:\operatorname{\mathrm{colim}}_{\\_}{k<j}D_{\\_}k\rightarrow\operatorname{\mathrm{colim}}_{\\_}{k<i}D_{\\_}k$
(5)

for the unique $\mathcal{C}$-morphism satisfying $\forall
k<j<i.\;\mathrm{c}^{D}_{\\_}{j,i}\circ\mathrm{inc}^{D|_{\\_}j}_{\\_}k=\mathrm{inc}^{D}_{\\_}k$.

######  Definition 3.5.

Let $\kappa$ be a size. Given an endofunctor
$F:\mathcal{C}\rightarrow\mathcal{C}$ on a cocomplete category $\mathcal{C}$,
a diagram $D:\kappa\rightarrow\mathcal{C}$ is an _inflationary iteration of
$F$ over $\kappa$_ if for all $i\in\kappa$

$D_{\\_}i=\operatorname{\mathrm{colim}}_{\\_}{j<i}F(D_{\\_}j)\;\wedge\;\forall
j<i.\;D_{\\_}{j,i}=\mathrm{c}^{F\circ D}_{\\_}{j,i}$

######  Lemma 3.6.

Given an endofunctor $F:\mathcal{C}\rightarrow\mathcal{C}$ on a cocomplete
category $\mathcal{C}$, for each size $\kappa$ the inflationary iteration of
$F$ over $\kappa$ exists (and is unique).

###### Proof.

Given $i\in\kappa$, say that a diagram
$D:{\downarrow}(i)\rightarrow\mathcal{C}$ is an inflationary iteration of $F$
_up to_ $i$ if for all $j<i$,
$D_{\\_}j=\operatorname{\mathrm{colim}}_{\\_}{k<j}F(D_{\\_}k)$ and $\forall
k<j.\;D_{\\_}{k,j}=\mathrm{c}^{F\circ D}_{\\_}{k,j}$. Note that given such a
diagram, for any $j<i$ we have that
$D|_{\\_}j:{\downarrow}(j)\rightarrow\mathcal{C}$ is an inflationary iteration
of $F$ up to $j$. Using well-founded induction for $<$, one can prove that

$\forall i\in\kappa,\;\text{any two inflationary iterations of $F$ up to $i$
are equal}$ (6)

Then one can use well-founded recursion for $<$ (Remark 3.4) to define for
each $i\in\kappa$ an inflationary iteration of $F$ up to $i$,
$D^{(i)}:{\downarrow}(i)\rightarrow\mathcal{C}$. If $j<i$, then $D^{(j)}$ and
$D^{(i)}|_{\\_}j$ are both inflationary iterations of $F$ up to $j$ and so are
equal by (6). From this it follows that

$(D_{\\_}i\triangleq\operatorname{\mathrm{colim}}_{\\_}{j<i}F(D^{(i)}_{\\_}j))_{\\_}{i\in\kappa}\;\wedge\;(D_{\\_}{j,i}\triangleq\mathrm{c}^{F\circ
D^{(i)}}_{\\_}{j,i})_{\\_}{j,i\in\kappa\mid j<i}$

defines an inflationary iteration of $F$. (Furthermore, since any such
restricts to an up-to-$i$ inflationary iteration, uniqueness follows from
(6).) ∎

######  Remark 3.7.

We record some simple properties of inflationary iteration that we need in the
proof of the theorem below. Let $D:\kappa\rightarrow\mathcal{C}$ be the
inflationary iteration of $F:\mathcal{C}\rightarrow\mathcal{C}$ over $\kappa$.
Note that for all $j<i$ in $\kappa$, the components of the colimit cocone
$\mathrm{inc}^{F\circ
D|_{\\_}i}_{\\_}j:F(D_{\\_}j)\rightarrow\operatorname{\mathrm{colim}}_{\\_}{j<i}F(D_{\\_}j)$
are morphisms $\iota_{\\_}{j,i}:F(D_{\\_}j)\rightarrow D_{\\_}i$ satisfying

$\forall
k<j<i.\;D_{\\_}{j,i}\circ\iota_{\\_}{k,j}=\iota_{\\_}{k,i}=\iota_{\\_}{j,i}\circ
F(D_{\\_}{k,j})$ (7)

The first equation follows from the fact that $D_{\\_}{j,i}=\mathrm{c}^{F\circ
D}_{\\_}{j,i}$ and the second from the definition of $\iota_{\\_}{j,i}$ as a
component of a cocone. Since that cocone is colimiting, one also has for all
$i\in\kappa$ and all $\mathcal{C}$-morphisms $f,g:D_{\\_}i\rightarrow X$ that

$(\forall j<i.\;f\circ\iota_{\\_}{j,i}=g\circ\iota_{\\_}{j,i})\Rightarrow f=g$
(8)

The proof of Lemma 3.6 only used the transitive and well-founded properties of
the relation $<$ on a size $\kappa$, whereas the following theorem needs its
directedness property as well.

######  Theorem 3.8 ((Initial algebras via inflationary iteration)).

Suppose $\mathcal{C}$ is a cocomplete category,
$F:\mathcal{C}\rightarrow\mathcal{C}$ is an endofunctor and there is a size
$\kappa$ such that $F$ preserves colimits of diagrams
$\kappa\rightarrow\mathcal{C}$. Then $F$ has an initial algebra whose
underlying $\mathcal{C}$-object is the colimit $\mu
F=\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}\mu_{\\_}iF$ of the
inflationary iteration $\mu_{\\_}iF$ (Definition 3.5) of $F$ over $\kappa$.

###### Proof.

By Lemma 3.6 there is an inflationary iteration of
$F:\mathcal{C}\rightarrow\mathcal{C}$ over $\kappa$; call it
$D:\kappa\rightarrow\mathcal{C}$ and define $\mu
F\triangleq\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i$. For each
$i\in\kappa$, as in Definition 3.2 we have $\mathop{\uparrow^{s}}i\in\kappa$
with $i<\mathop{\uparrow^{s}}i$ and hence a $\mathcal{C}$-morphism

$\iota_{\\_}i\triangleq\left(F(D_{\\_}i)\xrightarrow{\iota_{\\_}{i,\mathop{\uparrow^{s}}i}}D_{\\_}{\mathop{\uparrow^{s}}i}\xrightarrow{\mathrm{inc}^{D}_{\\_}{\mathop{\uparrow^{s}}i}}\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i=\mu
F\right)$

By (7), $(\iota_{\\_}i)_{\\_}{i\in\kappa}$ is a cocone under the diagram
$F\circ D:\kappa\rightarrow\mathcal{C}$ and so induces
$\hat{\iota}:\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F(D_{\\_}i)\rightarrow\mu
F$. Then since $F$ preserves the colimit of $D$, we get a morphism

$\iota\triangleq\left(F(\mu
F)=F(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)\cong\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F(D_{\\_}i)\xrightarrow{\hat{\iota}}\mu
F\right)$ (9)

Therefore $\mu F$ has the structure of an $F$-algebra. To see that it is
initial, suppose we are given $a:F(A)\rightarrow A$. We have to show that
there is a unique $F$-algebra morphism $(\mu F,\iota)\rightarrow(A,a)$.

If $h:\mu F\rightarrow A$ is such an algebra morphism, that is
$h\circ\iota=a\circ F(h)$, then by definition of $\iota$ in (9) it follows
that the associated cocone $(h_{\\_}i\triangleq
h\circ\mathrm{inc}^{D}_{\\_}i:D_{\\_}i\rightarrow A)_{\\_}{i\in\kappa}$
satisfies
$h_{\\_}{\mathop{\uparrow^{s}}i}\circ\iota_{\\_}{i,\mathop{\uparrow^{s}}i}=a\circ
F(h_{\\_}i)$. From this, using the directedness property of sizes, we get

$\forall i\in\kappa.\forall j<i.\;h_{\\_}i\circ\iota_{\\_}{j,i}=a\circ
F(h_{\\_}i\circ D_{\\_}{j,i})$ (10)

So if $h$ and $h^{\prime}$ are both $F$-algebra morphisms $(\mu
F,\iota)\rightarrow(A,a)$, one can prove by well-founded induction for $<$,
using (8) and (10), that $\forall
i\in\kappa.\;h\circ\mathrm{inc}^{D}_{\\_}i=h^{\prime}\circ\mathrm{inc}^{D}_{\\_}i$
and hence that $h=h^{\prime}$.

So it just remains to prove that there is such an $h$. It suffices to
construct a cocone $(h_{\\_}i:D_{\\_}i\rightarrow A)_{\\_}{i\in\kappa}$
satisfying (10) and then take $h$ to be the morphism given by the universal
property of the colimit; for then we have $\forall
i\in\kappa.\;h_{\\_}{\mathop{\uparrow^{s}}i}\circ\iota_{\\_}{i,\mathop{\uparrow^{s}}i}=a\circ
F(h_{\\_}i)$ and hence $h\circ\iota=a\circ F(h)$, as required.

For each $i\in\kappa$, say that a morphism $h^{\prime}:D_{\\_}i\rightarrow A$
is an _up-to- $i$ algebra morphism_ if $\forall
j<i.\;h^{\prime}\circ\iota_{\\_}{j,i}=a\circ F(h^{\prime}\circ D_{\\_}{j,i})$
(_cf_. (10)). Given such a morphism, then for any $j<i$, $h^{\prime}\circ
D_{\\_}{j,i}:D_{\\_}j\rightarrow A$ is an up-to-$j$ algebra morphism. From
this it follows by well-founded induction for $<$ that any two up-to-$i$
algebra morphisms are equal. A well-founded recursion for $<$ allows one to
construct an up-to-$i$ algebra morphism $h_{\\_}i:D_{\\_}i\rightarrow A$ for
each $i\in\kappa$; and the uniqueness of up-to algebra morphisms implies that
$h_{\\_}j=h_{\\_}i\circ D_{\\_}{j,i}$ when $j<i$. Thus
$(h_{\\_}i)_{\\_}{i\in\kappa}$ is the required cocone satisfying (10). ∎

######  Corollary 3.9.

With the same assumptions on $\mathcal{C}$, $F$ and $\kappa$ as in Theorem
3.8, then free $F$-algebras exist, that is, the forgetful functor from the
category of $F$-algebras to $\mathcal{C}$ has a left adjoint.

###### Proof.

The free $F$-algebra on an object $X\in\mathcal{C}$ is the same thing as an
initial algebra for the endofunctor $F(\\_)+X$. So by the theorem, it suffices
to check that $F(\\_)+X$ preserves colimits of diagrams
$\kappa\rightarrow\mathcal{C}$. It does so because $F$ does by assumption and
because $\kappa$ is directed (cf. Proposition 4.7(4) below). ∎

##  4 Initial algebras for sized endofunctors

In classical set theory with the Axiom of Choice, given a set of operation
symbols $A\in\mathbf{Set}$ with associated arities $B\in\mathbf{Set}^{A}$, the
associated polynomial endofunctor $X\mapsto\sum_{\\_}{a\in A}X^{B(a)}$ on
$\mathbf{Set}$ preserves $\lambda$-colimits when the ordinal $\lambda$ is
large enough; specifically it does so if for all $a\in A$, $\lambda$ has upper
bounds (with respect to the strict total order given by membership) for all
$B(a)$-indexed families of ordinals less than $\lambda$. We will see that this
notion of “large enough” is also the right one for sizes in our constructive
setting.

######  Definition 4.1.

A _signature_ (also known as a _container_ [2, 17]) is specified by a set
$A\in\mathbf{Set}$ and an $A$-indexed family of sets $B\in\mathbf{Set}^{A}$.
We write $\mathbf{Sig}\in\mathbf{Set}_{\\_}1$ for the large set of all such
signatures. Given $\Sigma=(A,B)\in\mathbf{Sig}$, we say that a size
$(\kappa,{<})$ is _$\Sigma$ -filtered_ if for all $a\in A$ and every function
$f:B(a)\rightarrow\kappa$, there exists $i\in\kappa$ with $\forall x\in
B(a).\;f(x)<i$.

We can deduce the existence of $\Sigma$-filtered sizes by abstracting from the
constructive analysis of Conway’s surreal numbers by Shulman [31], which in
turn is inspired by Taylor’s constructive notion of “plump” ordinal [36]. For
each $\Sigma=(A,B)\in\mathbf{Sig}$, let $W_{\\_}{\Sigma}$ be the initial
algebra for the associated polynominal endofunctor
$F_{\\_}{A,B}:\mathbf{Set}\rightarrow\mathbf{Set}$,
$F_{\\_}{A,B}(X)=\sum_{\\_}{a\in A}X^{B(a)}$. Thus $W_{\\_}\Sigma$ is an
example of a W-type [27, Chapter 15]. The function $\Sigma\mapsto
W_{\\_}{\Sigma}$ exists in our constructive setting, because W-types can be
constructed in elementary toposes with natural number objects [25, Proposition
3.6]; one can take the elements of $W_{\\_}\Sigma$ to be well-founded trees
representing the algebraic terms inductively generated by the signature
$\Sigma$. Each such term $t$ is uniquely of the form $\sup_{\\_}{a}f$ where
$\sup_{\\_}{a}$ is the $B(a)$-arity operation symbol named by $a\in A$ and,
inductively, $f=(t_{\\_}x)_{\\_}{x\in B(a)}$ is a $B(a)$-tuple of well-founded
algebraic terms over $\Sigma$. The _plump_ ordering on $W_{\\_}\Sigma$ is
given by the least relations ${\\_<\\_}\subseteq W_{\\_}\Sigma\times
W_{\\_}\Sigma$ and ${\\_\leq\\_}\subseteq W_{\\_}\Sigma\times W_{\\_}\Sigma$
satisfying for all $a\in A$, $f:B(a)\rightarrow W_{\\_}\Sigma$ and $t\in
W_{\\_}\Sigma$

$(\forall x\in B(a).\;f(x)<t)\Rightarrow\textstyle\sup_{\\_}af\leq
t\quad\text{and}\quad(\exists x\in B(a).\;t\leq f(x))\Rightarrow
t<\textstyle\sup_{\\_}af$ (11)

As noted in [15, Example 5.4], $<$ is transitive and well-founded, and $\leq$
is a preorder (reflexive and transitive). In particular, since $\leq$ is
reflexive, from (11) we deduce that $\forall x\in B(a).\;f(x)<\sup_{\\_}af$,
in other words for each arity set $B(a)$ in the signature, any function
$f:B(a)\rightarrow W_{\\_}\Sigma$ is bounded above in the $<$ relation by
$\sup_{\\_}af$. This allows us to construct $\Sigma$-filtered sizes:

######  Proposition 4.2.

There is a $\Sigma$-filtered size $(\kappa_{\\_}\Sigma,{<})$ for every
signature $\Sigma$.

###### Proof.

Given a signature $\Sigma=(A,B)$, we extend it to a signature
$(A^{\prime},B^{\prime})$ by adding fresh nullary and binary operation
symbols. Thus $A^{\prime}\triangleq A\uplus\\{n,b\\}$ and
$B^{\prime}\in\mathbf{Set}^{A^{\prime}}$ satisfies $B^{\prime}(a)\triangleq
B(a)$ for $a\in A$, $B^{\prime}(n)\triangleq\emptyset$ and
$B^{\prime}(b)\triangleq\\{0,1\\}$. Let set $\kappa_{\\_}\Sigma$ be the W-type
$W_{\\_}{(A^{\prime},B^{\prime})}$ and let $<$ be the plump order given by
(11). As noted above, $<$ is transitive and well-founded and has upper bounds
for any arity-indexed family and hence in particular it is $\Sigma$-filtered.
It just remains to see that it is directed (Definition 3.2). Since
$A^{\prime}$ contains the nullary operation symbol $n$, $\kappa_{\\_}\Sigma$
contains $0^{s}\triangleq\sup_{\\_}n\emptyset$; and given
$i,j\in\kappa_{\\_}\Sigma$, letting
$f:B^{\prime}(b)=\\{0,1\\}\rightarrow\kappa_{\\_}\Sigma$ map $0$ to $i$ and
$1$ to $j$, then $i\mathbin{\sqcup^{s}}j\triangleq\sup_{\\_}bf$ is an upper
bound for $i$ and $j$ with respect to $<$. ∎

######  Definition 4.3.

Given a signature $\Sigma\in\mathbf{Sig}$, a functor
$F:\mathcal{C}\rightarrow\mathcal{D}$ between cocomplete categories is
_$\Sigma$ -sized_ if it preserves colimits of all diagrams
$\kappa\rightarrow\mathcal{C}$ for any $\Sigma$-filtered size $\kappa$. A
functor is _sized_ it there exists a signature $\Sigma$ for which it is
$\Sigma$-sized.

######  Theorem 4.4 ((Sized endofunctors have initial algebras)).

Assuming $\mathcal{C}$ is a cocomplete category, if
$F:\mathcal{C}\rightarrow\mathcal{C}$ is sized, then there exists an initial
algebra for $F$. More precisely, there is a function assigning to each
signature $\Sigma$ and each $\Sigma$-sized endofunctor $F$ an initial algebra
for $F$.

###### Proof.

If $F$ is $\Sigma$-sized for some $\Sigma\in\mathbf{Sig}$, then $F$ preserves
colimits of diagrams for the $\Sigma$-filtered size $\kappa_{\\_}\Sigma$
constructed in the proof of Proposition 4.2. Hence by Theorem 3.8, it has an
initial algebra, given by taking the colimit of its inflationary iteration. ∎

To apply this theorem one needs a rich collection of sized functors. The rest
of the section is devoted to exploring closure properties of sized functors.
To do so we use the following operation on signatures:

######  Definition 4.5.

Suppose $\Sigma_{\\_}c=(A_{\\_}c,B_{\\_}c)$ is a family of signatures indexed
by the elements $c$ of some set $C$. Then the _signature sum_
$\bigoplus_{\\_}{c\in C}\Sigma_{\\_}c$ is the signature $(A,B)$ where
$A\triangleq\sum_{\\_}{c\in C}A_{\\_}c=\\{(c,a)\mid c\in C\wedge a\in
A_{\\_}c\\}$ and $B\in\mathbf{Set}^{A}$ maps each $(c,a)$ to the set
$B_{\\_}c(a)$. As a special case when $I=\\{0,1\\}$, we have the _binary sum_
$\Sigma_{\\_}0\oplus\Sigma_{\\_}1$. There is also an _empty signature_
$0=(\emptyset,\emptyset)$ which acts as a unit for $\oplus$ up to isomorphism
(for a suitable notion of signature morphism).

######  Remark 4.6.

Note that if a size is $(\bigoplus_{\\_}{c\in C}\Sigma_{\\_}c)$-filtered, it
is also $\Sigma_{\\_}c$-filtered for each $c\in C$. Conversely, given a single
signature $\Sigma$, if a size is $\Sigma$-filtered, it is also
$(\bigoplus_{\\_}{c\in C}\Sigma)$-filtered.

######  Proposition 4.7.

Suppose that $\mathcal{C}$,$\mathcal{D}$ and $\mathcal{E}$ are cocomplete
categories.

  1. 1.

Any cocontinuous functor $\mathcal{C}\rightarrow\mathcal{D}$ is sized.

  2. 2.

Identity functors are sized. If $F:\mathcal{C}\rightarrow\mathcal{D}$ and
$G:\mathcal{D}\rightarrow\mathcal{E}$ are sized, so is their composition
$G\circ F:\mathcal{C}\rightarrow\mathcal{E}$.

  3. 3.

The terminal functor $\mathcal{C}\rightarrow 1$ and the projection functors
$\pi_{\\_}1:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{C}$ and
$\pi_{\\_}2:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{C}$ are sized; if
$F:\mathcal{C}\rightarrow\mathcal{D}$ and
$G:\mathcal{C}\rightarrow\mathcal{E}$ are sized, then so is $\langle
F,G\rangle:\mathcal{C}\rightarrow\mathcal{D}\times\mathcal{E}$.

  4. 4.

For any $X\in\mathcal{C}$ the constant functor $1\rightarrow\mathcal{C}$ with
value $X$ is sized.

###### Proof.

For part 1, if $F:\mathcal{C}\rightarrow\mathcal{D}$ is cocontinuous, then it
is $\Sigma$-sized for any $\Sigma$ and in particular for the empty signature.

The first sentence of part 2 follows from part 1. If $F$ is $\Sigma$-sized and
$G$ is $\Sigma^{\prime}$-sized, then $F$ and $G$ both preserve colimits over
any $\Sigma\oplus\Sigma^{\prime}$-filtered size, because such a size is also
$\Sigma$\- and $\Sigma^{\prime}$-filtered. The composition $G\circ F$
preserves such a colimit because $F$ and $G$ do. Therefore $G\circ F$ is
$\Sigma\oplus\Sigma^{\prime}$-sized.

For part 3 we use the fact that colimits in a product category are computed
componentwise. Thus the terminal and projection functors are sized by part 1;
and if $F:\mathcal{C}\rightarrow\mathcal{D}$ is $\Sigma$-sized and
$G:\mathcal{C}\rightarrow\mathcal{E}$ is $\Sigma^{\prime}$-sized, then
$\langle F,G\rangle$ is $\Sigma\oplus\Sigma^{\prime}$-sized.

For part 4, note that each size $\kappa$ is directed and hence in particular
is a connected semi-category; therefore
$\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}X$ is canonically isomorphic
to $X$. So the constant functor with value $X$ is $\Sigma$-sized for any
$\Sigma$ and in particular for the empty signature. ∎

We can deduce further preservation properties involving infinitary operations
on sized functors by assuming a weak form of choice, which following
https://ncatlab.org/nlab/show/WISC we call the [wisc] axiom. It was introduced
in type theory by Streicher [33] under the name $\mathrm{TTCA}_{\\_}f$ (“Type
Theoretic Collection Axiom”) and independently in constructive set theory by
Moerdijk and van den Berg [39] under the name “Axiom of Multiple Choice”; see
also Levy [21, Section 5.1]:

######  Axiom 4.8 ([wisc]).

A (possibly large) _cover_ of a set $X\in\mathbf{Set}$ is a surjective
function $f:Y\twoheadrightarrow X$ with $Y\in\mathbf{Set}_{\\_}1$. An indexed
family555We will refer to elements of $\mathbf{Sig}$ as _families_ rather than
_signatures_ when we are not thinking of them as collections of operation
symbols of set-valued arity. $(E_{\\_}c)_{\\_}{c\in C}\in\mathbf{Sig}$ is a
_wisc_ for $X\in\mathbf{Set}$ if for any cover $f:Y\twoheadrightarrow X$,
there exist $c\in C$ and $g:E_{\\_}c\rightarrow Y$ such that $f\circ g$ is
surjective. The [wisc] axiom666For simplicity and following [33], we have
given the axiom just for a pair of universes,
$(\mathbf{Set}_{\\_}0,\mathbf{Set}_{\\_}1)$; more generally one can ask for
the property to hold for any pair $(\mathbf{Set}_{\\_}m,\mathbf{Set}_{\\_}n)$.
states that for every $X\in\mathbf{Set}$ there exists a family
$(E_{\\_}c)_{\\_}{c\in C}\in\mathbf{Sig}$ that is a wisc for it.

“Wisc” stands for “weakly initial set of covers” and the terminology is
justified by the fact that if in $\mathbf{Set}$ the family
$(E_{\\_}c)_{\\_}{c\in C}$ is a wisc for $X$, then the family of covers of $X$
whose domains are of the form $E_{\\_}c$ for some $c\in C$ is weakly initial
among all the (possibly large) covers of $X$: for every
$Y\in\mathbf{Set}_{\\_}1$ and $f:Y\twoheadrightarrow X$, there is some cover
$e:E_{\\_}c\twoheadrightarrow X$ in the family that factors as $e=f\circ g$
for some $g:E_{\\_}c\rightarrow Y$.

Classically, [wisc] is implied by the Axiom of Choice [ac], since the latter
implies that every surjection has a right inverse and hence the family whose
single member is $X$ is a is a wisc for $X$. From the results of van den Berg
and Moerdijk [39] (and as noted by Streicher [33]), if any elementary topos
$\mathcal{E}$ satisfies [wisc], then so do toposes of (pre)sheaves and
realizability toposes built from $\mathcal{E}$; it is in this sense that the
axiom is constructively acceptable. In particular, starting from the category
of sets in classical set theory with [ac], [wisc] holds in the kinds of topos
that have been used to model type theory with various kinds of higher
inductive types, whose semantics motivates the work presented here. (However,
it does not hold in all toposes [30].)

######  Lemma 4.9 ([wisc]).

Suppose [wisc] holds and that $\mathcal{C}$ and $\mathcal{D}$ are cocomplete
categories. If $(F_{\\_}x:\mathcal{C}\rightarrow\mathcal{D})_{\\_}{x\in X}$ is
a family of sized functors indexed by a set $X\in\mathbf{Set}$, then there
exists a signature $\Sigma\in\mathbf{Sig}$ such that $F_{\\_}x$ is
$\Sigma$-sized for all $x\in X$.

###### Proof.

Consider the large set $S\triangleq\sum_{\\_}{x\in
X}\\{\Sigma^{\prime}\in\mathbf{Sig}\mid\text{$F_{\\_}x$ is a
$\Sigma^{\prime}$-sized functor}\\}$ in $\mathbf{Set}_{\\_}1$. By assumption
on $F$, the first projection $\pi_{\\_}1:S\rightarrow X$ is a large777This
proof, as well as that for Lemma 4.12, illustrate the need for a wisc property
that quantifies over large covers of small sets. cover of $X$. By [wisc] there
is some surjection $e:X^{\prime}\twoheadrightarrow X$ in $\mathbf{Set}$ and a
function $\Sigma^{\prime}:X^{\prime}\rightarrow\mathbf{Sig}$ so that for all
$x^{\prime}\in X^{\prime}$, the functor $F_{\\_}{e(x^{\prime})}$ is
$\Sigma^{\prime}_{\\_}{x^{\prime}}$-sized; and since $e$ is surjective this
implies that each $F_{\\_}x$ is $\Sigma^{\prime}_{\\_}{x^{\prime}}$-sized for
some $x^{\prime}\in X^{\prime}$. Consider the signature
$\Sigma\triangleq\bigoplus_{\\_}{x^{\prime}\in
X^{\prime}}\Sigma^{\prime}_{\\_}{x^{\prime}}$ from Definition 4.5. By Remark
4.6, each $F_{\\_}x$ is $\Sigma$-sized. ∎

######  Theorem 4.10 ([wisc] (Colimits of sized functors)).

Suppose that [wisc] holds, $\mathcal{C}$ and $\mathcal{D}$ are cocomplete
categories, $\mathbf{C}$ is a small category and that
$F:\mathbf{C}\times\mathcal{C}\rightarrow\mathcal{D}$ is a functor. If for
some signature $\Sigma\in\mathbf{Sig}$ the functor $F(c,\\_)$ is
$\Sigma$-sized for each $c\in\mathbf{C}$, then
$\operatorname{\mathrm{colim}}_{\\_}{c\in\mathbf{C}}F(c,\\_):\mathcal{C}\rightarrow\mathcal{D}$
is also $\Sigma$-sized. More generally, if each $F(c,\\_)$ is sized, then so
is $\operatorname{\mathrm{colim}}_{\\_}{c\in\mathbf{C}}F(c,\\_)$.

###### Proof.

If $F(c,\\_):\mathcal{C}\rightarrow\mathcal{D}$ is $\Sigma$-sized for all
$c\in\mathbf{C}$ and $\kappa$ is a $\Sigma$-filtered size, then each
$F(c,\\_)$ preserves colimits of all diagrams $\kappa\rightarrow\mathcal{C}$.
Thus given such a diagram $D:\kappa\rightarrow\mathcal{C}$, we have a
canonical isomorphism
$F(c,\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)\cong\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F(c,D_{\\_}i)$,
natural in $c$. Taking the colimit over $c\in\mathbf{C}$ and writing
$F^{\prime}\triangleq\operatorname{\mathrm{colim}}_{\\_}{c\in\mathbf{C}}F(c,\\_)$,
we have
$F^{\prime}(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)=\operatorname{\mathrm{colim}}_{\\_}{c\in\mathbf{C}}F(c,\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)\cong\operatorname{\mathrm{colim}}_{\\_}{c\in\mathbf{C}}\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F(c,D_{\\_}i)$.
Since colimits commute with each other, it follows that the canonical morphism
$F^{\prime}(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)\rightarrow\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F^{\prime}(D_{\\_}i)$
is an isomorphism. Therefore $F^{\prime}$ is $\Sigma$-sized. The last sentence
of the theorem follows by Lemma 4.9. ∎

######  Corollary 4.11 ([wisc]).

Suppose [wisc] holds and that $\mathcal{C}$ and $\mathcal{D}$ are cocomplete
categories. If $F:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{D}$ is
sized, then there is a function $X\mapsto\mu Y.F(X,Y)$ assigning to each
$X\in\mathcal{C}$ an initial algebra $\mu Y.F(X,Y)$ for the functor
$F(X,\\_):\mathcal{D}\rightarrow\mathcal{D}$. The induced functor $\mu
Y.F(\\_,Y):\mathcal{C}\rightarrow\mathcal{D}$ is sized.

###### Proof.

Suppose $F:\mathcal{C}\times\mathcal{D}\rightarrow\mathcal{D}$ is
$\Sigma$-sized. It follows from Proposition 4.7 and Remark 4.6 that for each
$X\in\mathcal{C}$, the functor $F_{\\_}X\triangleq
F(X,\\_):\mathcal{D}\rightarrow\mathcal{D}$ is $\Sigma$-sized. Therefore by
Theorems 3.8 and 4.4, the function $X\mapsto\mu
Y.F(X,Y)\triangleq\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa_{\\_}\Sigma}\mu_{\\_}iF_{\\_}X$
is the required function mapping each $X\in\mathcal{C}$ to an initial algebra
for $F(X,\\_)$. Since each $\mu_{\\_}iF_{\\_}X$ is
$\operatorname{\mathrm{colim}}_{\\_}{j<i}F(X,\mu_{\\_}jF_{\\_}X)$, it follows
by well-founded induction on $i\in\kappa_{\\_}\Sigma$ that each
$\mu_{\\_}iF_{\\_}X$ is $\Sigma$-sized, using Theorem 4.10 (taking
$\mathbf{C}$ to be the category generated by the thin semi-category
${\downarrow}(i)$). Then by Theorem 4.10 again (taking $\mathbf{C}$ to be the
category generated by $\kappa$) we have that $\mu
Y.F(\\_,Y)=\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa_{\\_}\Sigma}\mu_{\\_}iF_{\\_}{\\_}$
is $\Sigma$-sized. ∎

Although Propositions 4.7, 4.10 and 4.11 show that there is quite a rich
collection of sized functors, what is lacking so far is any closure under
taking limits, assuming the target category has them; in other words the dual
of Theorem 4.10. We consider this for the case $\mathcal{D}=\mathbf{Set}$,
leaving consideration of more general complete and cocomplete categories for
future work. First note that if $F,G:\mathcal{C}\rightarrow\mathbf{Set}$ are
sized functors, the equalizer of any parallel pair $F\rightrightarrows G$ of
natural transformations is also a sized functor (it is
$(\Sigma\oplus\Sigma^{\prime})$-sized if $F$ is $\Sigma$-sized and $G$ is
$\Sigma^{\prime}$-sized). This is because each size $\kappa$ is directed and
so taking $\kappa$-colimits in $\mathbf{Set}$ commutes with finite limits and
hence in particular with equalizers. So to get closure of sized functors under
all small limits it suffices to consider small products. For this we need to
use a “double cover” signature of a set (the wiscs $W$ and $W^{\prime}$ in the
proof of Theorem 4.13 below), inspired by the use that Swan [35] makes of the
indexed form of the WISC Axiom; see also [15]. So we will need wiscs for
indexed families of sets; but their existence follows from [wisc]:

######  Lemma 4.12 ([wisc]).

Assuming [wisc] holds, then for every family of sets $(X_{\\_}i)_{\\_}{i\in
I}\in\mathbf{Sig}$ there exists a family $(E_{\\_}c)_{\\_}{c\in
C}\in\mathbf{Sig}$ that is a wisc for each set $X_{\\_}i$.

###### Proof.

Consider $S\triangleq\sum_{\\_}{i\in I}\\{W\in\mathbf{Sig}\mid\text{$W$ is a
wisc for $X_{\\_}i$}\\}\in\mathbf{Set}_{\\_}1$. By [wisc], the first
projection $\pi_{\\_}1:S\rightarrow I$ is a large cover of $I$. Since there is
a wisc for $I$, it follows that there is some surjection
$e:J\twoheadrightarrow I$ in $\mathbf{Set}$ and a function
$W:J\rightarrow\mathbf{Sig}$ so that for all $j\in J$, $W_{\\_}j$ is a wisc
for $X_{\\_}{e(j)}$. Consider the signature sum
$W\triangleq\bigoplus_{\\_}{j\in J}W_{\\_}j\in\mathbf{Sig}$ as in Definition
4.5. Thus writing $(C,E)$ for $W$ and $(C_{\\_}j,E_{\\_}j)$ for each
$W_{\\_}j$, we have $C\triangleq\sum_{\\_}{j\in J}C_{\\_}j\in\mathbf{Set}$ and
$E\in\mathbf{Set}^{C}$ is the function mapping each $(j,c)\in\sum_{\\_}{j\in
J}C_{\\_}j$ to $E_{\\_}j(c)$. Then we claim that $W\in\mathbf{Sig}$ is a wisc
for each set $X_{\\_}i$. For, given any cover $f:Y\twoheadrightarrow
X_{\\_}i$, since $e:J\twoheadrightarrow I$ is a surjection, there exists $j\in
J$ with $e(j)=i$; then since $W_{\\_}j=(C_{\\_}j,E_{\\_}j)$ is a wisc for
$X_{\\_}{e(j)}=X_{\\_}i$, there exists $c\in C_{\\_}j$ and
$g:E_{\\_}j(c)\rightarrow Y$ such that $f\circ g$ is surjective. So there
exists $(j,c)\in C$ and $g:E(j,c)=E_{\\_}j(c)\rightarrow Y$ with $f\circ g$ is
surjective. Therefore $W=(C,E)$ does indeed have the wisc property for
$X_{\\_}i$. ∎

######  Theorem 4.13 ([wisc] (Products of set-valued sized functors are
sized)).

Suppose that $\mathcal{C}$ is a cocomplete category. Assuming [wisc] holds, if
$(F_{\\_}x:\mathcal{C}\rightarrow\mathbf{Set})_{\\_}{x\in X}$ is a family of
sized functors indexed by some set $X\in\mathbf{Set}$, then the functor
$\prod_{\\_}{x\in X}F_{\\_}x:\mathcal{C}\rightarrow\mathbf{Set}$ given by
taking products in $\mathbf{Set}$ is also sized.

###### Proof.

By Lemma 4.9, there exists a signature $\Sigma$ so that each functor
$F_{\\_}x$ is $\Sigma$-sized. However, we need a bigger signature than
$\Sigma$ in order to prove that $\prod_{\\_}{x\in X}F_{\\_}x$ is sized. Using
[wisc], let $W=(E_{\\_}c)_{\\_}{c\in C}$ be a wisc for $X$. Then using Lemma
4.12, let $W^{\prime}=(E^{\prime}_{\\_}{c^{\prime}})_{\\_}{c^{\prime}\in
C^{\prime}}$ be a wisc for the sets in the family $(\ker p)_{\\_}{c\in
C,p:E_{\\_}c\twoheadrightarrow X}$, where

$\ker p\triangleq\\{(d_{\\_}1,d_{\\_}2)\in E_{\\_}c\times E_{\\_}c\mid
p(d_{\\_}1)=p(d_{\\_}2)\\}$ (12)

We claim that the functor $F^{\prime}\triangleq\prod_{\\_}{x\in X}F_{\\_}x$ is
$\Sigma^{\prime}$-sized when $\Sigma^{\prime}=\Sigma\oplus W\oplus W^{\prime}$
(using the signature sum from Definition 4.5).

If $D:\kappa\rightarrow\mathcal{C}$ is a diagram on a
$\Sigma^{\prime}$-filtered size $\kappa$, then by Remark 4.6, each $F_{\\_}x$
is $\Sigma^{\prime}$-sized and so we have a canonical isomorphism
$\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F_{\\_}x(D_{\\_}i)\cong
F_{\\_}x(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)$. Taking the
product over $x\in X$, we get $\prod_{\\_}{x\in
X}\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F_{\\_}x(D_{\\_}i)\cong\prod_{\\_}{x\in
X}F_{\\_}x(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)=(\prod_{\\_}{x\in
X}F_{\\_}x)(\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}D_{\\_}i)$. So it
just remains to show that the canonical function

$\textstyle\operatorname{\mathrm{can}}_{\\_}{F,D}:\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}\left(\left(\prod_{\\_}{x\in
X}F_{\\_}x\right)D_{\\_}i\right)=\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}\prod_{\\_}{x\in
X}F_{\\_}x(D_{\\_}i)\rightarrow\prod_{\\_}{x\in
X}\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F_{\\_}x(D_{\\_}i)$ (13)

is an isomorphism, that is, both an injection and a surjection. The summand
$W$ in $\Sigma^{\prime}$ ensures that $\kappa$ has upper bounds for
$E_{\\_}c$-indexed families for any $c\in C$; and the $W^{\prime}$ summand
ensures the same for $E^{\prime}_{\\_}{c^{\prime}}$-indexed families, for any
$c^{\prime}\in C^{\prime}$. The first kind of upper bound, together with the
wisc property of $W$ comes into play in proving that
$\operatorname{\mathrm{can}}_{\\_}{F,D}$ is injective; and both kinds of upper
bound and the wisc properties of $W$ and $W^{\prime}$ come into play in
proving that $\operatorname{\mathrm{can}}_{\\_}{F,D}$ is surjective.

To prove that $\operatorname{\mathrm{can}}_{\\_}{F,D}$ is injective and
surjective we use the fact that the colimit in $\mathbf{Set}$ of a directed
diagram $D:\kappa\rightarrow\mathbf{Set}$ can be described explicitly as the
quotient $(\sum_{\\_}{i\in\kappa}D_{\\_}i)/{\approx}$ where the equivalence
relation $\approx$ identifies
$(i,d),(i^{\prime},d^{\prime})\in\sum_{\\_}{i\in\kappa}D_{\\_}i$ if there is
some $j\in\kappa$ with $i<j$, $i^{\prime}<j$ and
$D_{\\_}{i,j}(d)=D_{\\_}{i^{\prime},j}(d^{\prime})$. We will write
$[i,d]_{\\_}{\approx}$ for the ${\approx}$-equivalence class of
$(i,d)\in\sum_{\\_}{i\in\kappa}D_{\\_}i$. Then the function in equation 13
satisfies for all $i\in\kappa$ and $f\in\prod_{\\_}{x\in X}F_{\\_}x(D_{\\_}i)$

$\operatorname{\mathrm{can}}_{\\_}{F,D}[i,f]_{\\_}{\approx}=\lambda x\in
X.\;[i,f(x)]_{\\_}{\approx}$

To see that $\operatorname{\mathrm{can}}_{\\_}{F,D}$ is injective, suppose we
also have $i^{\prime}\in\kappa$ and $f^{\prime}\in\prod_{\\_}{x\in
X}F_{\\_}x(D_{\\_}i)$ satisfying $\forall x\in
X.\;[i,f(x)]_{\\_}{\approx}=[i^{\prime},f^{\prime}(x)]_{\\_}{\approx}$; we
wish to prove that $(i,f)\approx(i^{\prime},f^{\prime})$. By definition of
$\approx$, from the assumption about $(i^{\prime},f^{\prime})$ we have
$\forall x\in X.\exists
j\in\kappa.\;i<j\;\wedge\;i^{\prime}<j\;\wedge\;F_{\\_}x(D_{\\_}{i,j})(f\,x)=F_{\\_}x(D_{\\_}{i^{\prime},j})(f^{\prime}x)$.
Since $W=(E_{\\_}c)_{\\_}{c\in C}$ is a wisc for $X$, there exists $c\in C$, a
surjection $p:E_{\\_}c\twoheadrightarrow X$ and a function
$q:E_{\\_}c\rightarrow\kappa$ so that

$\forall z\in
E_{\\_}c.\;i<q(z)\;\wedge\;i^{\prime}<q(z)\;\wedge\;F_{\\_}x(D_{\\_}{i,q(z)})(f(p\,z))=F_{\\_}x(D_{\\_}{i^{\prime},q(z)})(f^{\prime}(p\,z))$
(14)

Since $W$ is a summand in $\Sigma^{\prime}$ and $\kappa$ is a
$\Sigma^{\prime}$-filtered size, there is an $<$-upper bound $j\in\kappa$ for
$q:E_{\\_}c\rightarrow\kappa$; and since $\kappa$ is directed, we can assume
$i<j$ and $i^{\prime}<j$. So from (14) and surjectiviy of $p$ we deduce that
$\forall x\in
X.\;F_{\\_}x(D_{\\_}{i,j})(f\,x)=F_{\\_}x(D_{\\_}{i^{\prime},j})(f^{\prime}x)$,
which implies $(i,f)\approx(i^{\prime},f^{\prime})$. Therefore the function
$\operatorname{\mathrm{can}}_{\\_}{F,D}$ in (13) is indeed injective.

To see that $\operatorname{\mathrm{can}}_{\\_}{F,D}$ is also surjective,
suppose we have $g\in\prod_{\\_}{x\in
X}\operatorname{\mathrm{colim}}_{\\_}{i\in\kappa}F_{\\_}x(D_{\\_}i)$. Since

$\textstyle\forall x\in
X.\exists(i,d)\in\sum_{\\_}{i\in\kappa}F_{\\_}x(D_{\\_}i).\;g(x)=[i,d]_{\\_}{\approx}$

and $W$ is a wisc for $X$, there exists some $c\in C$,
$p:E_{\\_}c\twoheadrightarrow X$ and $\langle
q_{\\_}1,q_{\\_}2\rangle\in\prod_{\\_}{z\in
E_{\\_}c}\sum_{\\_}{i\in\kappa}F_{\\_}{p(z)}(D_{\\_}i)$ so that $\forall z\in
E_{\\_}c.\;g(p\,z)=[q_{\\_}1(z),q_{\\_}2(z)]_{\\_}{\approx}$. Then since $W$
is a summand in $\Sigma^{\prime}$ and $\kappa$ is a $\Sigma^{\prime}$-filtered
size, there is an $<$-upper bound $j\in\kappa$ for
$q_{\\_}1:E_{\\_}c\rightarrow\kappa$. So we have

$\forall z\in E_{\\_}c.\;g(p\,z)=[j,q^{\prime}(z)]_{\\_}{\approx}$ (15)

where $q^{\prime}\in\prod_{\\_}{z\in E_{\\_}c}F_{\\_}{p(z)}(D_{\\_}j)$ is
$q^{\prime}(z)\triangleq F_{\\_}{p(z)}(D_{\\_}{q_{\\_}1(z),j})(q_{\\_}2(z))$.
It follows that the relation $\Phi\subseteq\sum_{\\_}{x\in
X}F_{\\_}x(D_{\\_}j)$ given by $\Phi(x,d)\triangleq\exists z\in
E_{\\_}c.\;x=p(z)\;\wedge\;d=q^{\prime}(z)$ is total (because $p$ is
surjective); and were it also single-valued, it would determine a function
$f\in\prod_{\\_}{x\in X}F_{\\_}x(D_{\\_}j)$ which by virtue of (15) would
satisfy $can_{\\_}{F,D}[j,f]=g$. However, we need to increase $j$ to get this
single-valued property. Recall that $W^{\prime}$ is a wisc for the kernel (12)
of $p:E_{\\_}c\twoheadrightarrow X$. If $(z_{\\_}1,z_{\\_}2)\in\ker p$, then
by (15)
$[j,q^{\prime}(z_{\\_}1)]_{\\_}{\approx}=g(p\,z_{\\_}1)=g(p\,z_{\\_}2)=[j,q^{\prime}(z_{\\_}2)]_{\\_}{\approx}$.
Therefore we have

$\forall(z_{\\_}1,z_{\\_}2)\in\ker p.\exists
k\in\kappa.\;j<k\;\wedge\;F_{\\_}{p(z_{\\_}1)}(D_{\\_}{q_{\\_}1(z_{\\_}1),k})(q_{\\_}2(z_{\\_}1))=F_{\\_}{p(z_{\\_}2)}(D_{\\_}{q_{\\_}1(z_{\\_}2),k})(q_{\\_}2(z_{\\_}2))$

So since $W^{\prime}=(E_{\\_}{c^{\prime}})_{\\_}{c^{\prime}\in C^{\prime}}$ is
a wisc for $\ker p$ and $\kappa$ has $E_{\\_}{c^{\prime}}$-indexed upper
bounds for any $c^{\prime}\in C^{\prime}$ and is directed, it follows that
there exists $c^{\prime}\in C^{\prime}$, $\langle
p_{\\_}1,p_{\\_}2\rangle:E_{\\_}{c^{\prime}}\twoheadrightarrow\ker p$ and
$k\in\kappa$ with $j<k$ and

$\forall z^{\prime\prime}\in
E_{\\_}{c^{\prime}}.F_{\\_}{p(p_{\\_}1\,z^{\prime\prime})}(D_{\\_}{q_{\\_}1(p_{\\_}1z^{\prime\prime}),k})(q_{\\_}2(p_{\\_}1\,z^{\prime\prime}))=F_{\\_}{p(p_{\\_}2\,z^{\prime\prime})}(D_{\\_}{q_{\\_}1(p_{\\_}2z^{\prime\prime}),k})(q_{\\_}2(p_{\\_}2\,z^{\prime\prime}))$
(16)

Now if we let $q^{\prime\prime}\in\prod_{\\_}{z\in
E_{\\_}c}F_{\\_}{p(z)}(D_{\\_}k)$ be $q^{\prime\prime}(z)\triangleq
F_{\\_}{p(z)}(D_{\\_}{q_{\\_}1(z),k})(q_{\\_}2(z))$, then from (15) we have

$\forall z\in E_{\\_}c.\;g(p\,z)=[k,q^{\prime\prime}(z)]_{\\_}{\approx}$ (17)

Let the relation $\Phi^{\prime}\subseteq\sum_{\\_}{x\in X}F_{\\_}x(D_{\\_}k)$
be $\Phi^{\prime}(x,d)\triangleq\exists z\in
E_{\\_}c.\;x=p(z)\;\wedge\;d=q^{\prime\prime}(z)$. It is total because $p$ is
surjective; but it is also single-valued because if
$\Phi^{\prime}(x,d)\wedge\Phi^{\prime}(x,d^{\prime})$, then
$d=q^{\prime\prime}(z_{\\_}1)\wedge d^{\prime}=q^{\prime\prime}(z_{\\_}2)$ for
some $(z_{\\_}1,z_{\\_}2)\in\ker p$, so that there exists $z^{\prime\prime}\in
E_{\\_}{c^{\prime}}$ with $p_{\\_}1(z^{\prime\prime})=z_{\\_}1\wedge
p_{\\_}2(z^{\prime\prime})=z_{\\_}2$ and hence
$d=q^{\prime\prime}(z_{\\_}1)=q^{\prime\prime}(z_{\\_}2)=d^{\prime}$ by (16).
Therefore $\Phi^{\prime}$ is the graph of a function $f\in\prod_{\\_}{x\in
X}F_{\\_}x(D_{\\_}k)$; and by virtue of (17) we have $\forall x\in
X.\;g(x)=[k,f(x)]_{\\_}{\approx}$, so that $g=can_{\\_}{F,D}[k,f]$. Thus
$can_{\\_}{F,D}$ is indeed surjective. ∎

######  Example 4.14.

The _symmetric containers_ of Gylterud [18] generalize ordinary signatures by
replacing the set of operation symbols by a groupoid $\mathbf{A}$ and the
arity function by a functor $B:\mathbf{A}\rightarrow\mathbf{Set}$. The
associated endofunctor
$S_{\\_}{\mathbf{A},B}:\mathbf{Set}\rightarrow\mathbf{Set}$ maps each set
$X\in\mathbf{Set}$ to the colimit

$S_{\\_}{\mathbf{A},B}(X)\triangleq\operatorname{\mathrm{colim}}_{\\_}{a\in\mathbf{A}}X^{B(a)}$
(18)

Applying Theorem 4.4, Proposition 4.7 and Theorem 4.13 we have that any topos
with universes satisfying [wisc] has initial algebras for symmetric
containers.

In fact these initial algebras are special cases of QW-types [15]: they can be
seen as sets of terms quotiented by the symmetries given by the groupoid
structure on the arguments of an operation symbol. So their existence in
toposes with [wisc] follows from the results of that paper. However, the
construction here in terms of a colimit of an inflationary iteration gives a
simpler description than for the general case of a QW-type.

##  5 Related and future work

The results in this paper make use of the constructive techniques introduced
by the authors and Fiore in our prior paper [15]: the use of sizes given by
“plump” well-founded orders on W-types and the use of a WISC axiom to see that
certain functors preserve colimits of that shape. That paper constructs a
large class of quotient-inductive types, called _QWI-types_ , which by
definition are initial among algebras for indexed containers [2] satisfying a
given system of equations. Although the construction proceeds by forming a
size-indexed family of objects in the case $\mathcal{C}$ is $\mathbf{Set}^{I}$
(with $I\in\mathbf{Set}$) and taking its colimit, it does not appear to be a
direct corollary of Theorem 3.8. Conversely, the results here do not follow
from the ones in [15], since for one thing here we consider general cocomplete
categories $\mathcal{C}$, rather than just products of $\mathbf{Set}$. In this
respect we are closer to the approach of Fiore and Hur [13] and it would be
interesting to see whether our techniques can be extended to give constructive
proofs of existence of free algebras for the very general notion of equational
system on a category that is introduced in that paper. This may involve
investigating the extent to which our approach allows a constructive treatment
of some of the classical theory of locally presentable and accessible
categories [8], which is future work.

The inflationary iteration indexed by a notion of size that we have introduced
in this paper generalises from complete posets to cocomplete categories
aspects of Abel and Pientka’s work [3, 4]. These papers develop a theory of
_sized types_ and its semantics. Abel has added a version of this to the type
theory provided by the Agda proof assistant [9]. Unfortunately recent versions
of Agda contain features that allow one to use sized types to prove a logical
contradiction. The problem is that, in contrast to the notion of size used
here, the one by Abel et al. [3, 4] features a generic size $\infty$ at which
sized-indexed sequences become stationary. Currently in Agda (version 2.6.2)
one both has $\infty<\infty$ and can prove that $<$ is well-founded, leading
to a contradiction. For us, the intuitive and important aspect of “size” is
that there is well-founded ordering, thus permitting definitions by well-
founded recursion on a set of sizes. Then having a single size $\infty$ at
which all sequences become stationary is semantically problematic. So we avoid
having an explicit stationary size $\infty$, at the expense of having to take
a colimit to obtain an initial algebra, rather that just instantiating an
inflationary iteration at $\infty$.

We hope Agda’s sized types will get fixed, since they are useful in practice;
they are most often used (together with copatterns) to demonstrate that
recursively defined functions on a coinductively defined record type are well-
defined (that is, are “productive”) [4]. Here, while avoiding sized types, we
can still dualise Theorem 3.8. Applying it to the opposite category
$\mathcal{C}^{\mathrm{op}}$, we have that if $\mathcal{C}$ is complete and
$F:\mathcal{C}\rightarrow\mathcal{C}$ preserves limits of diagrams
$\kappa\rightarrow\mathcal{C}$ for some size $\kappa$, then _$F$ has a final
coalgebra $\nu F$ given by the limit of a deflationary iteration
$(\nu_{\\_}iF=\lim_{\\_}{j<i}F(\nu_{\\_}jF))_{\\_}{i\in\kappa}$_. We have yet
to investigate whether this is useful, that is, how rich is the class of such
endofunctors in a constructive setting.

Adámek, Milius and Moss [6] take a different approach to constructive initial
algebra theorems than the one here, avoiding iteration of the endofunctor.
They consider categories $\mathcal{C}$ with colimits of diagrams of
monomorphisms (from some well-behaved class) and endofunctors
$F:\mathcal{C}\rightarrow\mathcal{C}$ that preserve those monomorphisms. Using
the intuitionistically valid fixed point theorem of Pataraia (see [11, Theorem
3.2]), they prove that such an $F$ has an initial algebra iff it has a
prefixed point (an algebra whose structure morphism is a monomorphism).
Preserving monomorphisms seems less of a condition on a functor than the one
we need for Theorem 3.8, that is, preserving colimits of some size $\kappa$
(although the two conditions are independent). However, as we saw in Theorem
4.10, our class of sized endofunctors is closed under taking coequalizers, so
that we get initial algebras for constructs involving quotients, such as
Example 4.14; whereas endofunctors preserving monomorphisms are not in general
closed under taking coequalizers. Another difference to [6] is that it uses
impredicative principles (the proof of Pataraia’s fixed point theorem uses
impredicative quantification); whereas our Agda development [29] shows that
our initial algebra theorem (Theorem 3.8) is valid in a predicative
constructive logic.

## References

  * [1]
  * [2] M. Abbott, T. Altenkirch & N. Ghani (2005): _Containers: Constructing Strictly Positive Types_.  Theoretical Computer Science 342(1), pp. 3–27, 10.1016/j.tcs.2005.06.002.
  * [3] A. Abel (2012): _Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types_.  Electronic Proceedings in Theoretical Computer Science 77, pp. 1–11, 10.4204/EPTCS.77.1.
  * [4] A. Abel & B. Pientka (2016): _Well-Founded Recursion with Copatterns and Sized Types_.  Journal of Functional Programming 26, p. 61, 10.1017/S0956796816000022.
  * [5] J. Adámek (1974): _Free Algebras and Automata Realizations in the Language of Categories_.  Commentationes Mathematicae Universitatis Carolinae 15(4), pp. 589–602.
  * [6] J. Adámek, S. Milius & L. S. Moss (2021): _An Initial Algebra Theorem Without Iteration_.  ArXiv e-prints arXiv:2104.09837 [cs.LO].  Available at https://arxiv.org/abs/2104.09837.
  * [7] J. Adámek, S. Milius & L. S. Moss (2021): _Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors_.  Available at http://www.stefan-milius.eu.  Draft book.
  * [8] J. Adámek & J. Rosický (1994): _Locally Presentable and Accessible Categories_.  London Mathematical Society Lecture Note Series, Cambridge University Press, 10.1017/CBO9780511600579.
  * [9] Agda v2.6.1 (2021): Available at https://agda.readthedocs.io/en/v2.6.1.3/index.html.
  * [10] T. Altenkirch, P. Capriotti, G. Dijkstra, N. Kraus & F. N. Forsberg (2018): _Quotient Inductive-Inductive Types_.  In C. Baier & U. Dal Lago, editors: Foundations of Software Science and Computation Structures, FoSSaCS 2018, Lecture Notes in Computer Science 10803, Springer International Publishing, pp. 293–310, 10.1007/978-3-319-89366-2_16.
  * [11] A Bauer & P. Lumsdaine (2013): _On the Bourbaki–Witt Principle in Toposes_.  Mathematical Proceedings of the Cambridge Philosophical Society 155(1), pp. 87–99, 10.1017/S0305004113000108.
  * [12] P. Dybjer (2000): _A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory_.  Journal of Symbolic Logic 65(2), pp. 525–549.
  * [13] M. P. Fiore & C.-K. Hur (2008): _On the Construction of Free Algebras for Equational Systems_.  Theoretical Computer Science 410, pp. 1704–1729, 10.1016/j.tcs.2008.12.052.
  * [14] M. P. Fiore, A. M. Pitts & S. C. Steenkamp (2020): _Constructing Infinitary Quotient-Inductive Types_.  In J. Goubault-Larrecq & B. König, editors: 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), Lecture Notes in Computer Science 12077, Springer, pp. 257–276, 10.1007/978-3-030-45231-514.
  * [15] M. P. Fiore, A. M. Pitts & S. C. Steenkamp (2021): _Quotients, Inductive Types and Quotient Inductive Types_.  ArXiv e-prints arXiv:2101.02994 [cs.LO].  Available at https://arxiv.org/abs/2101.02994.
  * [16] F. N. Forsberg (2013): _Inductive-Inductive Definitions_.  Ph.D. thesis, Swansea University.
  * [17] N. Gambino & M. Hyland (2004): _Wellfounded Trees and Dependent Polynomial Functors_.  In S. Berardi, M. Coppo & F. Damiani, editors: Types for Proofs and Programs, Lecture Notes in Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 210–225, 10.1007/978-3-540-24849-1_14.
  * [18] H. R. Gylterud (2011): _Symmetric Containers_.  Master of Science, Department of Mathematics, University of Oslo.  Available at https://www.duo.uio.no/bitstream/handle/10852/10740/thesisgylterud.pdf.
  * [19] P. T. Johnstone (2002): _Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2_.  Oxford Logic Guides 43–44, Oxford University Press.
  * [20] A. Kovács & A. Kaposi (2020): _Large and Infinitary Quotient Inductive-Inductive Types_.  In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, Association for Computing Machinery, New York, NY, USA, p. 648–661, 10.1145/3373718.3394770.
  * [21] P. B. Levy (2021): _Broad Infinity and Generation Principles_.  ArXiv e-prints arXiv:2101.01698 [math.LO].  Available at https://arxiv.org/abs/2101.01698.
  * [22] D. R. Licata, I. Orton, A. M. Pitts & B. Spitters (2018): _Internal Universes in Models of Homotopy Type Theory_.  In H. Kirchner, editor: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs) 108, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 22:1–22:17, 10.4230/LIPIcs.FSCD.2018.22.
  * [23] P. Martin-Löf (1984): _Intuitionistic Type Theory_.  Bibliopolis, Napoli.
  * [24] E. Meijer, M. Fokkinga & R. Paterson (1991): _Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire_.  In J. Hughes, editor: Functional Programming Languages and Computer Architecture, FPCA 1991, Lecture Notes in Computer Science 523, Springer, Berlin, Heidelberg, pp. 124–144, 10.1007/3540543961_7.
  * [25] I. Moerdijk & E. Palmgren (2000): _Wellfounded Trees in Categories_.  Annals of Pure and Applied Logic 104(1), pp. 189–218, 10.1016/S0168-0072(00)00012-9.
  * [26] I. Moerdijk & E. Palmgren (2002): _Type theories, Toposes and Constructive Set Theory: Predicative Aspects of AST_.  Annals of Pure and Applied Logic 114(1), pp. 155–201, 10.1016/S0168-0072(01)00079-3.
  * [27] B. Nordström, K. Petersson & J. M. Smith (1990): _Programming in Martin-Löf’s Type Theory_.  Oxford University Press.
  * [28] I. Orton & A. M. Pitts (2016): _Axioms for Modelling Cubical Type Theory in a Topos_.  In J.-M. Talbot & L. Regnier, editors: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics (LIPIcs) 62, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 24:1–24:19, 10.4230/LIPIcs.CSL.2016.24.
  * [29] A. M. Pitts & S. C. Steenkamp (2021): _Agda code accompanying this paper_.  Available at https://www.cl.cam.ac.uk/~amp12/agda/coniau.
  * [30] D. M. Roberts (2015): _The Weak Choice Principle WISC may Fail in the Category of Sets_.  Studia Logica 103, pp. 1005–1017, 10.1007/s11225-015-9603-6.
  * [31] M. Shulman (2014): _The surreals contain the plump ordinals_.  Available at https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/.  Homotopy Type Theory blog.
  * [32] C. Sprenger & M. Dam (2003): _On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $\mu$Calculus_.  In A. D. Gordon, editor: Foundations of Software Science and Computation Structures (FoSSaCS 2003), Lecture Notes in Computer Science 2620, Springer, Berlin, Heidelberg., pp. 425–440, 10.1007/3-540-36576-1_27.
  * [33] T. Streicher (2005): _Realizability Models for CZF + $\neg$ Pow_.  Available at http://www2.mathematik.tu-darmstadt.de/~streicher/CIZF/rmczfnp.pdf.  Unpublished note.
  * [34] T. Streicher (2005): _Universes in Toposes_.  In L. Crosilla & P. Schuster, editors: From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics, chapter 4, Oxford Logic Guides 48, Oxford University Press, pp. 78–90, 10.1093/acprof:oso/9780198566519.001.0001.
  * [35] A. Swan (2018): _W-Types with Reductions and the Small Object Argument_.  ArXiv e-prints arXiv:1802.07588 [math.CT].  Available at https://arxiv.org/abs/1802.07588.
  * [36] P. Taylor (1996): _Intuitionistic Sets and Ordinals_.  Journal of Symbolic Logic 61, pp. 705–744, 10.2307/2275781.
  * [37] P. Taylor (1999): _Practical Foundations of Mathematics_.  Cambridge Studies in Advanced Mathematics 59, Cambridge University Press.
  * [38] The Univalent Foundations Program (2013): _Homotopy Type Theory: Univalent Foundations for Mathematics_.  Institute for Advanced Study.  Available at http://homotopytypetheory.org/book.
  * [39] B. van den Berg & I. Moerdijk (2014): _The Axiom of Multiple Choice and Models for Constructive Set Theory_.  Journal of Mathematical Logic 14(01), p. 1450005, 10.1142/S0219061314500056.