# Univalent material set theory

Håkon Robbestad Gylterud  Elisabeth Stenholm

###### Abstract

The aim of this paper is to give a generalisation of material set theory to
higher type levels within homotopy type theory. More specifically, we define
the notion of an $\in$-structure as a type with an extensional binary relation
and generalise the axioms of constructive set theory to higher type levels.
Once an $\in$-structure is given, its elements can be seen as representing
types in the ambient type theory. This perspective is then used to give a
formulation of the axiom of infinity which is does not fix a specific encoding
of the natural numbers.

The theory has an alternative, coalgebraic formulation, in terms of coalgebras
for a certain hierarchy of functors. The coalgebras which furthermore are
fixed-points of their respective functors in the hierarchy are shown to model
the axioms given in the first part. Finally, we show the existence of such
fixed-points by constructing the initial algebras of all the functors in the
hierarchy.

##  1 Introduction

_Material set theories_ are set theories which emphasise the notion of sets as
collections of elements (often themselves sets) and where the identity of
individual elements is tracked across sets, usually with a global, binary
membership relation ($\in$). This category includes Zermelo–Fraenkel (ZF) set
theory. ZF is a theory in the language of first-order logic, intended as a
foundation for mathematics. At the time of ZF’s formulation, fear of
inconsistency necessitated a formal theory, which could be reasoned about
meta-mathematically. In what follows, we work within the framework of
(informal) homotopy type theory (HoTT). HoTT is a structural framework, with
the Univalence Axiom in particular allowing identification of types which are
structurally the same, i.e. equivalent – deemphasising the individual elements
and their identity outside the structure of the type. From this vantage point
we will regard material set theory in the same way that a classical
mathematician regards group theory. Namely, we study a certain type of
mathematical structures, and interest ourselves in their properties and
relationships. The structures we study are not groups, but what we call
$\in$-structures: types with an extensional elementhood relation.

Since we are working in HoTT, we can consider the type level of the underlying
type of sets and of the relation of an $\in$-structure. In classical set
theory, the statement “$x\in y$” is a proposition. But in our setting, we can
consider $\in$-structures where $x\in y$ is a type of any type level.
Similarly, we can generalise the axioms of ZF to higher type levels. An
example of such a $\in$-structure, where $x\in y$ is allowed to be a type of
any level, was considered in _Multisets in type theory_ [7] by one of the
authors.

We aim to give a higher level generalisation of material set theory, by
considering $\in$-structures where $x\in y$ is an $n$-type. With care, the
usual properties, which we know and love from set-theory, can be reformulated
and proven to hold in our models. But sometimes what used to be one property
generalises to several properties when taking higher type levels into
consideration. For instance, for a model on the level of groupoids, $x=x$ may
be a set with several distinct elements. Therefore, there is a distinction
between the singleton $\\{x\\}_{0}$ where $(x\in\\{x\\}_{0})\simeq 1$ and
$\\{x\\}_{\infty}$ which is such that $(x\in\\{x\\}_{\infty})\simeq(x=x)$.

Thus, in section § ‣ 2 we will present a version for each truncation level for
most properties***Exponentiation being a notable exception, since it is the
same exact axiom for each level., the $(-1)$-truncated version being
equivalent to the usual set-theoretic property. The $\infty$-truncated
properties are the same, or slight variations of, the ones presented and
proved for multisets [7].

Another perspective we explore is extracting types from $\in$-structures. A
given element of an $\in$-structure has a type of elements, and considering
the whole $\in$-structure we can ask what types can be represented as types of
elements within it. Some insights into how replacement affects representations
of types, such as $\mathbb{N}$ for the axiom of infinity, has been collected
in section 3.

There is a well-established coalgebraic reading of set theory in which models
of set theory can be understood as coalgebras for the powerset functor on the
category of classes. This can be traced back to Rieger [9], but perhaps found
more explicitly in work by Osius [8].†††More recent work in this direction is
the work of Paul Taylor [11] studying coalgebraic notions of well-foundedness
and recursion. In section 4 we establish a similar correspondence between
$\in$-structures and coalgebras. We define a hierarchy of functors
$\operatorname{T}^{n}_{U}$, relative to a universe, and stratified by type
levels, whose extensional coalgebras correspond to $\in$-structures at the
given type level.

The coalgebraic view also points towards a way to construct $\in$-structures,
since initial algebras are extensional coalgebras. Section 5 demonstrates that
any fixed-point of $\operatorname{T}^{n}_{U}$ gives an $\in$-structure
powerful enough to model the axioms of section § ‣ 2. And finally, section 6
constructs the initial algebra for each of the $\operatorname{T}^{n}_{U}$
functors.

###  1.1 Formalisation

Everything in this paper has been formalised in the Agda proof assistant [1].
Our formalisation builds on the agda-unimath library [10], which is an
extensive library of formalised mathematics from the univalent point of view.

The formalisation for this paper can be found at:
https://git.app.uib.no/hott/hott-set-theory. Throughout the paper there will
also be clickable links to specific lines of Agda code corresponding to a
given result. These will be shown as the Agda logo  .

###  1.2 Notation and universes

A lot of the basic constructions within HoTT have an established notation at
this point in time. Nevertheless, to avoid confusion, we include here a list
of some of the, perhaps less obvious, notation we will use in this paper. The
notation we do not include in this list will usually follow the conventions of
the HoTT Book [12].

  * •

$\mathbf{0}$ denotes the empty type, with eliminator
$\operatorname{ex\mbox{-}falso}$.

  * •

$\mathbf{1}$ denotes the unit type.

  * •

$\mathbf{2}$ denotes the type with two elements.

  * •

$\mathbb{N}$ denotes the type of natural numbers, with constructors $0$ and
$\operatorname{s}$.

  * •

$\operatorname{id\mbox{-}equiv}$ denotes the identity equivalence, on a given
type.

  * •

$f\sim g$ denotes the type of homotopies from $f$ to $g$:
$\prod_{x:X}f\,x=g\,x$.

  * •

$\operatorname{refl\mbox{-}htpy}$ denotes the homotopy $f\sim f$ given by the
map $\lambda\,x.\,\operatorname{refl}$.

  * •

$\operatorname{fiber}\,f\,y$ denotes the homotopy fiber: $\sum_{x:X}f\,x=y$.

  * •

$\pi_{0}$ and $\pi_{1}$ denote the first, respectively second, projection out
of a $\Sigma$-type.

  * •

Given a path $p:x=y$, $p^{-1}$ denotes the inverse path $y=x$.

  * •

Given an invertible function $f$ (usually an equivalence), $f^{-1}$ denotes
the inverse.

  * •

Given a family of maps $f:\prod_{x:X}P\,x\rightarrow Q\,x$,
$\operatorname{total}\,f:\sum_{x:X}P\,x\rightarrow\sum_{x:X}Q\,x$ is the
function: $\lambda\,(x,p).\,(x,f\,x\,p)$.

  * •

$\operatorname{is\mbox{-}}n\operatorname{\mbox{-}trunc\mbox{-}map\,}f$ is the
proposition that $f$ is an $n$-truncated map:
$\prod_{y:Y}\operatorname{is\mbox{-}}n\operatorname{\mbox{-}type\,}(\operatorname{fiber}\,f\,y)$.

  * •

$X\hookrightarrow Y$ is the type of propositionally truncated maps:
$\sum_{f:X\rightarrow
Y}\operatorname{is\mbox{-}}(-1)\operatorname{\mbox{-}trunc\mbox{-}map\,}f$.

  * •

$X\hookrightarrow_{n}Y$ is the type of $n$-truncated maps:
$\sum_{f:X\rightarrow
Y}\operatorname{is\mbox{-}}n\operatorname{\mbox{-}trunc\mbox{-}map\,}f$.

  * •

$X\twoheadrightarrow Y$ is the type of $(-1)$-connected maps:
$\sum_{f:X\rightarrow
Y}\prod_{y:Y}\operatorname{is\mbox{-}contr\,}\|\operatorname{fiber}\,f\,y\|_{-1}$.

  * •

$X\twoheadrightarrow_{n}Y$ is the type of $n$-connected maps:
$\sum_{f:X\rightarrow
Y}\prod_{y:Y}\operatorname{is\mbox{-}contr\,}\|\operatorname{fiber}\,f\,y\|_{n}$

  * •

$\exists!_{x:X}P\,x$ denotes the type:
$\operatorname{is\mbox{-}contr\,}\left(\sum_{x:X}P\,x\right)$.

  * •

$\operatorname{funext}$ is the function $f\sim g\rightarrow f=g$ given by
function extensionality.

  * •

$\operatorname{ua}$ is the function $X\simeq Y\rightarrow X=Y$ given by
univalence.

  * •

$\operatorname{Prop}_{U}$ is the type of all propositions in the universe $U$:
$\sum_{X:U}\operatorname{is\mbox{-}prop\,}X$.

  * •

$\operatorname{Set}_{U}$ is the type of all sets in the universe $U$:
$\sum_{X:U}\operatorname{is\mbox{-}set\,}X$.

  * •

More generally, $n\operatorname{\mbox{-}Type}_{U}$ is the type of all
$n$-types in the universe $U$:
$\sum_{X:U}\operatorname{is\mbox{-}}n\operatorname{\mbox{-}type\,}X$.

We will use the same terminology as the HoTT Book regarding type levels. But
we will also define a notion of _level_ for $\in$-structures and elements in
(the carrier of) an $\in$-structure. This overloading of terminology should be
fine however, since it should be clear from the context what kind of level we
are referring to.

In this paper we will assume two type universes, a large universe, denoted
$\operatorname{Type}$, and a small univalent universe, denoted $U$.‡‡‡The
formalisation differs in this respect as it uses a hierarchy of universes, but
the relationship between $U$ and $\operatorname{Type}$ in the article, is the
same as the relationship between UU i and UU (lsuc i) in the formalisation. We
use cumulative universes, i.e. $U:\operatorname{Type}$ and
$X:\operatorname{Type}$, for all $X:U$. It is assumed that both $U$ and
$\operatorname{Type}$ are closed under the usual type formers, such as
$\Pi$-types, $\Sigma$-types, and identity types. The constructions below also
use the empty type and the type of natural numbers. We will use function
extensionality freely.

From section 4 and onwards, we will also assume that we can construct small
images in certain situations. This assumption is informed by Rijke’s modified
join construction [5], which can be used to construct such small images. One
can alternatively assume that $U$ is closed under homotopy colimits, from
which the smallness of (certain) images follows by the join construction.

##  2 $\in$-structures§§§This section defines the notion of $\in$-structure
slightly differently than $\in$-structures were defined in a previous article
by one of the authors [6]. This difference is by incorporating extensionality
and generalising to higher type levels.

In this section we give the definition of $\in$-structures and formulate
properties of these inspired by set theory. Most of the properties are indexed
by a type level, from 0 to $\infty$. The level 0 version of the property is
equivalent to the usual set theoretic concept for $\in$-structures of level 0,
while the $\infty$ version was explored in [7].

######  Definition 1 ( ).

An $\in$-structure is a pair $(V,\in)$ where $V:\operatorname{Type}$ and
$\in\,:V\rightarrow V\rightarrow\operatorname{Type}$, which is extensional:
for each $x,y:V$, the canonical map $x=y\rightarrow\prod_{z:V}{z\in
x}\simeq{z\in y}$ is an equivalence of types.

Extensionality states that we can distinguish sets by their elements. It is
expressed in first order logic using logical equivalence, but since we are
working in the framework of HoTT and want to allow for elementhood relations
of higher type level, we use instead equivalence of types. This of course
reduces to logical equivalence in the case when the $\in$-relation is
propositional.

Many times we will want to talk about all members of a given element in $V$.
We introduce a notation for this.

######  Definition 2 ( ).

Given an $\in$-structure, $(V,\in)$, we define the family
$\operatorname{El}:V\rightarrow\operatorname{Type}$ by
$\operatorname{El}\,a:=\sum_{x:V}x\in a$.

The usual notion of (extensional) model of set theory corresponds to
$\in$-structures, $(V,\in)$, where $x\in y$ is a mere proposition for each
$x,y:V$ (and consequently $V$ is a mere set). However, there are examples of
extensional $\in$-structures where $V$ is not a mere set. One such example,
based on Aczel’s [2] type $\operatorname{W}_{A:U}A$, was explored in an
article by one of the authors [7].

We can stratify $\in$-structures based on the type level of the
$\in$-relation.

######  Definition 3 ( ).

Given $n:\mathbb{N}_{-2}$, an $\in$-structure $(V,\in)$ is said to be of level
(n+1) if for every $x,y:V$ the type $x\in y$ is an $n$-type.

The following proposition explains the occurrence of $n+1$ in the definition
above:

######  Proposition 1 ( ).

In an $\in$-structure, $(V,\in)$, of level $n$ the type $V$ is an $n$-type.

###### Proof.

Let $(V,\in)$ be an $\in$-structure of level $(n+1)$, for $n:\mathbb{N}_{-2}$.
By extensionality $x=y$ is equivalent to $\prod_{z:V}{z\in x}\simeq{z\in y}$,
which is an $n$-type, hence $V$ is an $(n+1)$-type.∎

Remark: By definition there are no $-2$ level $\in$-structures, and the $-1$
level structures all have trivial $\in$-structure. Thus, we shall from here on
focus on the $\in$-structures of level 0 or higher.

Of special interest will be the elements of an $\in$-structure which look like
sets, in the sense that elementhood is a proposition. This is by definition
the case for all elements in $\in$-structures of level 0, but such elements
may occur in structures of all levels.

######  Definition 4 ( ).

An element $x:V$ is a $(k+1)$-type in $(V,\in)$ if $y\in x$ is of level
$k:\mathbb{N}_{-1}$ for all $y:V$.

If $x:V$ is a $0$-type in $(V,\in)$, we also say it is a _mere set_ in
$(V,\in)$.

######  Proposition 2 ( ).

If $x:V$ is a $(k+1)$-type in $(V,\in)$ then $x=y$ is a $k$-type for any
$y:V$.

Note that $x:V$ being a $k$-type in $(V,\in)$ does not imply that
$\operatorname{El}\,x$ is a $k$-type. However, if $V$ is a $k$-type then
$\operatorname{El}\,x$ is a $k$-type if $x$ is a $k$-type.

###  2.1 Ordered pairing

The characteristic property of ordered pairs is that two pairs are equal if
and only if the first coordinates are equal and the second coordinates are
equal, i.e. it is a pair where the order of the elements matters. In our
setting this means that the ordered pair of two elements $x,y:V$ should be an
element $\langle x,y\rangle:V$ such that for any other ordered pair $\langle
x^{\prime},y^{\prime}\rangle$, for some $x^{\prime},y^{\prime}:V$, $\langle
x,y\rangle=\langle x^{\prime},y^{\prime}\rangle$ exactly when $x=x^{\prime}$
and $y=y^{\prime}$. Using the characterisation of the identity types of
cartesian products, this is equivalently saying that $\langle
x,y\rangle=\langle x^{\prime},y^{\prime}\rangle$ exactly when $(x,y)=_{V\times
V}(x^{\prime},y^{\prime})$. In order to allow for higher level
$\in$-structures the “exactly when” should be replaced with type equivalence.
Moreover, we want it to be the canonical one, in the sense that if $x\equiv
x^{\prime}$ and $y\equiv y^{\prime}$ then the equivalence should send
$\operatorname{refl}$ to $\operatorname{refl}$.

In HoTT, this is the statement that ordered pairing is an embedding $V\times
V\hookrightarrow V$. This neatly encapsulates and generalises the usual
characterisation of equality of ordered pairs in a way that is completely
independent of the level of the $\in$-structure. But it does not uniquely
define the encoding of ordered pairs. Indeed, there are several ways to encode
ordered pairs in ordinary set theory. The usual Kuratowsky pairing will work
for 0-level $\in$-structures, but not for higher level structures. Luckily,
Norbert Wiener’s encoding, $\langle
x,y\rangle:=\\{\\{\\{x\\},\emptyset\\},\\{\\{y\\}\\}\\}$, will work for
structures of any level.

This was originally observed in previous work by one of the authors [7].
However, there the equivalence $\left(\langle x,y\rangle=\langle
x^{\prime},y^{\prime}\rangle\right)\simeq\left((x,y)=_{V\times
V}(x^{\prime},y^{\prime})\right)$ was not required to be the canonical one, as
we require here. Moreover, the encoding of ordered pairs used the untruncated
variants of singletons and unordered pairs. But it may be the case we can only
construct truncated variants in a given $\in$-structure. Therefore, we will
here construct ordered pairs, based on the Wiener encoding, but for any
truncation level of singletons and unordered pairs.

Since the results which follow are independent of encoding, we will not commit
to any specific way of forming ordered pairs, but simply assume ordered
pairing as an extra structure.

######  Definition 5 ( ).

Given an $\in$-structure, $(V,\in)$, an ordered pairing structure on $(V,\in)$
is an embedding $V\times V\hookrightarrow V$.

While having ordered pairing is a structure, once the pairing structure is
fixed, the notion of _being an ordered pair_ is a proposition. As is clear
from the proof below, this fact is just another formulation of the
characterisation of equality of ordered pairs.

######  Proposition 3.

Being an ordered pair is a mere proposition: for a fixed $\in$-structure
$(V,\in)$ with ordered pairing structure $\langle-,-\rangle$, the type
$\sum_{a,b:V}\langle a,b\rangle=x$ is a proposition, for all $x:V$.

###### Proof.

Observe that $\sum_{a,b:V}\langle a,b\rangle=x$ is the fiber of
$\langle-,-\rangle$ over $x$, which is a proposition since $\langle-,-\rangle$
is an embedding.∎

###  2.2 Properties of $\in$-structures

In this section we explore how usual set-theoretic notions, such as pairing,
union, replacement, separation and exponentiation, can be expressed as mere
propositions about $\in$-structures. As mentioned in the introduction, these
notions can be generalised in different ways by using different levels of
truncation. When characterising unions, for instance, it makes a difference
whether the truncated existential quantifier or dependent pair types are used.
With the truncated existential quantifier we only get one copy of each element
in the union, but with the dependent pair type we can get more copies.

A given $\in$-structure can satisfy several versions, but a recurring theme is
that $n$-level structures will only satisfy the $k$-truncated versions for
$k\leq n$.

Convention: _In the rest of the paper we will consider the type of truncation
levels to be the type $\mathbb{N}^{\infty}_{-2}$, i.e. the usual truncation
levels extended by an element $\infty$ for which $\|P\|_{\infty}$ is defined
as $P$ and such that $\infty-1=\infty=\infty+1$._

_The properties of $\in$-structures will be parameterised by truncation level.
If the truncation level is omitted, in the notation or reference to a
property, we mean the variant that is labeled with $0$ (which usually involves
$(-1)$-truncation in the definition)._

Interestingly, even the untruncated versions of the set theoretic properties
end up being propositions. For instance, to have all $\infty$-unions is a mere
property of $\in$-structures. This is because the properties characterise the
material sets they claim existence of up to equality, by extensionality.

######  Proposition 4 ( ).

Given an $\in$-structure, $(V,\in)$, let
$\phi:V\rightarrow\operatorname{Type}$ be a type family on $V$. Then the type
$\sum_{x:V}\prod_{z:V}z\in x\simeq\phi\,z$ is a proposition.

###### Proof.

Assume $(x,\alpha):\sum_{x:V}\prod_{z:V}z\in x\simeq\phi\,z$, then it is
enough to show that the type is contractible. We have the following chain of
equivalences:

$\displaystyle\left(\sum_{x^{\prime}:V}\prod_{z:V}z\in
x^{\prime}\simeq\phi\,z\right)\simeq\left(\sum_{x^{\prime}:V}\prod_{z:V}z\in
x^{\prime}\simeq z\in
x\right)\simeq\left(\sum_{x^{\prime}:V}x^{\prime}=x\right)$

The last type is contractible.∎

####  2.2.1 Unordered tuples

The usual notion of pairing naturally extends to unordered tupling of any
arity. The arity can be expressed by any type. The usual pairing operation is
tupling with respect to the booleans, the singleton operation is tupling for
the unit type, and the empty set is tupling for the empty type. We generalise
the property of having tupling to all truncation levels.

######  Definition 6 ( ).

Given $k:\mathbb{N}^{\infty}_{-1}$ and a type $I$, an $\in$-structure,
$(V,\in)$, has $(k+1)$-unordered $I$-tupling if for every $v:I\rightarrow V$
there is $\\{v\\}_{k+1}:V$ such that
$\prod_{z:V}z\in\\{v\\}_{k+1}\simeq\|\sum_{i:I}v\,i=z\|_{k}$

For the special cases $I=\operatorname{Fin}\,n$, we say that $(V,\in)$ has
$k$-unordered $n$-tupling. If $(V,\in)$ has $k$-unordered $n$-tupling for
every $n:\mathbb{N}$, we say that $(V,\in)$ has finite, $k$-unordered tupling.

We will use the usual notation for finite tuplings, but with a subscript for
the truncation level: $\\{x_{0},\cdots,x_{n-1}\\}_{k}$ is $k$-unordered
$n$-tupling. For $k$-unordered $\mathbf{0}$-tupling we will use the notation
$\emptyset$. Observe that $\\{x_{0},\cdots,x_{n-1}\\}_{k}$ is a $k$-type in
$(V,\in)$.

The set $\emptyset$ is the set with no elements. For any $z:V$ we have:

$\displaystyle
z\in\emptyset\simeq\Big{\|}\sum_{i:\mathbf{0}}\operatorname{ex\mbox{-}falso}\,i=z\
\Big{\|}_{k-1}\simeq\|\ \mathbf{0}\ \|_{k-1}\simeq\mathbf{0}$ (1)

Note here that the truncation level $k$ does not matter (hence why we exclude
it from the notation $\emptyset$). By extensionality, the sets corresponding
to $k$-unordered and $k^{\prime}$-unordered $\mathbf{0}$-tupling, for any two
$k$ and $k^{\prime}$, are equal. Note also that $\emptyset$ is a mere set in
any $\in$-structure.

Remark: We say that an $\in$-structure, $(V,\in)$, has empty set if there is
an element $x:V$ such that $\prod_{z:V}z\in x\simeq\mathbf{0}$. By the
previous paragraph, this is equivalent to saying that $(V,\in)$ has
$\mathbf{0}$-tupling.

However, the singletons $\\{x\\}_{k}$ may be different for different
truncation levels. For any $x,z:V$ we have:

$\displaystyle z\in\\{x\\}_{k}\simeq\Big{\|}\sum_{i:\mathbf{1}}x=z\
\Big{\|}_{k-1}\simeq\|\ x=z\ \|_{k-1}$ (2)

In the special case when $x$ is a mere set in $(V,\in)$, the truncation level
does not matter in that $\\{x\\}_{k}=\\{x\\}_{0}$, by extensionality. As an
example: $\\{\emptyset\\}_{k}=\\{\emptyset\\}_{k^{\prime}}$ for any two $k$
and $k^{\prime}$, since $\emptyset$ is a mere set.

For $\in$-structures of higher level, the higher level versions of tupling may
occur. Higher level tupling differs from 0-tupling in that repetitions matter:
In $\infty$-unordered tupling,
$\emptyset\in\\{\emptyset,\emptyset\\}_{\infty}$ would be a type with two
elements, and thus $\\{\emptyset,\emptyset\\}_{\infty}$ is distinct from
$\\{\emptyset\\}_{\infty}$, while
$\\{\emptyset,\emptyset\\}_{0}=\\{\emptyset\\}_{0}$. In fact, for any $k>0$ it
is the case that $\\{\emptyset,\emptyset\\}_{k}\neq\\{\emptyset\\}_{k}$. In
general, $x\in\\{x\\}_{\infty}\simeq(x=_{M}x)$, which may be a type of any
level. In comparison, $x\in\\{x\\}_{0}$ is contractible for any $x$ in any
$\in$-structure with 0-unordered 1-tupling.

As another example of how the truncation levels work for unordered tupling,
the two sets $\\{\\{\emptyset,\emptyset\\}_{1}\\}_{0}$ and
$\\{\\{\emptyset,\emptyset\\}_{1}\\}_{\infty}$ are not equal. This is because
$\\{\emptyset,\emptyset\\}_{1}=\\{\emptyset,\emptyset\\}_{1}$ is a type with
two elements (one which equates the first two elements with each other and the
second two with each other, and one which equates the first element of each
set with the second of the other). So
$\\{\emptyset,\emptyset\\}_{1}\in\\{\\{\emptyset,\emptyset\\}_{1}\\}_{\infty}$
is a proper set and
$\\{\emptyset,\emptyset\\}_{1}\in\\{\\{\emptyset,\emptyset\\}_{1}\\}_{0}$ is
the propositional truncation of this set. These two types are distinct and
therefore
$\\{\\{\emptyset,\emptyset\\}_{1}\\}_{0}\neq\\{\\{\emptyset,\emptyset\\}_{1}\\}_{\infty}$
by extensionality.

####  2.2.2 Ordered pairs from unordered tuples

As noted above, ordered pairs can be constructed from the empty set,
singletons and unordered pairs, using Norbert Wiener’s definition: $\langle
x,y\rangle:=\\{\\{\\{x\\},\emptyset\\},\\{\\{y\\}\\}\\}$. In $\in$-structures
of arbitrary level it makes sense to ask what level of truncation
$\\{-\\}_{k}$ and $\\{-,-\\}_{k^{\prime}}$ should be used when defining
ordered pairs. The construction using the $(-1)$-truncated variants does not
work in higher level structures since
$\\{\\{\\{x\\}_{0},\emptyset\\}_{0},\\{\\{y\\}_{0}\\}_{0}\\}_{0}=\\{\\{\\{x^{\prime}\\}_{0},\emptyset\\}_{0},\\{\\{y^{\prime}\\}_{0}\\}_{0}\\}_{0}$
is a proposition, while $(x,y)=(x^{\prime},y^{\prime})$ need not be.

If $(V,\in)$ has level $n$, then we know that $(x,y)=(x^{\prime},y^{\prime})$
has type level $n-1$. For that case the $(n-1)$-truncated variants would give
us the correct type level for $\langle x,y\rangle=\langle
x^{\prime},y^{\prime}\rangle$. But, we observe that
$\\{-\\}_{n}=\\{-\\}_{\infty}$ in $\in$-structures of level $n$ since we have
$z\in\\{x\\}_{n}\simeq\|z=x\|_{n-1}\simeq(z=x)$. For unordered pairs we need
to distinguish between the $(-1)$-truncated case and all other cases since
coproducts are not closed under propositions. More specifically, for $n\geq 1$
we have $\\{-,-\\}_{n}=\\{-,-\\}_{\infty}$ if $(V,\in)$ has level $n$, since
$z\in\\{x,y\\}_{n}\simeq\|z=x+z=y\|_{n-1}\simeq(z=x+z=y)$. This equivalence
does not hold for $n=0$ and arbitrary $x,y:V$. However, if $x\neq y$, then
$z=x\rightarrow z\neq y$ and the equivalence holds. We use these observations
to make a general construction of ordered pairs which we can instantiate for
$\in$-structures of all levels.

######  Lemma 1 ( ).

Given an $\in$-structure, $(V,\in)$, with an operation $\alpha:V\times
V\rightarrow V$ with equivalences $e:\prod_{x,y:V}x\neq
y\rightarrow\prod_{z:V}z\in\alpha(x,y)\simeq(z=x+z=y)$, and two disjoint
embeddings, $f\ g:V\hookrightarrow V$, i.e. $\prod_{x,y:V}f\,x\neq g\,y$, then
$\alpha\circ(f\times g):V\times V\rightarrow V$ is an embedding.

###### Proof.

We need to show, for any $(x,y),(x^{\prime},y^{\prime}):V\times V$, that
$\operatorname{ap}_{\alpha\circ(f\times
g)}:(x,y)=(x^{\prime},y^{\prime})\rightarrow\alpha(f\,x,g\,y)=\alpha(f\,x^{\prime},g\,y^{\prime})$
is an equivalence. To this end, it is enough to construct some equivalence
between the identity types that sends
$\operatorname{refl}:\alpha(f\,x,g\,y)=\alpha(f\,x,g\,y)$ to
$\operatorname{refl}:(x,y)=(x,y)$.

We have the following chain of equivalences:

$\displaystyle\left(\alpha(f\,x,g\,y)=\alpha(f\,x^{\prime},g\,y^{\prime})\right)$
$\displaystyle\simeq\prod_{z:V}z\in\alpha(f\,x,g\,y)\simeq
z\in\alpha(f\,x^{\prime},g\,y^{\prime})$ (3)
$\displaystyle\simeq\prod_{z:V}(z=f\,x+z=g\,y)\simeq(z=f\,x^{\prime}+z=g\,y^{\prime})$
(4)
$\displaystyle\simeq\prod_{z:V}((z=f\,x)\simeq(z=f\,x^{\prime}))\times((z=g\,y)\simeq(z=g\,y^{\prime}))$
(5)
$\displaystyle\simeq\left(\prod_{z:V}(z=f\,x)\simeq(z=f\,x^{\prime})\right)\times\left(\prod_{z:V}(z=g\,y)\simeq(z=g\,y^{\prime})\right)$
(6)
$\displaystyle\simeq\left(f\,x=f\,x^{\prime}\right)\times\left(g\,y=g\,y^{\prime}\right)$
(7)
$\displaystyle\simeq\left(x=x^{\prime}\right)\times\left(y=y^{\prime}\right)$
(8) $\displaystyle\simeq((x,y)=(x^{\prime},y^{\prime}))$ (9)

In step (3) we use extensionality for $(V,\in)$. In step (4) we use the
equivalences $e\,(f\,x)\,(g\,y)$ and $e\,(f\,x^{\prime})\,(g\,y^{\prime})$,
together with the fact that $f\,x\neq g\,y$ and $f\,x^{\prime}\neq
g\,y^{\prime}$. The equivalence (5) follows from the fact that $z=f\,x$ and
$z=g\,y^{\prime}$, and $z=f\,x^{\prime}$ and $z=g\,y$, are, respectively,
mutually exclusive. In step (8) we use the fact that $f$ and $g$ are
embeddings.

We chase $\operatorname{refl}:\alpha(f\,x,g\,y)=\alpha(f\,x,g\,y)$ through the
equivalence:

$\displaystyle\operatorname{refl}$
$\displaystyle\mapsto\lambda\,z.\operatorname{id\mbox{-}equiv}$ (10)
$\displaystyle\mapsto\lambda\,z.\left(e\,z\right)\circ\operatorname{id\mbox{-}equiv}\circ\left(e\,z\right)^{-1}$
(11) $\displaystyle=\ \lambda\,z.\operatorname{id\mbox{-}equiv}$ (12)
$\displaystyle\mapsto\lambda\,z.(\operatorname{id\mbox{-}equiv},\operatorname{id\mbox{-}equiv})$
(13)
$\displaystyle\mapsto(\lambda\,z.\operatorname{id\mbox{-}equiv},\lambda\,z.\operatorname{id\mbox{-}equiv})$
(14) $\displaystyle\mapsto(\operatorname{refl},\operatorname{refl})$ (15)
$\displaystyle=\
\left(\operatorname{ap}_{f}\,\operatorname{refl},\operatorname{ap}_{g}\,\operatorname{refl}\right)$
(16)
$\displaystyle\mapsto\left(\operatorname{ap}_{f}^{-1}\left(\operatorname{ap}_{f}\,\operatorname{refl}\right),\operatorname{ap}_{g}^{-1}\left(\operatorname{ap}_{g}\,\operatorname{refl}\right)\right)$
(17) $\displaystyle=\ (\operatorname{refl},\operatorname{refl})$ (18)
$\displaystyle\mapsto\ \operatorname{refl}$ (19)

where we have used the fact that extensionality for $(V,\in)$ sends
$\operatorname{refl}$ to $\operatorname{id\mbox{-}equiv}$.∎

For the Norbert Wiener construction of ordered pairs we thus have to show that
both $\\{\\{-\\}_{n}\\}_{n}$ and $\\{\\{-\\}_{n},\emptyset\\}_{n}$ are
embeddings. Using the previous observation about the relationship between the
$n$-truncated versions and the $\infty$-truncated ones, it is enough to show
this for the $\infty$-truncated versions.

######  Lemma 2 ( ).

The function $\\{-\\}_{\infty}:V\rightarrow V$ is an embedding.

###### Proof.

We follow the same outline as the proof of Lemma 1. For any $x,y:V$ we have
the following chain of equivalences:

$\displaystyle\left(\\{x\\}_{\infty}=\\{y\\}_{\infty}\right)$
$\displaystyle\simeq\prod_{z:V}z\in\\{x\\}_{\infty}\simeq
z\in\\{y\\}_{\infty}$ (20)
$\displaystyle\simeq\prod_{z:V}\left(z=x\right)\simeq\left(z=y\right)$ (21)
$\displaystyle\simeq\left(x=y\right)$ (22)

In step (20) we use extensionality for $(V,\in)$.

Let $e:\prod_{x:V}\prod_{z:V}z\in\\{x\\}_{\infty}\simeq\left(z=x\right)$ be
the defining family of equivalences for $\\{-\\}_{\infty}$. We chase
$\operatorname{refl}:\\{x\\}_{\infty}=\\{x\\}_{\infty}$ along the chain of
equivalences above:

$\displaystyle\operatorname{refl}$
$\displaystyle\mapsto\lambda\,z.\operatorname{id\mbox{-}equiv}$ (23)
$\displaystyle\mapsto\lambda\,z.(e\,x\,z)\circ\operatorname{id\mbox{-}equiv}\circ(e\,x\,z)^{-1}$
(24) $\displaystyle=\ \lambda\,z.\operatorname{id\mbox{-}equiv}$ (25)
$\displaystyle\mapsto\operatorname{refl}$ (26)

In step (23) we use the fact that extensionality for $(V,\in)$ sends
$\operatorname{refl}$ to $\operatorname{id\mbox{-}equiv}$.∎

######  Lemma 3 ( ).

Let $\alpha:V\rightarrow V\rightarrow V$ be such that $e:\prod_{x,y:V}x\neq
y\rightarrow\prod_{z:V}z\in\alpha\,x\,y\simeq(z=x+z=y)$. Then
$\lambda\,x.\,\alpha\,\\{x\\}_{\infty}\,\emptyset:V\rightarrow V$ is an
embedding.

###### Proof.

First, we observe that for all $x:V$, $\\{x\\}_{\infty}\neq\emptyset$ since
$x\in\\{x\\}_{\infty}$ is inhabited but $x\in\emptyset$ is empty. We now
follow the same outline as the proof of Lemma 1. For any $x,y:V$ we have the
following chain of equivalences:

$\displaystyle\left(\alpha\,\\{x\\}_{\infty}\,\emptyset=\alpha\,\\{y\\}_{\infty}\,\emptyset\right)$
$\displaystyle\simeq\prod_{z:V}z\in\alpha\,\\{x\\}_{\infty}\,\emptyset\simeq
z\in\alpha\,\\{y\\}_{\infty}\,\emptyset$ (27)
$\displaystyle\simeq\prod_{z:V}\left(z=\\{x\\}_{\infty}+z=\emptyset\right)\simeq\left(z=\\{y\\}_{\infty}+z=\emptyset\right)$
(28)
$\displaystyle\simeq\prod_{z:V}\left((z=\\{x\\}_{\infty})\simeq(z=\\{y\\}_{\infty})\right)\times\left((z=\emptyset)\simeq(z=\emptyset)\right)$
(29)
$\displaystyle\simeq\prod_{z:V}(z=\\{x\\}_{\infty})\simeq(z=\\{y\\}_{\infty})$
(30) $\displaystyle\simeq\left(\\{x\\}_{\infty}=\\{y\\}_{\infty}\right)$ (31)
$\displaystyle\simeq\left(x=y\right)$ (32)

In step (27) we use extensionality for $(V,\in)$. In step (29) we use the fact
that $\\{x\\}_{\infty}\neq\emptyset$ and $\\{y\\}_{\infty}\neq\emptyset$. In
step (30) we use the fact that $(z=\emptyset)\simeq(z=\emptyset)$ is
contractible since $\emptyset$ is a mere set, and hence $z=\emptyset$ is a
proposition. In step (32) we use Lemma 2.

We chase
$\operatorname{refl}:\alpha\,\\{x\\}_{\infty}\,\emptyset=\alpha\,\\{x\\}_{\infty}\,\emptyset$
along the chain of equivalences above:

$\displaystyle\operatorname{refl}$
$\displaystyle\mapsto\lambda\,z.\operatorname{id\mbox{-}equiv}$ (33)
$\displaystyle\mapsto\lambda\,z.(e\,z)\circ\operatorname{id\mbox{-}equiv}\circ(e\,z)^{-1}$
(34) $\displaystyle=\ \lambda\,z.\operatorname{id\mbox{-}equiv}$ (35)
$\displaystyle\mapsto\lambda\,z.(\operatorname{id\mbox{-}equiv},\operatorname{id\mbox{-}equiv})$
(36) $\displaystyle\mapsto\lambda\,z.\operatorname{id\mbox{-}equiv}$ (37)
$\displaystyle\mapsto\operatorname{refl}$ (38) $\displaystyle=\
\operatorname{ap}_{\\{-\\}_{\infty}}\,\operatorname{refl}$ (39)
$\displaystyle\mapsto\operatorname{ap}_{\\{-\\}_{\infty}}^{-1}\,\left(\operatorname{ap}_{\\{-\\}_{\infty}}\,\operatorname{refl}\right)$
(40) $\displaystyle=\ \operatorname{refl}$ (41)

In step (33) we use the fact that extensionality for $(V,\in)$ sends
$\operatorname{refl}$ to $\operatorname{id\mbox{-}equiv}$.∎

######  Theorem 1 ( ).

If $(V,\in)$ is an $\in$-structure of level $n$ which has $\emptyset$,
$\\{-\\}_{n}$ and $\\{-,-\\}_{n}$, then it has an ordered pairing structure
given by
$\lambda\,(x,y).\\{\\{\\{x\\}_{n},\emptyset\\}_{n},\\{\\{y\\}_{n}\\}_{n}\\}_{n}$.

###### Proof.

Corollary of Lemma 1, Lemma 2 and Lemma 3.∎

####  2.2.3 Restricted separation

In constructive set theory, restricted separation is the ability to construct
sets of the form $\\{z\in x\,|\,\Phi\,z\\}$, for a formula $\Phi$ where all
quantifiers are bounded (i.e. $\forall a\in b\cdots$ and $\exists a\in
b\cdots$). The usual way to internalise this to type theory is to require that
the predicate $\Phi:V\rightarrow\operatorname{Prop}_{U}$ is a predicate of
propositions in $U$. We do the same here in that we require the predicate to
take values in $U$, but as with the other properties, we generalise to higher
truncation levels.

######  Definition 7 ( ).

An $\in$-structure, $(V,\in)$, has $U$-restricted $(k+1)$-separation, for
$k:\mathbb{N}^{\infty}_{-1}$, if for every $x:V$ and $P:V\rightarrow
k\operatorname{\mbox{-}Type}_{U}$ there is an element $\\{x\,|\,P\\}:V$ such
that $\prod_{z:V}z\in\\{x\,|\,P\\}\simeq((z\in x)\times P\,z)$.

####  2.2.4 Replacement

Replacement says that given a set $a$, and a description of how to replace its
elements, we can create a new set containing exactly the replacements of
elements in $a$. Of course, two elements in $a$ may be replaced by the same
elements, so the property must include truncation.

######  Definition 8 ( ).

An $\in$-structure, $(V,{\in})$, has $(k+1)$-replacement, for
$k:\mathbb{N}^{\infty}_{-1}$, if for every $a:V$ and
$f:\operatorname{El}\,a\rightarrow V$ there is an element $\\{f(x)\,|\,x\in
a\\}:V$ such that $\prod_{z:V}z\in\\{f(x)\,|\,x\in
a\\}\simeq\big{\|}\sum_{x:\operatorname{El}\,a}f\,x=z\;\big{\|}_{k}$

Remark: Having $k$-replacement is to have $k$-unordered $I$-tupling for
$I=\operatorname{El}a$, for any $a:V$.

In Section 3 we further explore the implications of $k$-replacement and how it
affects representations of types within $\in$-structures.

####  2.2.5 Union

Just as for tupling, there is a notion of union to consider for each type
level, for $\in$-structures, distinguished by the truncation of the
existential quantifier.

######  Definition 9 ( ).

An $\in$-structure, $(V,\in)$, has $(k+1)$-union, for
$k:\mathbb{N}^{\infty}_{-1}$, if for every $x:V$ there is $\bigcup_{k}x:V$
such that $\prod_{z:V}z\in\bigcup_{k}x\simeq\big{\|}\sum_{y:V}\;z\in y\
\times\ y\in x\;\big{\|}_{k}$.

As usual, from pairing and general unions, one can define binary $k$-union by
$x\cup_{k}y:=\bigcup_{k}\\{x,y\\}_{k}$. For $z:V$ we have:

$\displaystyle z\in x\cup_{k}y$ $\displaystyle\simeq\Big{\|}\sum_{w:V}\;z\in
w\ \times\ w\in\\{x,y\\}_{k}\Big{\|}_{k-1}$ (42)
$\displaystyle\simeq\Big{\|}\sum_{w:V}\;z\in w\ \times\
\|w=x+w=y\|_{k-1}\Big{\|}_{k-1}$ (43)
$\displaystyle\simeq\Big{\|}\sum_{w:V}\;z\in w\ \times\
\left(w=x+w=y\right)\Big{\|}_{k-1}$ (44) $\displaystyle\simeq\Big{\|}z\in
x+z\in y\Big{\|}_{k-1}$ (45)

Binary $0$-union corresponds to the usual binary union in set theory, in that
copies are discarded, while in higher level binary union copies are kept. For
example,
$\\{\emptyset\\}_{\infty}\cup_{0}\\{\emptyset\\}_{\infty}=\\{\emptyset\\}_{0}$,
while
$\\{\emptyset\\}_{\infty}\cup_{k}\\{\emptyset\\}_{\infty}=\\{\emptyset,\emptyset\\}_{k}$,
for $k\geq 1$.

####  2.2.6 Exponentiation

Exponentiation states that for any two sets $a$ and $b$ there is a set that
contains exactly the functions from $a$ to $b$. In order to express this
property we need to first generalise the notion of a function internal to an
$\in$-structure. As opposed to the other properties, the notion of a function
can be expressed in a uniform way for $\in$-structures of any level. As in
usual set theory, the notion of a function is relative to a choice of ordered
pairing structure.

######  Definition 10 ( ).

Given three elements $a,b,f:V$ in an $\in$-structure $(V,\in)$ with ordered
pairing $\langle-,-\rangle:V\times V\hookrightarrow V$, define a type:

$\displaystyle\operatorname{operation}_{a\,b}\,f:=$
$\displaystyle\left(\prod_{x:V}\,x\in a\simeq\sum_{y:V}\langle x,y\rangle\in
f\right)$ $\displaystyle\times$
$\displaystyle\left(\prod_{x:V}\prod_{y:V}\langle x,y\rangle\in f\rightarrow
y\in b\right)$ $\displaystyle\times$ $\displaystyle\left(\prod_{z:V}\,z\in
f\rightarrow\sum_{x:V}\,\sum_{y:V}\,z=\langle x,y\rangle\right)$

The first conjunct of $\operatorname{operation}_{a\,b}\,f$ states that the
pairs in $f$ form an operation with domain $a$, and the second states that its
codomain is $b$. The third conjunct, which is always a proposition by
Proposition 3, states that $f$ only contains pairs.

Note that $\operatorname{operation}$ here is the same as Definition 8 in [7].
However, in this paper we define another type which we show is equivalent to
$\operatorname{operation}$ and which is of a more type theoretic flavor.

The type $\operatorname{operation}_{a\,b}\,f$ is not always a proposition.
Hence, an element $p:\operatorname{operation}_{a\,b}\,f$ should be regarded as
an operation structure on $f$ with domain $a$ and codomain $b$. However, in
the case when $a$ and $b$ are mere sets, $\operatorname{operation}_{a\,b}\,f$
is a proposition.

######  Proposition 5 ( ).

Given three elements $a,b,f:V$ in an $\in$-structure $(V,\in)$ with ordered
pairing $\langle-,-\rangle:V\times V\hookrightarrow V$, if $a$ and $b$ are
mere sets in $(V,\in)$, then $\operatorname{operation}_{a\,b}\,f$ is a
proposition and is equivalent to the following type:

$\displaystyle\left(\prod_{x:V}\,x\in
a\rightarrow\underset{y:V}{\exists!}\langle x,y\rangle\in f\right)$
$\displaystyle\times$ $\displaystyle\left(\prod_{x:V}\prod_{y:V}\langle
x,y\rangle\in f\ \rightarrow\ x\in a\ \times\ y\in b\right)$
$\displaystyle\times$ $\displaystyle\left(\prod_{z:V}\,z\in
f\rightarrow\sum_{x:V}\,\sum_{y:V}\,z=\langle x,y\rangle\right)$

###### Proof.

We start by proving the equivalence. First, we observe that for any $x:V$,
$p:x\in a$, and function $e:\sum_{y:V}\langle x,y\rangle\in f\rightarrow x\in
a$ we have an equivalence

$\displaystyle\operatorname{fiber}\,e\ p\ \simeq\sum_{y:V}\langle
x,y\rangle\in f$

since for any $q:\sum_{y:V}\langle x,y\rangle\in f$ the type $e\,q=p$ is
contractible because $a$ is a mere set. It thus follows that for any $x:V$ we
have

$\displaystyle\left(x\in a\simeq\sum_{y:V}\langle x,y\rangle\in f\right)$
$\displaystyle\simeq\sum_{e:\sum_{y:V}\langle x,y\rangle\in f\rightarrow x\in
a}\prod_{p:x\in
a}\operatorname{is\mbox{-}contr\,}(\operatorname{fiber}\,e\,p)$
$\displaystyle\simeq\left(\sum_{y:V}\langle x,y\rangle\in f\rightarrow x\in
a\right)\times\left(x\in a\rightarrow\underset{y:V}{\exists!}\langle
x,y\rangle\in f\right)$

The desired equivalence follows from this, after some currying and
rearranging.

Since $\exists!_{y:V}\langle x,y\rangle\in f$ is a proposition it follows that
$\left(\prod_{x:V}\,x\in a\rightarrow\exists!_{y:V}\langle x,y\rangle\in
f\right)$ is a proposition. When $a$ and $b$ are mere sets, $x\in a\ \times\
y\in b$ is a proposition, and hence $\\\ \left(\prod_{x:V}\prod_{y:V}\langle
x,y\rangle\in f\ \rightarrow\ x\in a\ \times\ y\in b\right)$ is a proposition.
Finally, since ordered pairing is an embedding, and
$\sum_{x:V}\,\sum_{y:V}\,z=\langle x,y\rangle$ is essentially the fibres of
the pairing operation, it follows that $\left(\prod_{z:V}\,z\in
f\rightarrow\sum_{x:V}\,\sum_{y:V}\,z=\langle x,y\rangle\right)$ is a
proposition.∎

This equivalence was proven as Lemma 6.10 in [6] for the type $V$ constructed
there. Here we show the equivalence for general $\in$-structures.

######  Corollary 1.

If $(V,\in)$ is of level 0 then $\operatorname{operation}_{a\,b}\,f$ is a
proposition, for all $a,b,f:V$.

We can now define exponentiation for $\in$-structures.

######  Definition 11 ( ).

An $\in$-structure, $(V,\in)$ with an ordered pairing structure, has
exponentiation if for every two $a,b:V$ there is an element $b^{a}$ such that
$\prod_{f:V}(f\in b^{a})\simeq\operatorname{operation}_{a\,b}\,f$.

While $\operatorname{operation}$ is a straightforward internalisation of the
set theoretic definition of a function, it can be inconvenient to work with.
What follows is a definition that is equivalent to $\operatorname{operation}$
but which is sometimes easier to use.

######  Definition 12 ( ).

Given three elements $a,b,f:V$ in an $\in$-structure $(V,\in)$ with ordered
pairing $\langle-,-\rangle:V\times V\hookrightarrow V$, define a type:

$\displaystyle\operatorname{operation^{\prime}}_{a\,b}\,f:=$
$\displaystyle\sum_{\phi:\operatorname{El}\,a\,\rightarrow\,\operatorname{El}\,b}\
\prod_{z:V}\left(z\in f\simeq\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\
x,\pi_{0}\,(\phi\ x)\rangle=z\right)$

######  Proposition 6 ( ).

For any $a,b,f:V$ we have the following equivalence:

$\displaystyle\operatorname{operation}_{a\,b}\,f\simeq\operatorname{operation^{\prime}}_{a\,b}\,f$

Before we prove this equivalence we prove two general lemmas that we will
need, concerning fiberwise functions and equivalences.

######  Lemma 4 ( ).

Let $A$ and $B$ be types and let $C:B\rightarrow\operatorname{Type}$ be a type
family over $B$. For any embedding $f:A\hookrightarrow B$ and element
$\gamma:\prod_{(b,c):\sum_{b:B}C\,b}\operatorname{fiber}\,f\ b$ we have an
equivalence

$\displaystyle\sum_{a:A}C\,(f\ a)\simeq\sum_{b:B}C\,b.$

###### Proof.

Let $F:\sum_{a:A}C\,(f\ a)\rightarrow\sum_{b:B}C\,b$ be the function given by
$F\,(a,c):=(f\,a,c)$. For $(b,c):\sum_{b:B}C\,b$, we have the following chain
of equivalences:

$\displaystyle\operatorname{fiber}\,F\,(b,c)$
$\displaystyle\simeq\sum_{a:A}\sum_{c^{\prime}:C\,(f\,a)}\sum_{p:f\,a=b}\operatorname{tr}^{C}_{p}c^{\prime}=c$
(46)
$\displaystyle\simeq\sum_{a:A}\sum_{p:f\,a=b}\sum_{c^{\prime}:C\,(f\,a)}c^{\prime}=\operatorname{tr}^{C}_{p^{-1}}c$
(47) $\displaystyle\simeq\operatorname{fiber}\,f\,b$ (48)

Step (48) uses the fact that
$\sum_{c^{\prime}:C\,(f\,a)}c^{\prime}=\operatorname{tr}^{C}_{p^{-1}}c$ is
contractible.

Thus, $\operatorname{fiber}\,F\ (b,c)$ is a proposition, since $f$ is an
embedding, which is inhabited by $\gamma$, and therefore contractible.∎

There is an equivalence between fiberwise equivalences and equivalences of the
total spaces that respect the first coordinate. This will be useful several
times because it gives two equivalent characterisations of equality in slices
over a type.

######  Lemma 5 ( ).

For any type $A$, and any families $P,Q:A\rightarrow\operatorname{Type}$ we
have that

$\left(\prod_{x:A}P\,x\rightarrow
Q\,x\right)\,\simeq\,\left(\sum_{\alpha:\sum_{x:A}P\,x\rightarrow\sum_{x:A}Q\,x}\pi_{0}\circ\alpha=\pi_{0}\right)$

###### Proof.

We have the following chain of equivalences:

$\displaystyle\left(\prod_{x:A}P\,x\rightarrow Q\,x\right)$
$\displaystyle\simeq\prod_{(x,\\_):\sum_{x:A}P\,x}Q\,x$ (49)
$\displaystyle\simeq\prod_{(x,\\_):\sum_{x:A}P\,x}\;\sum_{(x^{\prime},\\_):\sum_{x^{\prime}:A}x^{\prime}=x}Q\,x^{\prime}$
(50)
$\displaystyle\simeq\prod_{(x,\\_):\sum_{x:A}P\,x}\;\sum_{(x^{\prime},\\_):\sum_{x^{\prime}:A}Q\,x^{\prime}}x^{\prime}=x$
(51)
$\displaystyle\simeq\sum_{\alpha:\sum_{x:A}P\,x\rightarrow\sum_{x:A}Q\,x}\pi_{0}\circ\alpha=\pi_{0}$
(52)

where (49) is currying, (50) follows from the fact that
$\sum_{x^{\prime}:A}x^{\prime}=x$ is contractible and (52) is the interchange
law between $\Sigma$-types and $\Pi$-types, together with function
extensionality. The equivalence sends $f$ to
$(\operatorname{total}\,f,\operatorname{refl})$.∎

Remark: Lemma 5 has been independently added by Egbert Rijke to the agda-
unimath library [10]. The proof there is slightly different, with an direct
construction of the equivalence, instead of equivalence reasoning.

######  Corollary 2 ( ).

For any type $A$, and any families $P,Q:A\rightarrow\operatorname{Type}$ we
have an equivalence

$\left(\prod_{x:A}P\,x\,\simeq\,Q\,x\right)\,\simeq\,\left(\sum_{\alpha:\sum_{x:A}P\,x\,\simeq\,\sum_{x:A}Q\,x}\pi_{0}\circ\alpha=\pi_{0}\right)$

###### Proof.

This follows from Lemma 5 by an application of Theorem 4.7.7 in the HoTT book
[12, p. 185], which states that a fiberwise transformation is a fiberwise
equivalence if and only if the corresponding total function is an
equivalence.∎

###### Proof of Proposition 6.

We outline the key steps of the equivalence. For full details see the Agda
formalisation. We have the following chain of equivalences:

$\displaystyle\operatorname{operation}_{a\,b}\,f\simeq$
$\displaystyle\left(\prod_{z:\operatorname{El}\,f}\operatorname{fiber}\
\langle-,-\rangle\ (\pi_{0}\ z)\right)$ (53) $\displaystyle\times$
$\displaystyle\left(\sum_{\sigma:\operatorname{El}\,a\simeq\sum_{(x,y):V\times
V}\langle x,y\rangle\in f}\pi_{0}\sim\pi_{0}\circ\pi_{0}\circ\sigma\right)$
$\displaystyle\times$ $\displaystyle\left(\sum_{\phi:\sum_{(x,y):V\times
V}\langle x,y\rangle\in
f\rightarrow\operatorname{El}\,b}\pi_{0}\circ\phi\sim\pi_{1}\circ\pi_{0}\right)$
$\displaystyle\simeq$
$\displaystyle\sum_{\gamma:\prod_{z:\operatorname{El}\,f}\operatorname{fiber}\
\langle-,-\rangle\ (\pi_{0}\ z)}$ (54) $\displaystyle\hskip
16.0pt\left(\sum_{\sigma:\operatorname{El}\,a\simeq\operatorname{El}\,f}\pi_{0}\circ\sigma^{-1}\sim\pi_{0}\circ\pi_{0}\circ\gamma\right)$
$\displaystyle\hskip
6.0pt\times\left(\sum_{\phi:\operatorname{El}\,f\rightarrow\operatorname{El}\,b}\pi_{0}\circ\phi\sim\pi_{1}\circ\pi_{0}\circ\gamma\right)$
$\displaystyle\simeq$
$\displaystyle\sum_{\sigma:\operatorname{El}\,a\simeq\operatorname{El}\,f}\sum_{\phi:\operatorname{El}\,f\rightarrow\operatorname{El}\,b}\prod_{z:\operatorname{El}\,f}$
(55) $\displaystyle\hskip 16.0pt\sum_{(x,y):V\times V}\left(\langle
x,y\rangle=\pi_{0}\,z\right)\times\left(\pi_{0}\,(\sigma^{-1}\
z)=x\right)\times\left(\pi_{0}\,(\phi\ z)=y\right)$ $\displaystyle\simeq$
$\displaystyle\sum_{\sigma:\operatorname{El}\,a\simeq\operatorname{El}\,f}\sum_{\phi:\operatorname{El}\,f\rightarrow\operatorname{El}\,b}\prod_{z:\operatorname{El}\,f}\langle\pi_{0}\,(\sigma^{-1}\
z),\pi_{0}\,(\phi\ z)\rangle=\pi_{0}\ z$ (56) $\displaystyle\simeq$
$\displaystyle\sum_{\phi:\operatorname{El}\,a\rightarrow\operatorname{El}\,b}\sum_{\sigma:\operatorname{El}\,a\simeq\operatorname{El}\,f}\prod_{x:\operatorname{El}\,a}\langle\pi_{0}\
x,\pi_{0}\,(\phi\ x)\rangle=\pi_{0}\,(\sigma\ x)$ (57) $\displaystyle\simeq$
$\displaystyle\ \operatorname{operation^{\prime}}_{a\,b}\,f$ (58)

where in (53) we apply Corollary 2 to the first conjunct and Lemma 5 to the
second conjunct, and then rearrange. In (54) we use Lemma 4 to construct an
equivalence $\sum_{(x,y):V\times V}\langle x,y\rangle\in
f\simeq\operatorname{El}\,f$ which we apply in the second and third conjuncts.
In (55) we rearrange and then use the interchange law for $\prod$-types and
$\sum$-types. In (56) we use extensionality for cartesian products and the
fact that $\sum_{(x,y):V\times V}(\pi_{0}\,(\sigma^{-1}\
z),\pi_{0}\,(\phi\,z))=(x,y)$ is contractible. In (57) we swap
$\operatorname{El}\,a$ for $\operatorname{El}\,f$ and then rearrange. Finally,
in (58) we use Corollary 2 again.

∎

The notion of $\operatorname{operation^{\prime}}$ captures type theoretic
functions in the sense that the type of all operations from $a:V$ to $b:V$ is
a subtype of the type $\operatorname{El}a\rightarrow\operatorname{El}b$.

######  Proposition 7 ( ).

Given $a,b:V$ in an $\in$-structure $(V,\in)$ with ordered pairing
$\langle-,-\rangle$, there is a canonical embedding

$\displaystyle\left(\sum_{f:V}\operatorname{operation^{\prime}}_{a\,b}\,f\right)\hookrightarrow\left(\operatorname{El}a\rightarrow\operatorname{El}b\right)$

###### Proof.

By swapping the $\Sigma$-types we have the following equivalence

$\displaystyle\left(\sum_{f:V}\operatorname{operation^{\prime}}_{a\,b}\,f\right)\simeq\sum_{\phi:\operatorname{El}a\rightarrow\operatorname{El}b}\sum_{f:V}\prod_{z:V}\left(z\in
f\simeq\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\ x,\pi_{0}\,(\phi\
x)\rangle=z\right)$ (59)

The type $\sum_{f:V}\prod_{z:V}\left(z\in
f\simeq\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\ x,\pi_{0}\,(\phi\
x)\rangle=z\right)$ is a proposition, by Proposition 4. The embedding is thus
the composition of (59) with the first projection.∎

An operation from $a:V$ to $b:V$ is thus a function from
$\operatorname{El}a\rightarrow\operatorname{El}b$. A natural question to ask
is when all functions $\operatorname{El}a\rightarrow\operatorname{El}b$
correspond to some operation.

######  Proposition 8 ( ).

Given $a,b:V$ in an $\in$-structure $(V,\in)$ of level
$n:\mathbb{N}^{\infty}$, with ordered pairing $\langle-,-\rangle$, the
embedding in Proposition 7 is an equivalence if $(V,\in)$ has $n$-replacement.

###### Proof.

Suppose $(V,\in)$ has $n$-replacement. By applying it to the map
$\lambda\,x.\langle\pi_{0}\ x,\pi_{0}\,(\phi\
x)\rangle:\operatorname{El}a\rightarrow V$, we get an element of the following
type:

$\displaystyle\sum_{f:V}\prod_{z:V}\left(z\in
f\simeq\Big{\|}\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\ x,\pi_{0}\,(\phi\
x)\rangle=z\Big{\|}_{n-1}\right)$

Claim: The type $\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\
x,\pi_{0}\,(\phi\ x)\rangle=z$ is $(n-1)$-truncated.

Given that the claim is true we can drop the truncation. Thus the type

$\displaystyle\sum_{f:V}\prod_{z:V}\left(z\in
f\simeq\sum_{x:\operatorname{El}\,a}\langle\pi_{0}\ x,\pi_{0}\,(\phi\
x)\rangle=z\right)$

is contractible, because it is an inhabited proposition, and hence the
embedding constructed in Proposition 7 is an equivalence.

It remains to prove the claim. First, we have the following equivalence:

$\displaystyle\sum_{x:\operatorname{El}\,a}\left(\langle\pi_{0}\
x,\pi_{0}\,(\phi\
x)\rangle=z\right)\simeq\sum_{(x,y):\operatorname{El}a\times\operatorname{El}b}\left(\langle\pi_{0}\
x,\pi_{0}\,y\rangle=z\right)\times\left(\phi\ x=y\right)$ (60)

This follows from the fact that $\sum_{y:\operatorname{El}b}\phi\ x=y$ is
contractible. The type $\phi\ x=y$ is $(n-1)$-truncated since $V$ is an
$n$-type, by Proposition 1. The type
$\sum_{(x,y):\operatorname{El}a\times\operatorname{El}b}\left(\langle\pi_{0}\
x,\pi_{0}\ y\rangle=z\right)$ is the fiber of the composite map
$\langle-,-\rangle\circ(\pi_{0}\times\pi_{0})$ over $z:V$. The map
$\langle-,-\rangle$ is an embedding and thus an $(n-1)$-truncated map. The
fibers of the two projection maps over $z$ are $z\in a$ and $z\in b$
respectively. These types are $(n-1)$-truncated. So the composite map is
$(n-1)$-truncated, and the claim follows.∎

####  2.2.7 Accessible elements and foundation

We choose the same approach as the HoTT book [12][10.3] to well-foundedness,
namely accessibility predicates. The axiom of foundation is then the statement
that all elements are accessible. This need not be true in a given
$\in$-structure, but the subtype of accessible elements inherits the
$\in$-structure from the base type. This new $\in$-structure satisfies
foundation.

######  Definition 13 ( ).

Given an $\in$-structure, $(V,\in)$, define inductively the predicate
$\operatorname{Acc}:V\rightarrow\operatorname{Type}$ by

  * •

$\operatorname{acc}:\prod_{x:V}(\prod_{y:V}y\in
x\rightarrow\operatorname{Acc}y)\rightarrow\operatorname{Acc}x$

######  Lemma 6 ( ).

For every $x:V$ the type $\operatorname{Acc}x$ is a mere proposition.

###### Proof.

Lemma 10.3.2 in the HoTT book [12, p. 454].∎

######  Definition 14 ( ).

An $\in$-structure, $(V,\in)$, has foundation if
$\prod_{x:V}\operatorname{Acc}x$.

Since accessibility is a proposition, we can define for a given
$\in$-structure, the subtype of accessible elements.

######  Definition 15 ( ).

Given an $\in$-structure, $(V,\in)$, define the type
$V_{\operatorname{Acc}}:=\sum_{x:V}\operatorname{Acc}x$ and define the binary
relation
$\in_{\operatorname{Acc}}:=\lambda\,(x:V_{\operatorname{Acc}})\,(y:V_{\operatorname{Acc}}).\,\pi_{0}\,x\in\pi_{0}\,y$.

The subtype of accessible elements inherits the $\in$-structure from the base
type.

######  Proposition 9 ( ).

Given an $\in$-structure, $(V,\in)$, the pair
$(V_{\operatorname{Acc}},\in_{\operatorname{Acc}})$ forms an $\in$-structure.

###### Proof.

We need to prove extensionality for
$(V_{\operatorname{Acc}},\in_{\operatorname{Acc}})$. For
$x,y:V_{\operatorname{Acc}}$ we have the following chain of equivalences:

$\displaystyle\left(x=y\right)$
$\displaystyle\simeq\left(\pi_{0}\,x=\pi_{0}\,y\right)$ (61)
$\displaystyle\simeq\prod_{z:V}z\in\pi_{0}\,x\simeq z\in\pi_{0}\,y$ (62)
$\displaystyle\simeq\sum_{e\,:\,\sum_{z:V}z\in\pi_{0}\,x\ \simeq\
\sum_{z:V}z\in\pi_{0}\,y}\pi_{0}\circ e\sim\pi_{0}$ (63)
$\displaystyle\simeq\sum_{e\,:\,\sum_{z:V}\left(z\in\pi_{0}\,x\right)\times\left(\operatorname{Acc}z\right)\
\simeq\
\sum_{z:V}\left(z\in\pi_{0}\,y\right)\times\left(\operatorname{Acc}z\right)}\pi_{0}\circ
e\sim\pi_{0}$ (64)
$\displaystyle\simeq\sum_{e\,:\,\sum_{z:V_{\operatorname{Acc}}}\pi_{0}\,z\in\pi_{0}\,x\
\simeq\ \sum_{z:V_{\operatorname{Acc}}}\pi_{0}\,z\in\pi_{0}\,y}\pi_{0}\circ
e\sim\pi_{0}$ (65)
$\displaystyle\simeq\prod_{z:V_{\operatorname{Acc}}}z\in_{\operatorname{Acc}}x\simeq
z\in_{\operatorname{Acc}}y$ (66)

In step (61) we use Lemma 6. Step (62) is extensionality for $(V,\in)$ and
step (63) is Corollary 2. In step (64) we use the fact that elements of
accessible sets are accessible and thus $\operatorname{Acc}z$ is contractible.
Step (65) is some rearranging of conjuncts in the base type together with the
characterisation of equality in subtypes for the fibration. The last step is
again an application of Corollary 2.

Chasing $\operatorname{refl}$ along this chain of equivalences we see that it
is sent to $\lambda\,z.\operatorname{id\mbox{-}equiv}$.∎

The subtype of accessible elements satisfies foundation.

######  Theorem 2 ( ).

Given an $\in$-structure, $(V,\in)$, the $\in$-structure
$(V_{\operatorname{Acc}},\in_{\operatorname{Acc}})$ has foundation.

###### Proof.

There are two different accessibility predicates at play here. Let
$\operatorname{Acc}$ and $\operatorname{acc}$ be accessibility with respect to
$(V,\in)$ and let $\operatorname{Acc}^{\prime}$ and
$\operatorname{acc}^{\prime}$ be accessibility with respect to
$(V_{\operatorname{Acc}},\in_{\operatorname{Acc}})$. We need to show
$\prod_{x:V_{\operatorname{Acc}}}\operatorname{Acc}^{\prime}x$, which we do by
using the induction principle of $\operatorname{Acc}$ (modulo a transport):

$\displaystyle\alpha:\prod_{x:V_{\operatorname{Acc}}}\operatorname{Acc}^{\prime}x$
$\displaystyle\alpha(x,\operatorname{acc}\,f):=\operatorname{acc}^{\prime}\,\left(\lambda\,(y:V_{\operatorname{Acc}})(p:\pi_{0}\,y\in
x).\,\alpha(\pi_{0}\,y,f\,(\pi_{0}\,y)\,p)\right)$

∎

##  3 Internalisations of types in $\in$-structures

Any element $a:V$ gives rise to a type $\operatorname{El}a$ (Definition 2),
and in some sense $a$ represents $\operatorname{El}a$ inside the bigger
structure of $(V,\in)$. For instance, an operation from $a$ to $b$ is
precisely a function from $\operatorname{El}a\rightarrow\operatorname{El}b$
(Proposition 7). A natural question to ask is: Which types can be represented
as elements in this way in a given $\in$-structure? In this section we
introduce some basic vocabulary for talking about this kind of representation.
We apply this by giving a very flexible formulation of the axiom of infinity –
which constructively is often formulated as the existence of a set collecting
the natural numbers for some chosen encoding of these. The flexibility of our
formulation is that it takes the encoding as a parameter, making very few
assumptions about it. We prove that for $\in$-structures that satisfy
replacement, the existence of a set of natural numbers is independent of
encoding.

###  3.1 Internalisations and representations

For the rest of this section, fix an $\in$-structure $(V,\in)$ and
$A:\operatorname{Type}$.

######  Definition 16 ( ).

A $(V,\in)$-internalisation of $A$ is an element $a:V$ such that
$\operatorname{El}a\simeq A$.

There can be several different internalisations of $A$. However, if we fix an
encoding of the elements of $A$ in $V$, there is at most one element in $V$
which is an internalisation of $A$ with respect to this encoding.

An encoding of the elements of $A$ in $V$ is a function $A\rightarrow V$. We
will call this a representation because of the superficial similarity with
classical representation theory, which can be seen as the study of functors
$G\rightarrow\operatorname{Vec}_{k}$ for some group $G$ and field $k$. In our
case representations are functions $A\rightarrow V$ where $A$ can be any type
(not necessarily a group), and the codomain is some $\in$-structure.

######  Definition 17 ( ).

A $(V,\in)$-representation of $A$ is a function $A\rightarrow V$.

Our main concern is going to be if a given representation gives rise to an
internalisation of the domain in the $\in$-structure itself. In other words,
if the elements pointed out by the representation can be collected to a set
such that the type of elements is exactly the type being represented.

######  Definition 18 ( ).

Given a $(V,\in)$-representation of $A$, say $f:A\rightarrow V$, let an
internalisation of $f$ be an $a:V$ such that for every $z:V$ we have $z\in
a\simeq\operatorname{fiber}f\,z$.

We say that a representation is internalisable if there is an internalisation
of it. An internalisation of a representation is an internalisation of the
domain.

######  Proposition 10 ( ).

Let $f:A\rightarrow V$ be a $(V,\in)$-representation of $A$ and let $a:V$ be
an internalisation of $f$. Then $a$ is an internalisation of $A$.

###### Proof.

By Lemma 4.8.2 in the HoTT book [12], we have:

$\displaystyle\operatorname{El}a\equiv\left(\sum_{z:V}z\in
a\right)\simeq\left(\sum_{z:V}\operatorname{fiber}f\,z\right)\simeq A$

∎

Once a representation of a type is fixed, the internalisation is uniquely
defined. Thus, we will speak of _the_ internalisation of a given
representation.

######  Proposition 11 ( ).

Given a $(V,\in)$-representation of $A$, say $f:A\rightarrow V$, the
internalisation of $f$ is uniquely defined. That is, the type
$\sum_{a:V}\prod_{z:V}\left(z\in a\simeq\operatorname{fiber}f\,z\right)$ is a
proposition.

###### Proof.

Corollary of Proposition 4.∎

To take some of the mystery out of where the notions of representation and
internalisation comes from, we have a simpler formulation of the type of all
internalisable representations of a type, $A$. It is the type of all
internalisations of $A$.

######  Proposition 12 ( ).

The type of all internalisable $(V,\in)$-representations of $A$,
$\sum_{f:A\rightarrow V}\sum_{a:V}\prod_{z:V}z\in
a\simeq\operatorname{fiber}f\,z$ is equivalent to the type of all
internalisations of $A$, $\sum_{a:V}\left(\operatorname{El}\,a\simeq
A\right)$.

###### Proof.

For $a:A$, we have the following chain of equivalences:

$\displaystyle\left(\sum_{f:A\rightarrow V}\prod_{z:V}z\in
a\simeq\operatorname{fiber}f\,z\right)$
$\displaystyle\simeq\sum_{f:A\rightarrow V}\sum_{e:\operatorname{El}a\simeq
A}f\circ e=\pi_{0}$ (67) $\displaystyle\simeq\sum_{e:\operatorname{El}a\simeq
A}\sum_{f:A\rightarrow V}f=\pi_{0}\circ e^{-1}$ (68)
$\displaystyle\simeq\left(\operatorname{El}a\simeq A\right)$ (69)

Step (67) is an application of Corollary 2. We rearrange in step (68), and
finally, step (69) is the fact that the total space of paths from a given
point is contractible.

The desired equivalence follows from the equivalence above, after some
rearranging.∎

If a representation $f:A\rightarrow V$ is an embedding, we say that the
representation is _faithful_. The truncation level of a representation
determines the level of the internalisation. In the special case of a faithful
representation, the internalisation is a mere set.

######  Proposition 13 ( ).

An internalisation of $f:A\rightarrow V$ is a $(k+1)$-type if and only if $f$
is a $k$-truncated representation, for $k:\mathbb{N}_{-1}$.

###### Proof.

Let $a:V$ be an internalisation of $f$. Then $a$ is a $(k+1)$-type if and only
if $\operatorname{fiber}f\,z$ is a $k$-type, for all $z:V$. In other words,
$a$ is a $(k+1)$-type if and only if $f$ is a $k$-truncated map.∎

Note here that if $f$ is a faithful representation, it is not necessarily the
case that the type $A$ itself is a set. A mere set in $V$ can be the
internalisation of a faithful representation of a type of any level, as long
as it can be embedded into $V$. An exception to this is if $V$ is of level 0,
meaning that it _only_ contains mere sets, then $V$ itself is a set, all
internalisable representations are faithful, and hence any type with an
internalisable representation will be a set.

Representations and internalisations give an interesting perspective on
replacement. In classical set theory, replacement is the axiom schema which
says that if you have a set you can replace its elements and still get a set,
as long as the replacements are uniquely defined (by a formula in the first-
order language of set theory). In terms of representations we can view this as
follows: Given an internalised representation of a type as a set, any other
representation can be internalised by replacing the elements of the
internalisation by their alternate representation. The various levels of
replacement properties correspond to restrictions on what kind of
representations can be replaced. For instance, 0-replacement gives the
replacement property for faithful representations.

######  Proposition 14 ( ).

If $(V,\in)$ satisfies $(k+1)$-replacement and $A$ has an internalisation,
then any $k$-truncated representation $f:A\rightarrow V$ of $A$ has an
internalisation.

###### Proof.

Let $a:V$ be an internalisation of $A$, with a given
$\alpha:\operatorname{El}a\simeq A$. Then apply $(k+1)$-replacement to
$f\circ\alpha:\operatorname{El}a\rightarrow V$ to obtain $b:V$ such that for
all $z:V$ there is an equivalence

$\displaystyle z\in
b\simeq\Big{\|}\sum_{x:\operatorname{El}\,a}f(\alpha\,x)=z\Big{\|}_{k}$ (70)

Since $f$ is $k$-truncated and $\alpha$ is an equivalence, we can drop the
truncation, and we have

$\displaystyle z\in b\simeq\sum_{x:\operatorname{El}\,a}f(\alpha\,x)=z$ (71)

Since $\alpha$ is an equivalence
$\left(\sum_{x:\operatorname{El}\,a}f(\alpha\,x)=z\right)\simeq\left(\sum_{x:A}f\,x=z\right)$,
which gives the desired equivalence $z\in b\simeq\sum_{x:A}f\,x=z$, proving
that $b$ internalises $f$.∎

###  3.2 Natural Numbers / Infinity

There are many ways of formulating the axiom of infinity. The simplest
formulation is perhaps $\exists\,u\,(\emptyset\in u\wedge\forall\,x\in u\
\exists\,y\in u\ x\in y)$, which can be found in some texts, such as Bell [3].
This formulation depends on foundation for the result to actually be an
infinite set, as this axiom is also satisfied by the co-hereditarily finite
sets (the final coalgebra of the the finite powerset functor), by the element
defined by the equation $x=\\{\emptyset,x\\}$. Another approach is to define
the notion of a successor set, for instance $s\,x=x\cup\\{x\\}$ or
$s\,x=\\{x\\}$ and then postulate the existence of a set containing
$\emptyset$ and which is closed under $s$. This becomes an infinite set even
without foundation, since the successor function preserves well-foundedness
and increases rank.

In Aczel’s CZF [2], the axiom of infinity is formulated as the existence of a
set of natural numbers, $\exists\,z\,\operatorname{Nat}(z)$. Aczel’s
formulation of this axiom determines the set of natural numbers uniquely if
foundation is assumed. However, if foundation is not assumed, one may have
fixed points of the successor function which can be thrown in while still
satisfying Aczel’s $\operatorname{Nat}$ predicate. For instance, given a quine
atom, $q=\\{q\\}$, then for any $n$ we have
$\operatorname{Nat}(n)\rightarrow\operatorname{Nat}(n\cup q)$. This can be
remedied by further assuming that $n$ is accessible, in which case $n$ is
uniquely determined.

When choosing a property corresponding to the axiom infinity for
$\in$-structures in general, we will leverage the fact that we are not bound
by first-order logic, and try to give a direct and intuitive formulation,
which does not depend on foundation or assumptions about accessibility. We
will also keep to the principle that properties postulating existence of sets
should be uniquely determined, or be explicitly given as extra structure.
Therefore, we will _not_ say that an $\in$-structure has natural numbers to
mean that $\mathbb{N}$ has an internalisation, as the type
$\sum_{a:V}\operatorname{El}a\simeq\mathbb{N}$ is not a proposition. Having an
internalisation of a type is a structure, rather than a property. However,
having an internalisation _with respect to a fixed representation_ is a
property (Proposition 11), and it is the one we will use.

We will follow Aczel in choosing the natural numbers as the canonical infinite
set, but leave the exact encoding of the natural numbers as extra structure.
This leaves room for some exotic natural numbers, as they might not even be
mere sets. Once an encoding is given, the set of naturals is uniquely
determined, and will from a certain point of view behave like the usual
natural numbers.

######  Definition 19 ( ).

Given an $\in$-structure $(V,\in)$ with a representation of $\mathbb{N}$,
$f:\mathbb{N}\rightarrow V$, we say that $(V,\in)$ has natural numbers
represented by $f$ if $f$ has an internalisation.

Suppose $n$ is a set of natural numbers represented by $f$ and let
$e:\operatorname{El}n\simeq\mathbb{N}$ be the equivalence given by Proposition
10. Then we can define zero as

$\displaystyle\operatorname{zero}:\operatorname{El}n$ (72)
$\displaystyle\operatorname{zero}:=e^{-1}\,0$ (73)

and we can define the successor function as

$\displaystyle\operatorname{suc}:\operatorname{El}n\rightarrow\operatorname{El}n$
$\displaystyle\operatorname{suc}x=e^{-1}\circ\operatorname{s}\circ e$

where $\operatorname{s}$ is the successor function on $\mathbb{N}$.

The usual induction principle holds, with respect to $\operatorname{zero}$ and
$\operatorname{suc}$.

######  Proposition 15 ( ).

Given an $\in$-structure $(V,\in)$ with natural numbers $n:V$ represented by
$f:\mathbb{N}\rightarrow V$, let
$P:\operatorname{El}n\rightarrow\operatorname{Type}$ be a type family on
$\operatorname{El}n$. Given $P\,\operatorname{zero}$ and
$\prod_{x:\operatorname{El}n}P\,x\rightarrow P\,(\operatorname{suc}\,x)$,
there is an element of the type $\prod_{x:\operatorname{El}n}P\,x$.

###### Proof.

Let $e:\operatorname{El}n\simeq\mathbb{N}$ be the equivalence given by
Proposition 10. The result follows from the induction principle on
$\mathbb{N}$, transported along $e$.∎

######  Example 1 ( ).

Let $(V,\in)$ be an $\in$-structure with the empty set, 0-singletons and
binary 0-union. Then we can define the usual von Neumann representation of the
natural numbers $f:\mathbb{N}\rightarrow V$ recursively by $f\,0:=\emptyset$
and $f\,(k+1):=f\,k\cup_{0}\\{f\,k\\}_{0}$. This will be a faithful
representation, and an $\in$-structure having natural numbers represented by
$f$ will be equivalent to the usual characterisations of the von Neumann
natural numbers in set theory, such as the axiom of infinity in CZF (in the
well-founded sets).

######  Example 2.

Let $(V,\in)$ be an $\in$-structure with the empty set, binary 1-union and
0-singletons, then let $f:\mathbb{N}\rightarrow V$ be defined by
$f\,0:=\emptyset$ and $f\,(k+1):=f\,k\cup_{1}\\{\emptyset\\}_{0}$. This
representation of $\mathbb{N}$ is not faithful, since $f\,k$ has non-trivial
automorphisms when k > 1\. For instance
$f\,3=\\{\emptyset,\emptyset,\emptyset\\}_{1}$ has $3!=6$ automorphisms. An
internalisation, $n:V$, of this representation would be a multiset with the
interesting property that $(f\,k\in n)\simeq\operatorname{Fin}(k!)$.

Interestingly, as long as there is enough replacement in the $\in$-structure,
the exact choice of representation of $\mathbb{N}$ does not matter:

######  Proposition 16 ( ).

If $(V,\in)$ satisfies $(k+1)$-replacement and has natural numbers for some
representation, then $(V,\in)$ has natural numbers represented by $f$ for any
$k$-truncated representation $f$.

###### Proof.

Suppose $(V,\in)$ has natural numbers for some representation. By Proposition
10 it follows that $\mathbb{N}$ has an internalisation. Thus the result
follows by Proposition 14.∎

##  4 Equivalence of extensional coalgebras and U-like $\in$-structures

We will mimic the usual categorical view of set theory, where a model of set
theory is a class $V$ together with a coalgebra structure $R:V\rightarrow
P\,V$ for the powerset functor on classes. Instead of classes and the powerset
functor, we will have types and specific functors $\operatorname{T}^{n}_{U}$
on types, parameterised by a choice of a univalent universe.

######  Definition 20 ( ).

For $n:\mathbb{N}_{-1}^{\infty}$, define
$\operatorname{T}_{U}^{n+1}:\operatorname{Type}\rightarrow\operatorname{Type}$
by $\operatorname{T}_{U}^{n+1}\,X=\sum_{A:U}A\hookrightarrow_{n}X$.

Remark: $\operatorname{T}^{\infty}_{U}$ is a polynomial functor, but for
finite $n$, $\operatorname{T}^{n}_{U}$ is _not_ polynomial. Note that
$\operatorname{T}^{0}_{U}$ is a $U$-restricted ‘powerset functor’ in that
$\operatorname{T}^{0}_{U}\,X$ is the type of $U$-small subtypes of $X$.

The functorial action of $\operatorname{T}^{n}_{U}$ on a function
$f:X\rightarrow Y$ is to postcompose with $f$ and then take the $(n-1)$-image
and the $(n-1)$-image inclusion. There is a size issue with this though. With
the usual construction of the $n$-image as
$\sum_{b:B}\|\sum_{a:A}g\,a=b\|_{n}$ [12], this type is in $U$ if $U$ is
closed under truncation and if both the domain and the codomain are in $U$. In
our case the domain is in $U$, but the codomain need not be. Is it possible to
weaken the assumption that the codomain is in $U$ (given that the domain is)
and still conclude that the $n$-image is in $U$?

###  4.1 Images of small types

As a higher groupoid, the image of a function $f:X\rightarrow Y$ looks like it
has the points from $X$, but the paths are the paths from $Y$ resulting from
applying $f$. For example, consider the function
$f:\mathbf{1}\rightarrow\operatorname{Type}$ given by $f\,x:=\mathbf{2}$. The
image of $f$ is the type $\sum_{x:\operatorname{Type}}\|\mathbf{2}=x\|_{-1}$.
There is one point, namely $(\mathbf{2},|\operatorname{refl}|_{-1})$. However,
by univalence, there are two distinct paths
$(\mathbf{2},|\operatorname{refl}|_{-1})=(\mathbf{2},|\operatorname{refl}|_{-1})$:
the identity equivalence and the equivalence that flips the elements in
$\mathbf{2}$ (we only need to consider equality on the first coordinate).

More generally, the $n$-image looks like it has the $k$-cells, for $k\leq
n+1$, from $X$, but the $(n+2)$-cells are the $(n+2)$-cells from $Y$ between
the $(n+1)$-cells resulting from applying $f$. _From this intuition it seems
reasonable that if all the $(n+2)$-iterated identity types of $Y$ lie in $U$,
along with $X$, then the resulting higher groupoid $n$-image also lies in
$U$._

It turns out that it is enough to assume that this holds for $(-1)$-images. As
pointed out below, this is not true for all univalent universes, but the
results presented here will rely upon the assumption that this holds for our
particular universe.

Rijke’s modified join construction [5] proves that a sufficient criterion for
this smallness of images assumption to hold in a univalent universe is that
$U$ is closed under homotopy colimits (or has graph quotients), and that
global function extensionality holds. Here, we have chosen instead to directly
assume that images of $U$-small types into locally $U$-small types are
$U$-small.

The formulation of this assumption relies on two natural notions of smallness
— which are also found in Rijke’s work [5] along with the fact that being
small a proposition. We generalise to a definition of local smallness at any
level.

######  Definition 21 ( ).

A type $X$ is essentially $U$-small if there is $A:U$ such that $A\simeq X$.
That is, $\sum_{A:U}A\simeq X$.

We proceed by induction to define local smallness at higher levels.

######  Definition 22 ( ).

Let $X$ be a type. We define the notion of $X$ being $n$-locally $U$-small,
for $n:\mathbb{N}^{\infty}$, as follows:

  * •

$X$ is $0$-locally $U$-small if it is essentially $U$-small.

  * •

$X$ is $(n+1)$-locally $U$-small if for all $x,y:X$, the identity type $x=y$
is $n$-locally $U$-small.

  * •

$X$ is $\infty$-locally $U$-small.

We say that a $1$-locally $U$-small type is locally $U$-small.

######  Lemma 7 ( ).

Being essentially $U$-small is a mere proposition.

###### Proof.

We must show that the type $\sum_{A:U}A\simeq X$ is a mere proposition. This
type looks close to being of the form $\sum_{b:T}b=a$, which is known to be
contractible, but since $X$ is not a type in the universe we cannot directly
apply univalence. Instead we give a direct proof based on the definition of
being a mere proposition.

Let $(A,\alpha)$ and $(B,\beta)$ be two elements of $\sum_{A:U}A\simeq X$.
Applying univalence, we observe that
$\operatorname{ua}\,(\beta^{-1}\cdot\alpha):A=B$.

It remains to show that we get $\beta$ by transporting $\alpha$ along the path
$\operatorname{ua}\,(\beta^{-1}\cdot\alpha)$, in the family
$\lambda(Y:U).Y\simeq X$. But this is easily computed with path algebra:

$\displaystyle\operatorname{tr}^{\lambda Y.Y\simeq
X}_{\operatorname{ua}\,(\beta^{-1}\cdot\alpha)}\alpha$
$\displaystyle=\alpha\cdot(\beta^{-1}\cdot\alpha)^{-1}$
$\displaystyle=\alpha\cdot\alpha^{-1}\cdot\beta$ $\displaystyle=\beta$

∎

Now, the following assumption, which will be assumed throughout the rest of
the paper, can be formulated:

######  Assumption 1 (Images of small types  ).

For every small type $A:U$ and every locally $U$-small $X:Type$, and given a
function $f:A\rightarrow X$, there is a $U$-small type
$\operatorname{image}\,f:U$, and functions
$\operatorname{surj}f:A\twoheadrightarrow\operatorname{image}\,f$ and
$\operatorname{incl}f:\operatorname{image}\,f\hookrightarrow X$, such that for
every $a:A$ we have $\operatorname{incl}f\ (\operatorname{surj}f\,x)\equiv
f\,x$.

Remark: Not all univalent universes satisfy the above assumption. For
instance, given any univalent universe, $U$, we can define the subuniverse of
mere sets, $\operatorname{Set}_{U}$. This subuniverse is univalent, and
locally $\operatorname{Set}_{U}$-small, but the image of the map
$(\lambda\,x.\mathbf{2}):\mathbf{1}\rightarrow\operatorname{Set}_{U}$ is not a
set, as we saw above. Thus, the image of this map is not essentially
$\operatorname{Set}_{U}$-small.

While the work in this article is presented informally in type theory, there
might be some benefit here to spell out the assumption as formulated in Agda.
This formulation is uniform in universe levels (the parameters i and j) so
that it can be applied at any level.

    module _ {i j}
             {Domain : Type i} {Codomain : Type j}
             (_ : is-locally-small i Codomain)
             (f : Domain  Codomain) where

      postulate Image : Type i

      postulate image-inclusion : Image  Codomain

      postulate image-quotient : Domain  Image

      postulate image-
         :  x  (image-inclusion  image-quotient  x  )  f x

      {-# REWRITE image- #-}

This code can be found in the project source repository, where the file
containing the above snippet is called image-factorisation.agda ( ).

From the assumption of small $(-1)$-images, the smallness of $n$-images
follows.

######  Proposition 17 ( ).

Let $n:\mathbb{N}^{\infty}_{-2}$. For every small type $A:U$ and every
$(n+2)$-locally $U$-small $X:\operatorname{Type}$, and given a function
$f:A\rightarrow X$, there is a small type $\operatorname{image}_{n}\,f:U$,
together with an $n$-connected map
$\operatorname{surj}_{n}f:A\twoheadrightarrow_{n}\operatorname{image}_{n}\,f$
and an $n$-truncated map
$\operatorname{incl}_{n}f:\operatorname{image}_{n}\,f\hookrightarrow_{n}X$,
such that for every $a:A$ we have $\operatorname{incl}f\
(\operatorname{surj}f\,x)=f\,x$.

###### Proof.

This is Proposition 2.2 in [4], but we will also give our own proof here. Let
$A:U$ and $X:Type$ be $n$-locally $U$-small, and let $f:A\rightarrow X$. We
proceed by induction on $n$.

For the base case we need to construct a type $\operatorname{image}_{-2}\,f:U$
together with a $(-2)$-connected map
$\operatorname{surj}_{-2}f:A\twoheadrightarrow_{-2}\operatorname{image}\,f$
and a $(-2)$-truncated map
$\operatorname{incl}_{-2}f:\operatorname{image}\,f\hookrightarrow_{-2}X$. Note
that any map is $(-2)$-connected and that $(-2)$-truncated maps are precisely
equivalences. By assumption $X$ is essentially $U$-small, i.e. there is a type
$X^{\prime}:U$ together with an equivalence $e:X\simeq X^{\prime}$. So we take
$\operatorname{image}_{-2}\,f:=X^{\prime}$, $\operatorname{surj}_{-2}f:=e\circ
f$ and $\operatorname{incl}_{-2}f:=e^{-1}$.

Suppose the proposition holds for $n$, and suppose $X$ is $(n+1)$-locally
$U$-small. Let $\operatorname{image}^{HoTT}_{n}g$ denote the HoTT Book
definition of the $n$-image of a function $g$ [12, Def. 7.6.3]. We will show
that $\operatorname{image}^{HoTT}_{n-1}f$ is essentially $U$-small. By Theorem
7.6.6 in [12] we have a factorisation

${A}$${X}$${\operatorname{image}^{HoTT}_{n-1}f}$$\scriptstyle{f}$$\scriptstyle{s}$$\scriptstyle{i}$

where $s$ is $(n-1)$-connected and $i$ is $(n-1)$-truncated. The map $s$ is in
particular surjective, so by the uniqueness of the image factorisation,
$\operatorname{image}^{HoTT}_{n-1}f\simeq\operatorname{image}\,s$. Thus we are
done if we can show that $\operatorname{image}^{HoTT}_{n-1}f$ is locally
$U$-small. Since being $U$-small is a proposition and $s$ is surjective, it is
enough to show that $s\,x=s\,y$ is essentially $U$-small for all $x,y:A$. But
by the characterisation of equality in $n$-images we have the equivalence
$\left(s\,x=s\,y\right)\simeq\operatorname{image}^{HoTT}_{n-2}\,\left(\operatorname{ap}_{f}\,x\,y\right)$.
The domain $x=y$ of $\operatorname{ap}_{f}\,x\,y$ is in $U$ and the codomain
$f\,x=f\,y$ is $n$-locally $U$-small by assumption. Thus, by the induction
hypothesis and the uniqueness of the $(n-2)$-image factorisation,
$\operatorname{image}^{HoTT}_{n-2}\,\left(\operatorname{ap}_{f}\,x\,y\right)\simeq\operatorname{image}_{n-2}\,\left(\operatorname{ap}_{f}\,x\,y\right)$
and thus $s\,x=s\,y$ is essentially $U$-small.

For the case $n=\infty$, note that an $\infty$-connected map is an equivalence
and that any map is $\infty$-truncated. Thus we take
$\operatorname{image}_{\infty}\,f:=A$,
$\operatorname{surj}_{\infty}\,f:=\operatorname{id\mbox{-}equiv}$ and
$\operatorname{incl}_{\infty}\,f:=f$.∎

###  4.2 The functor $\operatorname{T}^{n}_{U}$

With the construction of $U$-small $n$-images, we can define the functorial
action of $\operatorname{T}^{n}_{U}$. For $n:\mathbb{N}^{\infty}$, and two
types $X,Y$ such that $Y$ is $(n+1)$-locally $U$-small, the $(n-1)$-image of
any function $\phi:X\rightarrow Y$, $\operatorname{image}_{n-1}\,\phi$, lies
in $U$ by Proposition 17. Moreover, the image inclusion
$\operatorname{incl}_{n-1}\,\phi:\operatorname{image}_{n-1}\,\phi\rightarrow
Y$ is an $(n-1)$-truncated map. Thus we make the following definition:

######  Definition 23 ( ).

Let $n:\mathbb{N}^{\infty}$. For types $X,Y$ such that $Y$ is $(n+1)$-locally
$U$-small, and a function $\phi:X\rightarrow Y$ let
$\operatorname{T}^{n}_{U}\,\phi:\operatorname{T}^{n}_{U}\,X\rightarrow\operatorname{T}^{n}_{U}\,Y$
be the function

$\displaystyle\operatorname{T}^{n}_{U}\phi\
(A,f):=\left(\operatorname{image}_{n-1}\,(\phi\circ
f),\operatorname{incl}_{n-1}\,(\phi\circ f)\right)$

Note: For $n=\infty$ we get $\operatorname{T}^{\infty}_{U}\phi\
(A,f)\equiv(A,\phi\circ f)$.

Thinking of the elements in $\operatorname{T}^{n}_{U}\,X$ as slices over the
type $X$, equality should be fiberwise equivalence. This is indeed the case,
as the next proposition shows.

######  Proposition 18 ( ).

Given $n:\mathbb{N}^{\infty}$ and a type $X$, for
$(A,f),(B,g):\operatorname{T}^{n}_{U}\,X$ there is an equivalence

$\left((A,f)=(B,g)\right)\simeq\prod_{x:X}\operatorname{fiber}\,f\,x\simeq\operatorname{fiber}\,g\,x$

###### Proof.

For $(A,f),(B,g):\operatorname{T}^{\infty}_{U}\,X$ we have the following chain
of equivalences:

$\displaystyle\left((A,f)=(B,g)\right)$
$\displaystyle\simeq\sum_{\alpha:A=B}g\circ(\operatorname{coe}\,\alpha)=f$
(74) $\displaystyle\simeq\sum_{\alpha:A\simeq B}g\circ\alpha=f$ (75)
$\displaystyle\simeq\sum_{\alpha:\sum_{x:X}\operatorname{fiber}\,f\,x\;\simeq\;\sum_{x:X}\operatorname{fiber}\,g\,x}\pi_{0}\circ\alpha=\pi_{0}$
(76)
$\displaystyle\simeq\prod_{x:X}\operatorname{fiber}\,f\,x\simeq\operatorname{fiber}\,g\,x$
(77)

Step (74) is the usual characterisation of equality in $\phi$-types, step (75)
is the univalence axiom, step (76) is Lemma 4.8.2 in the HoTT Book [12, p.
186] and step (77) is Corollary 2. (Note: the equivalence
$\left(\sum_{\alpha:A\simeq
B}g\circ\alpha=f\right)\simeq\prod_{x:X}(\operatorname{fiber}\,f\,x\simeq\operatorname{fiber}\,g\,x)$
was proved as Lemma 5 in _Multisets in type theory_ [7], by explicitly
constructing an equivalence.)

For finite $n$, the type $\operatorname{T}^{n}_{U}\,X$ is a subtype of
$\operatorname{T}^{\infty}_{U}\,X$, and thus has the same identity types.∎

The characterisation of equality on $\operatorname{T}^{n}_{U}$ allows us to
compute the type level.

######  Corollary 3 ( ).

Given $n:\mathbb{N}^{\infty}$ and a type $X$, the type
$\operatorname{T}^{n}_{U}\,X$ is an $n$-type.

###### Proof.

For $(A,f),(B,g):\operatorname{T}^{n}_{U}\,X$ and $x:X$, the types
$\operatorname{fiber}\,f\,x$ and $\operatorname{fiber}\,g\,x$ are
$(n-1)$-truncated. Thus the identity type $(A,f)=(B,g)$ is $(n-1)$-truncated.∎

The functor $\operatorname{T}^{n}_{U}$ preserves homotopies.

######  Proposition 19 ( ).

Let $n:\mathbb{N}^{\infty}$. For types $X,Y$ such that $Y$ is $(n+1)$-locally
$U$-small, and functions $\phi,\psi:X\rightarrow Y$, any homotopy
$\epsilon:\phi\sim\psi$ induces a homotopy
$\operatorname{T}^{n}_{U}\,\epsilon:\operatorname{T}^{n}_{U}\phi\sim\operatorname{T}^{n}_{U}\psi$.
Moreover, $\operatorname{refl\mbox{-}htpy}$ is sent to
$\operatorname{refl\mbox{-}htpy}$.

###### Proof.

Given $\epsilon:\phi\sim\psi$ we construct the homotopy

$\displaystyle\operatorname{T}^{n}_{U}\epsilon:\operatorname{T}^{n}_{U}\phi\sim\operatorname{T}^{n}_{U}\psi$
$\displaystyle\operatorname{T}^{n}_{U}\epsilon\,(A,f):=\operatorname{ap}_{\lambda\,\sigma.\operatorname{T}^{n}_{U}\sigma\,(A,f)}(\operatorname{funext}\,\epsilon)$

For $\operatorname{T}^{n}_{U}\operatorname{refl\mbox{-}htpy}$ we have the
following chain of equalities:

$\displaystyle\operatorname{T}^{n}_{U}\operatorname{refl\mbox{-}htpy}\,(A,f)$
$\displaystyle\equiv\operatorname{ap}_{\lambda\,\sigma.\operatorname{T}^{n}_{U}\sigma\,(A,f)}(\operatorname{funext}\,\operatorname{refl\mbox{-}htpy})$
$\displaystyle=\operatorname{ap}_{\lambda\,\sigma.\operatorname{T}^{n}_{U}\sigma\,(A,f)}\operatorname{refl}$
$\displaystyle\equiv\operatorname{refl}$

∎

We recap the definition of an algebra for the functor
$\operatorname{T}^{n}_{U}$ and a homomorphism between two algebras.

######  Definition 24 ( ).

A $\operatorname{T}^{n}_{U}$-algebra, $(X,m)$ consists of an $(n+1)$-locally
$U$-small type $X$ and a map $m:\operatorname{T}^{n}_{U}X\rightarrow X$.

The restriction to $(n+1)$-locally $U$-small carrier types for
$\operatorname{T}^{n}_{U}$ algebras, is because $\operatorname{T}^{n}_{U}$ is
only functorial on such types.

######  Definition 25 ( ).

Given two $\operatorname{T}^{n}_{U}$ algebras, $(X,m)$ and
$(X^{\prime},m^{\prime})$, a $\operatorname{T}^{n}_{U}$-algebra homomorphism
from $(X,m)$ to $(X^{\prime},m^{\prime})$ is a pair $(\phi,\alpha)$ where
$\phi:X\rightarrow X^{\prime}$ and $\alpha:\phi\circ m\sim
m^{\prime}\circ\operatorname{T}^{n}_{U}\phi$.

For two $\operatorname{T}^{n}_{U}$-algebra homomorphisms $(\phi,\alpha)$ and
$(\psi,\beta)$ to be equal, there needs to be a homotopy between the
underlying maps $\phi$ and $\psi$. But there is also a coherence condition on
$\alpha$ and $\beta$, which can be seen as saying that the two natural ways of
proving that
$m^{\prime}\,(\operatorname{T}^{n}_{U}\,\phi)=_{X}^{\prime}\psi\,(m\,a)$ are
equal identifications in $X^{\prime}$. This holds trivially if $X^{\prime}$ is
a mere set, and in that case only the homotopy between the maps is relevant.

######  Lemma 8 ( ).

For any two $\operatorname{T}^{n}_{U}$-algebra homomorphisms $(\phi,\alpha)$
and $(\psi,\beta)$, from $(X,m)$ to $(X^{\prime},m^{\prime})$, their identity
type is characterised by:

$\displaystyle\left((\phi,\alpha)=(\psi,\beta)\right)\simeq\sum_{\epsilon:\phi\sim\psi}\prod_{a:\operatorname{T}^{n}_{U}X}\alpha\,a\cdot\operatorname{ap}_{m^{\prime}}(\operatorname{T}^{n}_{U}\,\epsilon\,a)=\epsilon\,(m\,a)\cdot\beta\,a$
(78)

###### Proof.

We use the structure identity principle. Given an algebra homomorphism
$(\phi,\alpha)$, we need to define families $P:(X\rightarrow
X^{\prime})\rightarrow\operatorname{Type}$ and $Q:\prod_{\psi:X\rightarrow
X^{\prime}}\left(\psi\circ m\sim
m^{\prime}\circ\operatorname{T}^{n}_{U}\psi\right)\rightarrow
P\,\psi\rightarrow\operatorname{Type}$, which should characterise the identity
type of the base type and of the fibration respectively. Then we need to
construct elements $p:P\,\phi$ and $q:Q\,\phi\,\alpha\,p$. Finally, we need to
show that for all $\psi:X\rightarrow X^{\prime}$,
$\left(\phi=\psi\right)\simeq P\,\psi$ and that for all
$\alpha^{\prime}:\phi\circ m\sim m^{\prime}\circ\operatorname{T}^{n}_{U}\phi$,
$\left(\alpha=\alpha^{\prime}\right)\simeq Q\,\phi\,\alpha^{\prime}\,p$.

The family $P$ is defined as $P\,\psi:=\left(\phi\sim\psi\right)$, and $Q$ is
defined as
$Q\,\psi\,\beta\,p^{\prime}:=\prod_{a:\operatorname{T}^{n}_{U}X}\alpha\,a\cdot\operatorname{ap}_{m^{\prime}}(\operatorname{T}^{n}_{U}\,p^{\prime}\,a)=p^{\prime}\,(m\,a)\cdot\beta\,a$.
For the element in $P\,\phi$ we take $p:=\operatorname{refl\mbox{-}htpy}$, and
for $Q\,\phi\,\alpha\,p$ and $(A,f):\operatorname{T}^{n}_{U}X$ we have the
following chain of equalities:

$\displaystyle\alpha\,(A,f)\cdot\operatorname{ap}_{m^{\prime}}(\operatorname{T}^{n}_{U}\,p\,(A,f))$
$\displaystyle=\alpha\,(A,f)\cdot\operatorname{ap}_{m^{\prime}}\operatorname{refl}$
(79) $\displaystyle=\alpha\,(A,f)$ (80)
$\displaystyle=p\,(m\,(A,f))\cdot\alpha\,(A,f)$ (81)

In step (79) we use Proposition 19.

It remains to construct the equivalences. By function extensionality,
$\left(\phi=\psi\right)\simeq\left(\phi\sim\psi\right)$. Moreover, for
$\alpha^{\prime}:\phi\circ m\sim m^{\prime}\circ\operatorname{T}^{n}_{U}\phi$
we have the following chain of equivalences:

$\displaystyle\left(\alpha=\alpha^{\prime}\right)$
$\displaystyle\simeq\left(\alpha\sim\alpha^{\prime}\right)$ (82)
$\displaystyle\simeq\prod_{a:\operatorname{T}^{n}_{U}X}\alpha\,a\cdot\operatorname{ap}_{m^{\prime}}\operatorname{refl}=\operatorname{refl}\cdot\alpha^{\prime}\,a$
(83)
$\displaystyle\simeq\prod_{a:\operatorname{T}^{n}_{U}X}\alpha\,a\cdot\operatorname{ap}_{m^{\prime}}(\operatorname{T}^{n}_{U}\,p\,a)=p\,(m\,a)\cdot\alpha^{\prime}\,a$
(84) $\displaystyle\equiv Q\,\phi\,\alpha^{\prime}\,p$ (85)

Step (82) is function extensionality, and in step (84) we again use
Proposition 19.∎

###  4.3 U-likeness

In classical set theory, the Mostowsky collapse relates any well-founded _set-
like_ relation to the well-founded hierarchy. A set-like relation is a class
relation, say $R$, where $\\{y\ |\ (x,y)\in R\\}$ is a set for all $x$. The
notion of “being small”, i.e. being a set, is also one of the basic
distinctions in algebraic set theory.

In type theory, types take the role of classes while the universe $U$ provides
a measure of smallness, akin to being a set in set theory. Hence, the notion
of a $U$-like $\in$-structure will mirror the classical notion of an
extensional, set-like relation.

######  Definition 26 ( ).

An $\in$-structure, $(V,\in)$ is $U$-like if $\operatorname{El}a$ is
essentially $U$-small for every $a:V$.

Remark: To simplify notation, we will coerce $\operatorname{El}a:U$ in
$U$-like $\in$-structures.

######  Proposition 20 ( ).

Being $U$-like is a mere proposition for any $\in$-structure, $(V,\in)$.

The interaction between internalisable types and $U$-likeness is
straightforward:

######  Proposition 21 ( ).

An $\in$-structure, $(V,\in)$, is $U$-like if any only if for each
internalisable $A:\operatorname{Type}$, the type $A$ is essentially $U$-small.

###### Proof.

We have the following chain of equivalences:

$\displaystyle\prod_{A:\operatorname{Type}}$
$\displaystyle\left(\sum_{a:V}\operatorname{El}a\simeq
A\right)\rightarrow\sum_{X:U}A\simeq X$
$\displaystyle\simeq\prod_{a:V}\left(\sum_{A:\operatorname{Type}}\operatorname{El}a\simeq
A\right)\rightarrow\sum_{X:U}\operatorname{El}a\simeq X$ (86)
$\displaystyle\simeq\prod_{a:V}\left(\sum_{X:U}\operatorname{El}a\simeq
X\right)$ (87)

In step (87) we use the fact that the type
$\sum_{A:\operatorname{Type}}\operatorname{El}a\simeq A$ is contractible.∎

We will now investigate in detail the relationship between $U$-like
$\in$-structures and $\operatorname{T}^{n}_{U}$-coalgebras.

######  Lemma 9 ($\in$-structures are coalgebras  ).

For a fixed $V$, having a $U$-like $\in$-structure on $V$ is equivalent to
having a coalgebra structure
$V\hookrightarrow\operatorname{T}^{\infty}_{U}\,V$, which is an embedding.
This equivalence sends the relation $\in:V\rightarrow
V\rightarrow\operatorname{Type}$ to the coalgebra
$\lambda\,a.(\operatorname{El}\,a,\pi_{0})$ and, in the other direction, it
sends the coalgebra $m:V\rightarrow\operatorname{T}^{\infty}_{U}\,V$ to the
relation $\lambda\,b\,a.\operatorname{fiber}\ (\pi_{1}\,(m\,a))\ b$.

###### Proof.

We have the following chain of equivalences:

$\displaystyle V\rightarrow\sum_{A:U}(A\rightarrow V)$
$\displaystyle\simeq\left(V\rightarrow\sum_{F:V\rightarrow\operatorname{Type}}\sum_{E:U}\left(\left(\sum_{b:V}F\,b\right)\simeq
E\right)\right)$ (88) $\displaystyle\simeq\sum_{\in:V\rightarrow
V\rightarrow\operatorname{Type}}\prod_{a:V}\sum_{E:U}\left(\left(\sum_{b:V}b\in
a\right)\simeq E\right)$ (89)

The equivalence (88) follows by substituting $\sum_{A:U}(A\rightarrow V)$ with
the equivalent type
$\sum_{F:V\rightarrow\operatorname{Type}}\sum_{E:U}(\sum_{b:V}F\,b)\simeq E$,
since a fibration $A\rightarrow V$, with a total type $A:U$ is equivalent to a
family over $V$ with $U$-small total type, as being $U$-small is a mere
proposition. The equivalence (89) is essentially currying.

Chasing a coalgebra, respectively an $\in$-relation, along the chain of
equivalences we see that it computes as stated.

The type $\sum_{\in:V\rightarrow
V\rightarrow\operatorname{Type}}\prod_{a:V}\sum_{E:U}\left(\left(\sum_{b:V}b\in
a\right)\simeq E\right)$ is exactly the type of $\in$-structures on $V$ which
are $U$-like, except for the extensionality requirement. It remains to show
that the coalgebra is an embedding if and only if the corresponding
$\in$-relation, given by the equivalence above, is extensional.

Given a coalgebra $m:V\rightarrow\operatorname{T}^{\infty}_{U}\,V$, let $\in$
be the corresponding relation given by the equivalence. By Proposition 18 we
have, for any $x,y:V$, an equivalence

$\displaystyle e:\left(m\,x=m\,y\right)\simeq\left(\prod_{z:V}z\in x\simeq
z\in y\right)$

This equivalence sends $\operatorname{refl}$ to
$\lambda\,z.\operatorname{id\mbox{-}equiv}$. Let
$e^{\prime}:x=y\rightarrow\prod_{z:V}z\in x\simeq z\in y$ be the map defined
by path induction as
$e^{\prime}\,\operatorname{refl}:=\lambda\,z.\operatorname{id\mbox{-}equiv}$.
The following diagram commutes:

${x=y}$${m\,x=m\,y}$${\prod_{z:V}z\in x\simeq z\in
y}$$\scriptstyle{\operatorname{ap}_{m}}$$\scriptstyle{e^{\prime}}$$\scriptstyle{e}$

Since $e$ is an equivalence it follows that $\operatorname{ap}_{m}$ is an
equivalence if and only if $e^{\prime}$ is an equivalence.∎

######  Lemma 10.

Given a $U$-like $\in$-structure, $(V,\in)$, and any $n:\mathbb{N}_{-1}$, the
following are equivalent:

  1. 1.

$b\in a$ is an $n$-type for all $a,b:V$,

  2. 2.

$\lambda\,a.(\operatorname{El}\,a,\pi_{0})$ restricts to a map
$V\hookrightarrow\operatorname{T}^{n+1}_{U}\,V$.

###### Proof.

The fibres of $\pi_{0}:(\sum_{b:V}b\in a)\rightarrow V$ are exactly the types
$b\in a$.∎

The following theorem combines the two previous lemmas in order to
characterise $U$-like $\in$-structures of various levels in terms of
coalgebras.

######  Theorem 3 ( ).

For a fixed $V$ and for $n:\mathbb{N}^{\infty}_{-1}$, having a $U$-like
$\in$-structure on $V$ such that $b\in a$ is an $n$-type for all $a,b:V$ is
equivalent to having a coalgebra structure
$V\hookrightarrow\operatorname{T}^{n+1}_{U}\,V$.

###### Proof.

Simple corollary of the previous two lemmas.∎

##  5 Fixed-point models

Rieger’s theorem is a result in set theory which states that any class with a
set-like binary relation, which is a fixed-point of the related powerset
functor, is a model of ZFC- [9]. In this section we prove an analogous result,
considering the family of functors $\operatorname{T}^{n}_{U}$ as higher level
generalisations of the powerset functor. Any fixed-point for
$\operatorname{T}^{n}_{U}$ is in particular a
$\operatorname{T}^{n}_{U}$-coalgebra for which the coalgebra map is an
embedding. Thus, by Theorem 3, such a fixed-point gives rise to a $U$-like
$\in$-structure. This induced $\in$-structure will satisfy almost all the
properties defined in Section § ‣ 2, at some level, the only exception being
Foundation.

So we assume in this section that we are given a type $V$ and an equivalence
$\sup:\operatorname{T}^{n}_{U}V\simeq V$. Let
$\operatorname{desup}:V\simeq\operatorname{T}^{n}_{U}V$ be the inverse of
$\sup$. We will specifically show that the induced $\in$-structure on $V$ has
the following properties:

  * •

Empty set.

  * •

$U$-restricted $n$-separation.

  * •

If $V$ is $(n+1)$-locally $U$-small, it has $\infty$-unordered $I$-tupling for
all $(n-1)$-truncated types $I:U$.

  * •

If $V$ is $(k+1)$-locally $U$-small, for some $k\leq n$ then it has:

    * –

$k$-unordered $I$-tupling for all $I:U$,

    * –

$k$-replacement,

    * –

$k$-union.

  * •

$V$ has exponentiation for all ordered pairing structures.

  * •

$V$ has natural numbers represented by $f$ for any $(n-1)$-truncated
representation $f:\mathbb{N}\rightarrow V$.

Notation: Given $x:V$, we will use the notation $\overline{x}:U$ and
$\widetilde{x}:\overline{x}\hookrightarrow V$ for the type and propositionally
truncated map such that $x=\sup\,(\overline{x},\widetilde{x})$, i.e.
$\overline{x}=\pi_{0}\,(\operatorname{desup}\,x)$ and
$\widetilde{x}=\pi_{1}\,(\operatorname{desup}\,x)$.

######  Definition 27 ( ).

Let $(V,\in)$ be the $\in$-structure on $V$ given by Theorem 3. Note that for
$x,y:V$,

$\displaystyle y\in x\equiv\operatorname{fiber}\,\widetilde{x}\,y$

######  Proposition 22.

For any $x:V$ we have that $\overline{x}\simeq\operatorname{El}\,x$.

###### Proof.

We have the following:

$\displaystyle\operatorname{El}\,x\equiv\left(\sum_{y:V}\operatorname{fiber}\,\widetilde{x}\,y\right)\simeq\overline{x}$
(90)

where the equivalence in the last step is Lemma 4.8.2 in the HoTT book [12, p.
142].∎

######  Proposition 23 ( ).

The type $V$ is an $n$-type.

###### Proof.

$V\simeq\operatorname{T}^{n}_{U}V$ and $\operatorname{T}^{n}_{U}\,V$ is an
$n$-type by Corollary 3.∎

Many of the constructions of the properties defined in Section § ‣ 2 require
us to use $\sup$ on the $k$-image of some function, and its $k$-truncated
inclusion map. For this, the $k$-image needs to be $U$-small. We therefore
need to assume that $V$ is appropriately locally $U$-small in several of the
following theorems.

###  5.1 Empty set

The empty set is a special case of unordered tupling but it does not require
any assumption about local smallness. Therefore we note this special case
separately.

######  Theorem 4 ( ).

The $\in$-structure $(V,\in)$ has empty set.

###### Proof.

The empty type $\mathbf{0}$ embeds into any type, in particular, it embeds
into $V$. Let $f:\mathbf{0}\rightarrow V$ be the unique map from $\mathbf{0}$
to $V$. Since the map is an embedding, it is also an $(n-1)$-truncated map.
The empty set is defined as

$\displaystyle\emptyset:=\sup\,(\mathbf{0},f)$

For $x:V$ we have the following chain of equivalences:

$\displaystyle x\in\emptyset$ $\displaystyle\simeq\operatorname{fiber}\,f\,x$
$\displaystyle\simeq\sum_{s:\mathbf{0}}f\,s=x$ $\displaystyle\simeq\mathbf{0}$

∎

###  5.2 Restricted separation

######  Theorem 5 ( ).

The $\in$-structure $(V,\in)$ has $U$-restricted $n$-separation.

###### Proof.

For $x:V$ and $\Phi:V\rightarrow(n-1)\operatorname{\mbox{-}Type}_{U}$ we
construct the term $\\{y\in x\mid\Phi\,y\\}$ as follows:

$\\{y\in
x\mid\Phi\,y\\}:=\sup\,\left(\sum_{a:\overline{x}}\Phi\,(\widetilde{x}\,a),\lambda(a,\\_).\widetilde{x}\,a\right).$

The map $\lambda(a,\\_).\widetilde{x}\,a$ is $(n-1)$ truncated as it is the
composition of the $(n-1)$-truncated map $\widetilde{x}$ and the projection
$\pi_{0}:\sum_{a:\overline{x}}\Phi\,(\widetilde{x}\,a)\rightarrow\overline{x}$,
which is $(n-1)$-truncated since $\Phi$ is a family of $(n-1)$-truncated
types.

For $z:V$ we then get the following chain of equivalences:

$\displaystyle z\in\\{y\in x\mid\Phi\,y\\}$
$\displaystyle=\sum_{(a,\\_):\sum_{a:\overline{x}}\Phi\,(\widetilde{x}\,a)}\widetilde{x}\,a=z$
$\displaystyle\simeq\sum_{(a,\\_):\sum_{a:\overline{x}}\widetilde{x}\,a=z}\Phi\,(\widetilde{x}\,a)$
$\displaystyle\simeq(z\in x)\times\Phi\,z.$

∎

###  5.3 Unordered tupling

For unordered tupling we can construct the $k$-truncated version if $V$ is
$(k+1)$-locally $U$-small, and we can construct the $\infty$-truncated version
if the indexing type has lower type level than $V$.

######  Theorem 6 ( ).

Let $k:\mathbb{N}^{\infty}$ be such that $k\leq n$. If $V$ is $(k+1)$-locally
$U$-small then the $\in$-structure $(V,\in)$ has k-unordered I-tupling for all
$I:U$.

###### Proof.

Let $I:U$ and $v:I\rightarrow V$, and construct the element $\\{v\\}_{k}:V$ by

$\\{v\\}_{k}:=\sup\,(\operatorname{image}_{k-1}\,v,\operatorname{incl}_{k-1}\,v)$

Since $k\leq n$, $\operatorname{incl}_{k-1}\,v$ is an $(n-1)$-truncated map.
Then, for any $z:V$, we have the following chain of equivalences:

$\displaystyle z\in\\{v\\}_{k}$
$\displaystyle=\operatorname{fiber}\,(\operatorname{incl}_{k-1}\,v)\ z$
$\displaystyle\simeq\big{\|}\operatorname{fiber}\,v\ z\,\big{\|}_{k-1}$
$\displaystyle\equiv\big{\|}\sum_{i:I}v\,i=z\,\big{\|}_{k-1}$

∎

######  Corollary 4 ( ).

Let $k:\mathbb{N}^{\infty}$ be such that $k\leq n$. If $V$ is $(k+1)$-locally
$U$-small then $V$ contains the $k$-unordered $1$-tupling $\\{x\\}_{k}$, and
the $k$-unordered $2$-tupling $\\{x,y\\}_{k}$, for any $x,y:V$.

######  Theorem 7 ( ).

If $V$ is $(n+1)$-locally $U$-small then it has an ordered pairing structure.

###### Proof.

Follows from the previous corollary together with Theorem 4, Theorem 1 and
Proposition 23.∎

######  Theorem 8 ( ).

Let $k:\mathbb{N}$ be such that $k<n$. If $V$ is $(n+1)$-locally $U$-small,
then the $\in$-structure $(V,\in)$ has $\infty$-unordered I-tupling for all
$I:k\operatorname{\mbox{-}Type}_{U}$.

###### Proof.

Let $I:U$ and $v:I\rightarrow V$. We construct the element
$\\{v\\}_{\infty}:V$ as in Theorem 6:

$\\{v\\}_{\infty}:=\sup\,(\operatorname{image}_{n-1}\,v,\operatorname{incl}_{n-1}\,v)$

Then, for any $z:V$, we have the following chain of equivalences:

$\displaystyle z\in\\{v\\}_{\infty}$
$\displaystyle=\operatorname{fiber}\,(\operatorname{incl}_{k-1}\,v)\ z$ (91)
$\displaystyle\simeq\big{\|}\operatorname{fiber}\,v\ z\,\big{\|}_{n-1}$ (92)
$\displaystyle\equiv\big{\|}\sum_{i:I}v\,i=z\,\big{\|}_{n-1}$ (93)
$\displaystyle\simeq\sum_{i:I}v\,i=z$ (94)

where step (94) is the fact that $\sum_{i:I}v\,i=z$ is $(n-1)$-truncated since
$V$ is an $n$-type and $I$ is a $k$-type for some $k<n$.∎

###  5.4 Replacement

######  Theorem 9 ( ).

Let $k:\mathbb{N}^{\infty}$ be such that $k\leq n$. If $V$ is $(k+1)$-locally
$U$-small, then the $\in$-structure $(V,\in)$ has $k$-replacement.

###### Proof.

For $x:V$ and $f:\operatorname{El}\,x\rightarrow V$, let
$\phi:\overline{x}\rightarrow V$ be the function that sends $a:\overline{x}$
to $f\,(a,\operatorname{refl})$. We define the following element:

$\\{f(y)\mid y\in
x\\}:=\sup\,(\operatorname{image}_{k-1}\,\phi,\operatorname{incl}_{k-1}\,\phi)$

Since $k\leq n$, $\operatorname{incl}_{k-1}\,\phi$ is an $(n-1)$-truncated
map. For $z:V$ we have the following chain of equivalences:

$\displaystyle z\in\\{f(y)\mid y\in x\\}$
$\displaystyle=\operatorname{fiber}\,(\operatorname{incl}_{k-1}\,\phi)\,z$
(95) $\displaystyle\simeq\;\big{\|}\operatorname{fiber}\,\phi\
z\big{\|}_{k-1}$ (96)
$\displaystyle\simeq\;\big{\|}\sum_{s:\operatorname{El}\,x}f\,s=z\big{\|}_{k-1}$
(97)

where (97) uses Proposition 22.∎

###  5.5 Union

######  Theorem 10 ( ).

Let $k:\mathbb{N}^{\infty}$ be such that $k\leq n$. If $V$ is $(k+1)$-locally
$U$-small, then the $\in$-structure $(V,\in)$ has $k$-union.

###### Proof.

For $x:V$, let
$\phi_{x}:\sum_{a:\overline{x}}\overline{(\widetilde{x}\,a)}\rightarrow V$ be
the function that sends $(a,b)$ to $\widetilde{(\widetilde{x}\,a)}\,b$. We
then define the union by

$\bigcup_{k}x:=\sup\,(\operatorname{image}_{k-1}\,(\phi_{x}),\operatorname{incl}_{k-1}\,(\phi_{x}))$

Since $k\leq n$, $\operatorname{incl}_{k-1}\,(\phi_{x})$ is an
$(n-1)$-truncated map. For $z:V$ we thus have the following chain of
equivalences:

$\displaystyle z\in\bigcup_{k}x$
$\displaystyle=\operatorname{fiber}\,(\operatorname{incl}_{k-1}\,(\phi_{x}))\,z$
(98)
$\displaystyle\simeq\;\big{\|}\operatorname{fiber}\,\phi_{x}\,z\big{\|}_{k-1}$
(99)
$\displaystyle\simeq\;\big{\|}\sum_{a:\overline{x}}\;z\in\widetilde{x}\,a\big{\|}_{k-1}$
(100) $\displaystyle\simeq\;\big{\|}\sum_{y:V}\;z\in y\times y\in
x\big{\|}_{k-1},$ (101)

where (101) uses Proposition 22.∎

###  5.6 Exponentiation

The property of having exponentiation is relative to an ordered pairing
structure. It turns out that the construction of ordered pairs does not
matter. $(V,\in)$ has exponentiation for any ordered pairing structure. In
order to prove this though, we first need some lemmas.

######  Lemma 11 ( ).

Let $A$ be a type and $B$ a type family over $A$. For any two functions
$\phi,\psi:\prod_{a:A}B\,a$ there is an equivalence

$\displaystyle\left(\phi=\psi\right)\simeq\sum_{e:A\simeq
A}\prod_{a:A}(a,\phi\,a)=(e\,a,\psi\,(e\,a))$

Moreover, this equivalence sends $\operatorname{refl}$ to
$(\operatorname{id\mbox{-}equiv},\operatorname{refl\mbox{-}htpy})$.

###### Proof.

For $\phi,\psi:\prod_{a:A}B\,a$ we have the following chain of equivalences:

$\displaystyle\left(\phi=\psi\right)$
$\displaystyle\simeq\left(\phi\sim\psi\right)$ (102)
$\displaystyle\simeq\sum_{e:A\simeq A}\sum_{r:\operatorname{id}_{A}\sim
e}\prod_{a:A}\operatorname{tr}^{B}_{r\,a}(\phi\,a)=\psi\,(e\,a)$ (103)
$\displaystyle\simeq\sum_{e:A\simeq
A}\prod_{a:A}\sum_{p:a=e\,a}\operatorname{tr}^{B}_{p}(\phi\,a)=\psi\,(e\,a)$
(104) $\displaystyle\simeq\sum_{e:A\simeq
A}\prod_{a:A}(a,\phi\,a)=(e\,a,\psi\,(e\,a))$ (105)

Step (102) is function extensionality. In step (103) we use the fact that the
type $\sum_{e:A\simeq A}\operatorname{id}_{A}\sim e$ is contractible, with
$(\operatorname{id\mbox{-}equiv},\operatorname{refl\mbox{-}htpy})$ as the
center of contraction. Finally, step (105) is the characterisation of equality
in $\Sigma$-types.

Chasing $\operatorname{refl}$ along the chain of equivalences, we get:

$\displaystyle\operatorname{refl}$
$\displaystyle\mapsto\operatorname{refl\mbox{-}htpy}$
$\displaystyle\mapsto(\operatorname{id\mbox{-}equiv},\operatorname{refl\mbox{-}htpy},\operatorname{refl\mbox{-}htpy})$
$\displaystyle\mapsto(\operatorname{id\mbox{-}equiv},\lambda\,a.(\operatorname{refl},\operatorname{refl}))$
$\displaystyle\mapsto(\operatorname{id\mbox{-}equiv},\operatorname{refl\mbox{-}htpy})$

∎

######  Lemma 12 ( ).

Let $\langle-,-\rangle:V\rightarrow V\rightarrow V$ be an ordered pairing
structure on $V$. Given a small type $A:U$ and a type family
$B:A\rightarrow\operatorname{Type}$ together with $(n-1)$-truncated maps
$f:A\hookrightarrow_{n-1}V$ and $g:\prod_{a:A}B\,a\hookrightarrow_{n-1}V$,
there is an $(n-1)$-truncated map

$\displaystyle\operatorname{graph}_{f,g}:\left(\prod_{a:A}B\,a\right)\hookrightarrow_{n-1}V$

###### Proof.

Given $\phi:\prod_{a:A}B\,a$, we first need to construct an element in $V$. To
this end, we construct the $(n-1)$-truncated map

$\displaystyle F_{\phi}:A\hookrightarrow_{n-1}V$ $\displaystyle
F_{\phi}\,a=\langle f\,a,g\,a\,(\phi\,a)\rangle$

This map is $(n-1)$-truncated as it is the composition of the maps
$\langle-,-\rangle$, $\lambda\,(a,b).(f\,a,g\,a\,b)$ and
$\lambda\,a.(a,\phi\,a)$. The first is $(-1)$-truncated by assumption, and
thus $(n-1)$-truncated. The second is $(n-1)$-truncated since $f$ is
$(n-1)$-truncated and $g\,a$ is $(n-1)$-truncated for all $a:A$. To see that
the last map is $(n-1)$-truncated, for any pair $(a,b):\sum_{a:A}B\,a$ we have
the following chain of equivalences:

$\displaystyle\left(\sum_{a^{\prime}:A}(a^{\prime},\phi\,a^{\prime})=(a,b)\right)\simeq\left(\sum_{a^{\prime}:A}\sum_{p:a^{\prime}=a}\operatorname{tr}^{B}_{p}(\phi\,a^{\prime})=b\right)\simeq\left(\phi\,a=b\right)$

where we have used the fact that the type $\sum_{a^{\prime}:A}a^{\prime}=a$ is
contractible, with $(a,\operatorname{refl})$ as the center of contraction.
Since $V$ is $n$-truncated, it follows that
$\sum_{a^{\prime}:A}(a^{\prime},\phi\,a^{\prime})=(a,b)$ is $(n-1)$-truncated,
and thus $\lambda\,a.(a,\phi\,a)$ is an $(n-1)$-truncated map.

This gives us the underlying map

$\displaystyle\operatorname{graph}_{f,g}:\left(\prod_{a:A}B\,a\right)\rightarrow
V$ $\displaystyle\operatorname{graph}_{f,g}\,\phi:=\sup\,(A,F_{\phi})$

What is left is to show that this map is $(n-1)$-truncated. For this we show
that
$\operatorname{ap}_{\operatorname{graph}_{f,g}}:\phi=\psi\rightarrow\operatorname{graph}_{f,g}\,\phi=\operatorname{graph}_{f,g}\,\psi$
is $(n-2)$-truncated for all $\phi,\psi:\prod_{a:A}B\,a$.

Let $\phi,\psi:\prod_{a:A}B\,a$, let
$\alpha:\left(\phi=\psi\right)\simeq\sum_{e:A\simeq
A}\prod_{a:A}(a,\phi\,a)=(e\,a,\psi\,(e\,a))$ be the equivalence given by
Lemma 11 and let $\beta:\left(\sum_{e:A\simeq A}F_{\phi}\sim F_{\psi}\circ
e\right)\simeq\left((A,F_{\phi})=(A,F_{\psi})\right)$ be the equivalence given
by the usual characterisation of identity in $\Sigma$-types together with
univalence and function extensionality. We start by observing that

$\displaystyle\operatorname{ap}_{\operatorname{graph}_{f,g}}\sim\operatorname{ap}_{\sup}\circ\
\beta\ \circ\ (\lambda\,(e,H).(e,\operatorname{ap}_{\lambda\,(a,b).\langle
f\,a,g\,a\,b\rangle}\circ H))\circ\alpha$

All three of $\alpha$, $\beta$ and $\operatorname{ap}_{\sup}$ are
equivalences, and hence $(n-2)$-truncated maps. For the last map, it is enough
to show that for all $e:A\simeq A$ and all $a:A$

$\displaystyle\operatorname{ap}_{\lambda\,(a,b).\langle
f\,a,g\,a\,b\rangle}:(a,\phi\,a)=(e\,a,\psi\,(e\,a))\rightarrow
F_{\phi}\,a=F_{\psi}\,(e\,a)$

is $(n-2)$-truncated. But this follows from the fact that the map
$\lambda\,(a,b).\langle f\,a,g\,a\,b\rangle$ is $(n-1)$-truncated, as it is
the composition of two $(n-1)$-truncated maps.∎

######  Theorem 11 (Exponentiation  ).

The $\in$-structure $(V,\in)$ has exponentiation, for any ordered pairing
structure.

###### Proof.

Let $\langle-,-\rangle:V\rightarrow V\rightarrow V$ be an ordered pairing
structure on $V$. Given $x,y:V$, we define the element

$\displaystyle y^{x}:V$ $\displaystyle
y^{x}:=\sup\,(\overline{x}\rightarrow\overline{y},\operatorname{graph}_{\widetilde{x},\lambda\,\\_.\widetilde{y}})$

For $f:V$ we then have the following chain of equivalences:

$\displaystyle f\in y^{x}$
$\displaystyle\simeq\sum_{\phi:\overline{x}\rightarrow\overline{y}}f=\operatorname{graph}_{\widetilde{x},\lambda\,\\_.\widetilde{y}}\,\phi$
(106)
$\displaystyle\simeq\sum_{\phi:\overline{x}\rightarrow\overline{y}}\prod_{z:V}z\in
f\simeq
z\in\operatorname{graph}_{\widetilde{x},\lambda\,\\_.\widetilde{y}}\,\phi$
(107)
$\displaystyle\simeq\sum_{\phi:\overline{x}\rightarrow\overline{y}}\prod_{z:V}z\in
f\simeq\sum_{a:\overline{x}}\langle\widetilde{x}\,a,\widetilde{y}\,(\phi\,a)\rangle=z$
(108)
$\displaystyle\simeq\sum_{\phi:\operatorname{El}\,x\rightarrow\operatorname{El}\,y}\prod_{z:V}z\in
f\simeq\sum_{a:\operatorname{El}\,x}\langle\pi_{0}\,a,\pi_{0}\,(\phi\,a)\rangle=z$
(109) $\displaystyle\simeq\operatorname{operation}\,x\,y\,f$ (110)

In step (107) we use extensionality and in step (109) we use Proposition 22.
Finally, in step (110) we use Proposition 6.∎

###  5.7 Natural numbers

######  Theorem 12 ( ).

The $\in$-structure $(V,\in)$ has natural numbers represented by $f$, for any
$(n-1)$-truncated representation $f$.

###### Proof.

Let $f:\mathbb{N}\rightarrow V$ be an $(n-1)$-truncated representation of
$\mathbb{N}$. We construct the following element:

$n:=\sup\,(\mathbb{N},f)$

Then for any $z:V$ we have

$z\in
n\equiv\operatorname{fiber}\,\widetilde{n}\,z=\operatorname{fiber}\,f\,z$

∎

##  6 The initial $\operatorname{T}^{n}_{U}$-algebra

The most straightforward way to construct a fixed-point of a functor is by
constructing its initial algebra. For polynomial functors, the initial
algebras are well understood. They are called W-types and are used to create a
variety of inductive data structures, such as models of set theory in type
theory: The initial algebra for $\operatorname{T}^{\infty}_{U}$ formed the
basis for Aczel’s setoid model of CZF in Martin-Löf type theory [2]. The
initial algebras for $\operatorname{T}^{n}_{U}$, for finite $n$, are subtypes
of this type.

The functor $\operatorname{T}^{n}_{U}$ is not a polynomial functor, for finite
$n$. So, its initial algebra will not be a simple W-type. Looking carefully at
the type $\sum_{A:U}A\hookrightarrow_{n-1}X$ one can see that it is not
strictly positive, since the type
$A\hookrightarrow_{n-1}X:=\sum_{f:A\rightarrow
X}\prod_{x:X}\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}type\,}(\operatorname{fiber}\,f\,x)$
contains a negative occurrence of $X$. Being strictly positive is a usual
requirement for inductive definitions, so it is a bit surprising that
$\operatorname{T}^{n}_{U}$ still has an initial algebra.

In this section, we will construct the initial algebra for
$\operatorname{T}^{n}_{U}$, which then becomes a fixed-point $\in$-structure
of level $n$. One interesting aspect of doing this proof in HoTT is that the
carrier for a $\operatorname{T}^{n}_{U}$-algebra can lie on any type level.

We start by recalling Aczel’s W-type.

######  Definition 28 ( ).

Let $V^{\infty}:=W_{A:U}A$, and denote its (uncurried) constructor
$\sup^{\infty}:\operatorname{T}^{\infty}_{U}V^{\infty}\rightarrow V^{\infty}$.

Remark: The superscript of the name, $V^{\infty}$, indicates that there is no
bound on the level of the type. In fact, $V^{\infty}$ has the same type level
as $U$.

The pair $(V^{\infty},\sup^{\infty})$ is the initial algebra for the functor
$\operatorname{T}^{\infty}_{U}:\operatorname{Type}\rightarrow\operatorname{Type}$,
and hence a fixed-point of $\operatorname{T}^{\infty}_{U}$. Any fixed-point
has a canonical coalgebra structure, and by Lemma 9 this gives rise to a
$U$-like $\in$-structure. Thus, we will denote by
$\in^{\infty}:V^{\infty}\rightarrow V^{\infty}\rightarrow\operatorname{Type}$,
this elementhood relation on $V^{\infty}$. Note: by construction,
$x\in^{\infty}\sup^{\infty}\,(A,f)\equiv\operatorname{fiber}\,f\,x$.

This is the $\in$-structure explored in _Multisets in type theory_ [7], which
also introduced some of the axioms of the previous sections. In _From
multisets to sets in Homotopy Type Theory_ [6] a 0-level $\in$-structure was
carved out as a subtype of $V^{\infty}$. And we will now prove that this
0-level structure is, as previously suspected, the initial
$\operatorname{T}^{0}_{U}$ algebra. In fact, we will generalise the
construction to form a type $V^{n}$ for all $n:\mathbb{N}$ and show that
$V^{n}$ is the initial algebra for $\operatorname{T}^{n}_{U}$.

###  6.1 Iterative $n$-types

The types $V^{n}$ form a stratified hierarchy of $\in$-structures, where
$V^{\infty}$ is at the top. This is analogous to how the $n$-types in $U$ form
a hierarchy with $U$ itself at the top.

######  Definition 29 ( ).

Given $n:\mathbb{N}_{-1}$, define by induction on $V^{\infty}$, a predicate
$\operatorname{is\mbox{-}}n\operatorname{\mbox{-}ittype}:V^{\infty}\rightarrow\operatorname{Type}$
by:

$\operatorname{is\mbox{-}}n\operatorname{\mbox{-}ittype}\left(\sup^{\infty}\,(A,f)\right):=\left(\operatorname{is\mbox{-}}n\operatorname{\mbox{-}trunc\mbox{-}map\,}f\right)\times\left(\prod_{a:A}\operatorname{is\mbox{-}}n\operatorname{\mbox{-}ittype}(f\,a)\right)$

This predicate is propositional, and an element of $V^{\infty}$ for which the
predicate is true is called _an iterative $n$-type_.

Remark: We could define iterative $(-2)$-types analogously, but there are no
elements in $V^{\infty}$ which satisfy this predicate, as the existence of
such an element would imply that $V^{\infty}$ is essentially $U$-small.

######  Definition 30 ( ).

For $n:\mathbb{N}_{-1}$, let
$V^{n+1}:=\sum_{x:V^{\infty}}\operatorname{is\mbox{-}}n\operatorname{\mbox{-}ittype}x$
denote the type of iterative $n$-types, which is a subtype of $V^{\infty}$.

Even though the type $V^{n}$ is not itself $U$-small, it has $U$-small
identity types

######  Proposition 24 ( ).

The type $V^{n}$ is locally $U$-small.

###### Proof.

First, we observe that, since being an iterative $(n-1)$-type is a
proposition, $V^{n}$ is a subtype of $V^{\infty}$. It was shown in _Multisets
in type theory_ [7, Lemma 3] that the latter is locally $U$-small. Since the
equality of a subtype is the underlying equality of the base type, it follows
that $V^{n}$ is locally $U$-small.∎

In the following proofs we will leave out elements of types which are
propositions, unless they are necessary, in order to increase readability. For
the full details of the proofs, please see the Agda formalisation.

######  Proposition 25 ( ).

The map $\sup^{\infty}:\operatorname{T}^{\infty}_{U}V^{\infty}\rightarrow
V^{\infty}$ restricts to a map
$\sup^{n}:\operatorname{T}^{n}_{U}V^{n}\rightarrow V^{n}$.

###### Proof.

Let $A:U$ and $f:A\hookrightarrow_{n-1}V^{n}$. The element
$\sup^{\infty}\,(A,\pi_{0}\circ f)$ is an iterative $(n-1)$-type:

  * •

$\pi_{0}\circ f$ is $(n-1)$-truncated since $f$ is $(n-1)$-truncated, and
$\pi_{0}$ is the inclusion of a subtype, which is an embedding, and thus
$(n-1)$-truncated.

  * •

For every $a:A$ we have
$\pi_{1}\,(f\,a):\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}ittype}(\pi_{0}\,(f\,a))$.

Thus we construct the map

$\displaystyle\operatorname{sup}^{n}:\operatorname{T}^{n}_{U}V^{n}\rightarrow
V^{n}$
$\displaystyle\operatorname{sup}^{n}\,(A,f):=\left(\operatorname{sup}^{\infty}\,(A,\pi_{0}\circ
f),\rule{6.0pt}{0.4pt}\right)$

∎

######  Proposition 26 ( ).

There is a map
$\operatorname{desup}^{n}:V^{n}\rightarrow\operatorname{T}^{n}_{U}V^{n}$.

###### Proof.

Let $x:V^{n}$, without loss of generality we may assume that
$x\equiv(\operatorname{sup}^{\infty}\,(A,f),(p,q))$ for some $A:U$,
$f:A\rightarrow V^{\infty}$,
$p:\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}trunc\mbox{-}map\,}f$
and
$q:\prod_{a:A}\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}ittype}(f\,a)$.
The following function:

$\displaystyle\lambda\,a.(f\,a,q\,a):A\rightarrow V^{n}$

is $(n-1)$-truncated. This is because the composition
$\pi_{0}\circ(\lambda\,a.(f\,a,q\,a))$ is $(n-1)$-truncated, by $p$, and
$\pi_{0}$ is $(n-1)$-truncated as it is the inclusion of a subtype. This
implies that the right factor, $\lambda\,a.(f\,a,q\,a)$, is $(n-1)$-truncated.
Thus we construct the map

$\displaystyle\operatorname{desup}^{n}:V^{n}\rightarrow\operatorname{T}^{n}_{U}V^{n}$
$\displaystyle\operatorname{desup}^{n}\,(\operatorname{sup}^{\infty}\,(A,f),(p,q)):=(A,\lambda\,a.(f\,a,q\,a))$

∎

######  Proposition 27 ( ).

The maps $\sup^{n}$ and $\operatorname{desup}^{n}$ form an equivalence.

###### Proof.

For $(\operatorname{sup}^{\infty}\,(A,f),(p,q)):V^{n}$ we have

$\displaystyle\pi_{0}\,(\operatorname{sup}^{n}\,$
$\displaystyle(\operatorname{desup}^{n}\,(\operatorname{sup}^{\infty}\,(A,f),(p,q))))$
$\displaystyle\equiv\pi_{0}\,(\operatorname{sup}^{n}\,(A,\lambda\,a.(f\,a,q\,a)))$
$\displaystyle\equiv(\operatorname{sup}^{\infty}\,(A,f))$
$\displaystyle\equiv\pi_{0}\,(\operatorname{sup}^{\infty}\,(A,f),(p,q))$

Thus, by the characterisation of equality in subtypes,
$\sup^{n}\circ\operatorname{desup}^{n}\sim\operatorname{id}$.

For $A:U$ and $f:A\hookrightarrow_{n-1}V^{n}$ we have

$\displaystyle\pi_{0}\,(\operatorname{desup}^{n}\,(\operatorname{sup}^{n}\,(A,f)))\equiv
A$

and

$\displaystyle\pi_{0}\,(\pi_{1}$
$\displaystyle(\operatorname{desup}^{n}\,(\operatorname{sup}^{n}\,(A,f))))$
$\displaystyle\equiv\pi_{0}\,(\pi_{1}(\operatorname{desup}^{n}\,(\operatorname{sup}^{\infty}\,(A,\pi_{0}\circ
f),(\\_,\pi_{1}\circ f))))$
$\displaystyle\equiv\lambda\,a.(\pi_{0}\,(f\,a),\pi_{1}\,(f\,a))$
$\displaystyle\equiv\pi_{0}\,f$

Thus by the characterisation of equality in $\Sigma$-types, and equality in
subtypes, $\operatorname{desup}^{n}\circ\sup^{n}\sim\operatorname{id}$.∎

######  Theorem 13 ( ).

$V^{n}$ is a fixed-point to the functor $\operatorname{T}^{n}_{U}$.

###### Proof.

Corollary of the previous proposition.∎

######  Theorem 14.

There is an $\in$-structure $(V^{n},\in^{n})$, on $V^{n}$, of level $n$.

###### Proof.

This follows from Theorem 13 together with Theorem 3.∎

Remark: By construction, for $x,y:V^{n}$ we have
$y\in^{n}x\equiv\pi_{0}\,y\in^{\infty}\pi_{0}\,x$.

Remark: The $\in$-structure $(V^{0},\in^{0})$ is exactly the $\in$-structure
studied in _From multisets to sets in Homotopy Type Theory_ [6], which there
was established to be equivalent to the model of set theory given in the HoTT
Book [12].

###  6.2 Induction principle and recursors for $V^{n}$

Vn is a composite type: a $\Sigma$-type over a W-type and a predicate
involving induction on that W-type. Since it is not a primitive inductive type
it does not come with a ready-to-use induction principle. But, to some extent,
$\sup^{n}:\operatorname{T}^{n}_{U}\,V^{n}\rightarrow V^{n}$ acts as a
constructor, for which we have a corresponding induction principle. The
expected computation rules do not hold definitionally, but are instead proven
to hold up to identity.

######  Proposition 28 (Elimination for Vn ).

Given any family $P:V^{n}\rightarrow\operatorname{Type}$ and a function

$\phi:\prod_{A:U}\prod_{f:A\hookrightarrow_{n-1}V^{n}}\left(\prod_{a:A}P\,(f\,a)\right)\rightarrow
P\,(\sup^{n}\,(A,f))$

there is a function $\operatorname{elim}_{V^{n}}\,P\
\phi:\prod_{x:V^{n}}P\,x$.

Furthermore, there is a path $\operatorname{elim}_{V^{n}}\,P\
\phi\,(\sup^{n}(A,f))=\phi\,A\,f\,(\operatorname{elim}_{V^{n}}\,P\,\phi\circ
f)$, for any $A:U$ and $f:A\hookrightarrow_{n-1}V^{n}$.

###### Proof.

Given $x:V^{n}$, we may assume that
$x\equiv(\operatorname{sup}^{\infty}\,(A,f),(p,q))$ where $A:U$,
$f:A\rightarrow V^{\infty}$,
$p:\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}trunc\mbox{-}map\,}f$
and
$q:\prod_{a:A}\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}ittype}(f\,a)$.
The function $\operatorname{elim}_{V^{n}}\,P\ \phi$ is defined as follows

$\displaystyle\operatorname{elim}_{V^{n}}\,P\ \phi\
x:=\operatorname{tr}^{P}_{\alpha}\left(\phi\,A\,(\pi_{1}\,(\operatorname{desup}^{n}\,x))\,(\lambda\,a.\operatorname{elim}_{V^{n}}\,P\
\phi\ (f\,a,q\,a))\right)$

where $\alpha:\sup^{n}\,(\operatorname{desup}^{n}\,x)=x$ by Proposition 27. To
construct the path, we use univalence to do equivalence induction. Let $Q$ be
the type family

$\displaystyle Q:\prod_{B:\operatorname{Type}}V^{n}\simeq
B\rightarrow\operatorname{Type}$ $\displaystyle
Q\,B\,e:=\prod_{p:\prod_{b:B}P\,\left(e^{-1}\,b\right)}\prod_{b:B}\operatorname{tr}^{P}_{\alpha}\left(p\,\left(e\,\left(e^{-1}\,b\right)\right)\right)=p\,b$

where $\alpha:e^{-1}\,\left(e\,\left(e^{-1}\,b\right)\right)=e^{-1}\,b$ is the
proof that $e$ is a retraction applied to the element $e^{-1}\,b$. Then, for
the case $B:=V^{n}$ and $e:=\operatorname{id\mbox{-}equiv}$ we have

$\displaystyle
Q\,V^{n}\,\operatorname{id\mbox{-}equiv}\equiv\prod_{p:\prod_{x:V^{n}}P\,(a)}\prod_{x:V^{n}}(p\,x=p\,x)$

which is inhabited by $\lambda\,p.\operatorname{refl\mbox{-}htpy}$. By
univalence we thus have an element of the type $Q\,B\,e$ for any type $B$ and
equivalence $e:V^{n}\simeq B$. For $B:=V^{n}$ and
$e:=\operatorname{desup}^{n}$ we construct the term

$\displaystyle
p:\prod_{(A^{\prime},f^{\prime}):\operatorname{T}^{n}_{U}V^{n}}P\,(\operatorname{sup}^{n}\,(A^{\prime},f^{\prime}))$
$\displaystyle
p\,(A^{\prime},f^{\prime}):=\phi\,A^{\prime}\,f^{\prime}\,(\operatorname{elim}_{V^{n}}\,P\
\phi\ \circ f^{\prime})$

Then we have an element of the type
$Q\,\left(\operatorname{T}^{n}_{U}V^{n}\right)\,\operatorname{desup}^{n}\,p\
(A,f)$, which unfolds to

$\displaystyle\left(\operatorname{tr}^{P}_{\alpha}\left(\phi\,A\,(\pi_{1}\,(\operatorname{desup}^{n}\,x))\,(\lambda\,a.\operatorname{elim}_{V^{n}}\,P\
\phi\ (f\,a,q\,a))\right)=\phi\,A\,f\,(\operatorname{elim}_{V^{n}}\,P\ \phi\
\circ f)\right)$

where
$\alpha:\sup^{n}\,\left(\operatorname{desup}^{n}\,\left(\sup^{n}\,(A^{\prime},f^{\prime})\right)\right)=\sup^{n}\,(A^{\prime},f^{\prime})$
is the same element as was used in the construction of
$\operatorname{elim}_{V^{n}}\,P\ \phi$.∎

As usual, we can consider the specialisation from eliminators to recursors,
and in the recursors the computation rules end up holding definitionally.
Since $(n-1)$-truncated maps are also functions, $V^{n}$ actually has
recursors for both $\operatorname{T}^{\infty}_{U}$-algebras and
$\operatorname{T}^{n}_{U}$-algebras.

######  Proposition 29 (Untruncated recursion for Vn ).

Given any type $X$ and map $m:\operatorname{T}^{\infty}_{U}X\rightarrow X$
there is a map
$\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m:V^{n}\rightarrow X$ such that for $(A,f):\operatorname{T}^{n}_{U}V^{n}$ the
following definitional equality holds:

$\displaystyle\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m\ (\operatorname{sup}^{n}\,(A,f))\equiv
m\,(\operatorname{T}^{\infty}_{U}(\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m)\ (A,f))$

###### Proof.

Given $x:V^{n}$, we may assume that
$x\equiv(\operatorname{sup}^{\infty}\,(A,f),(p,q))$ where $A:U$,
$f:A\rightarrow V^{\infty}$,
$p:\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}trunc\mbox{-}map\,}f$
and
$q:\prod_{a:A}\operatorname{is\mbox{-}}(n-1)\operatorname{\mbox{-}ittype}(f\,a)$.
The map $\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}$ is
defined as:

$\displaystyle\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m\
x:=m\,(A,\lambda\,a.\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m\ (f\,a,q\,a))$

For $(A,f):\operatorname{T}^{n}_{U}V^{n}$ we thus have the following chain of
definitional equalities:

$\displaystyle\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m\ (\operatorname{sup}^{n}\,(A,f))$
$\displaystyle\equiv\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m\ (\operatorname{sup}^{\infty}\,(A,\pi_{0}\circ f),(\\_,\pi_{1}\circ f))$
$\displaystyle\equiv
m\,(A,\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\ m\circ
f)$ $\displaystyle\equiv
m\,(\operatorname{T}^{\infty}_{U}(\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m)\ (A,f))$

∎

######  Corollary 5 (Truncated recursion for Vn ).

Given a $\operatorname{T}^{n}_{U}$-algebra $(X,m)$ there is a map
$\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m):V^{n}\rightarrow
X$ such that for $(A,f):\operatorname{T}^{n}_{U}V^{n}$ the following
definitional equality holds:

$\displaystyle\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m)\,(\operatorname{sup}^{n}\,(A,f))\equiv
m\,(\operatorname{T}^{n}_{U}(\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m))\
(A,f))$

###### Proof.

The map $\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m)$ is
defined as:

$\displaystyle\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m):=\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
(\lambda\,(A,f).m\,(\operatorname{image}_{n-1}f,\operatorname{incl}_{n-1}f))$

For $(A,f):\operatorname{T}^{n}_{U}V^{n}$ we have the following chain of
definitional equalities:

$\displaystyle\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m)\,(\operatorname{sup}^{n}\,(A,f))$
$\displaystyle\equiv\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m^{\prime}\,(\operatorname{sup}^{n}\,(A,f))$ $\displaystyle\equiv
m^{\prime}\,(A,\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m^{\prime}\circ f)$ $\displaystyle\equiv
m\,(\operatorname{image}_{n-1}(\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m^{\prime}\circ
f),\operatorname{incl}_{n-1}(\operatorname{T}^{\infty}\operatorname{\mbox{-}rec}_{V^{n}}\,X\
m^{\prime}\circ f))$ $\displaystyle\equiv
m\,(\operatorname{image}_{n-1}(\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m)\circ
f),\operatorname{incl}_{n-1}(\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m)\circ
f))$ $\displaystyle\equiv
m\,(\operatorname{T}^{n}_{U}(\operatorname{T}^{n}\operatorname{\mbox{-}rec}_{V^{n}}\,(X,m))\
(A,f))$

where
$m^{\prime}:=\lambda\,(A,f).m\,(\operatorname{image}_{n-1}f,\operatorname{incl}_{n-1}f)$.∎

###  6.3 Initiality of Vn

In the proof of initiality we are to show that the type of homomorphisms from
the initial algebra, into any other algebra, is contractible. If we were
working with mere sets, it would be sufficient to show that the underlying
maps of the homomorphisms are equal to a specified canonical map. But being a
homomorphism is actually a structure when the types involved are of higher
levels. So, the proof of contractibility has to coherently transfer this
structure when proving that every homomorphism is equal to the center of
contraction. This is achieved by using the induction principle for $V^{n}$ and
the characterisation of the identity type on
$\operatorname{T}^{n}_{U}$-algebra homomorphisms.