11institutetext: Mathematical Institute, University of Oxford 11email:
<EMAIL_ADDRESS>

# The cumulative hierarchy in
Homotopy Type Theory

Ioannis Eleftheriadis 11 0000-0003-4764-8894

###### Abstract

We explore the cumulative hierarchy $V$ defined in Chapter 10 of the HoTT
book. We begin by showing how to translate formulas of set theory in HoTT, and
proceed to examine which axioms are satisfied in $V$. In particular, we show
that $V$ models ZF- in HoTT+PR, while LEM is required to obtain full ZF.
Finally, we attempt to model constructive set theories in V, and although this
is achieved for ECST, we only obtain IZF and CZF with LEM.

##  1 Introduction

Homotopy Type Theory (HoTT) is an emerging field of study within mathematics
and theoretical computer science, based on a connection between abstract
homotopy theory and intensional type theory. This connection manifests itself
in the form of a duality; on the one hand HoTT can be seen as an
interpretation and extension of Martin-Löf Type Theory (MLTT) using concepts
and ideas from homotopy theory, while on the other it can be seen as an
internal language for homotopy theory and higher category theory. Moreover,
HoTT offers a homotopical framework for the foundation of mathematics, which
differs from the standard set-theoretic foundations in many respects. Here, a
central role is played by Voevodsky’s _Univalence Axiom_ (UA) which
essentially allows isomorphic objects to be identified, something that is
frequently carried out in informal mathematical practice. While it is believed
that these univalent foundations will eventually become a viable alternative
to set theory, it is not clear a priori how the two compare in terms of
consistency strength.

A large body of work in the subject is devoted to building models of
(extensions of) HoTT within the current foundations. However, there seem to be
few results on models of set theory within HoTT. This is partly due to the
fact that this side of the question sits awkwardly between type theory and set
theory, at times requiring expertise in the former and at other times in the
latter. Furthermore, there is ambiguity as to how the underlying logic should
be interpreted. Aczel’s original model of set theory in MLTT ([4]) used a
propositions-as-types interpretation, which is strong enough to allow for full
Constructive Zermelo-Fraenkel (CZF) set theory to be modelled. Other pieces of
work treat the logic differently, resulting in models for different set
theories.

In the homotopical setting, the main point of reference is the 10th chapter of
[5]. There, a ”cumulative hierarchy of sets” is constructed as a higher
inductive type. Despite its name, the construction of this type does not
reflect the way that the standard Von Neumann hierarchy is built. This
cumulative hierarchy instead functions as a fixed hierarchy of small sets
relative to some ambient type universe, much like _Zermelo-Fraenkel algebras_
do in algebraic set theory. Furthermore, the book implicitly uses a
propositions-as-$(-1)$-types interpretation for the underlying logic, which
although very strict, permits the possibility of consistently extending HoTT
with a corresponding law of excluded middle.

The purpose of this work is to clarify and partially extend Section 10.5 of
the HoTT book. More precisely, we begin by explicitly providing semantics for
relational languages in HoTT, using the propositions-as-$(-1)$-types
interpretation. After reviewing the construction of $V$ and some of its
properties, we proceed to translate axioms of set theory and explore which of
these hold in $V$. For all of the axioms of ZF but Replacement and Separation,
these translations fully correspond to the ones given in the book, while we
provide and prove correspondences for the other two. Next, we show how under
additional assumptions we may recover Powerset, Foundation, and Choice, whose
proofs, although straightforward, do not appear to be in the literature.

The final section is devoted to constructive set theories, and contains a
combination of new results and old results translated to this homotopical
setting. Amongst other things, we prove that $V$ is a model of _Elementary
Constructive Set Theory_ (ECST), which merely rests on showing that $V$ models
Strong Infinity, as $\Delta_{0}$-Separation is essentially covered in the
book. We then briefly attempt to see if $H(x)$, the class of sets hereditarily
an image of a set in $x$, is a set in $V$, answering this in the positive for
$\omega$ as well as for general $x$ under LEM. Finally, we consider the
constructive set theories CZF and IZF with their much-discussed Collection
principles. Although we are unable to show that any of these holds in V, we
observe that they may be derived in HoTT+LEM, and are therefore consistent
with HoTT.

We shall work in HoTT:= MLTT + UA + HITs with two type universes
$U:U^{\prime}$. Recall that a type $P:U$ is called a mere proposition (or
(-1)-type) if $isProp(P):\equiv\prod_{x,y:P}x=y$ is inhabited, and $S:U$ is
called an h-set (or 0-type) if $isSet(S):\equiv\prod_{x,y:S}isProp(x=y)$ is
inhabited. We let $Prop_{U}:\equiv\sum_{P:U}isProp(P)$ and
$Set_{U}:\equiv\sum_{S:U}isSet(S)$, and we often write $P:Prop_{U}$ to mean
$P:U$ and $isProp(P)$ is inhabited, and likewise for $Set_{U}$. Also,
$\exists$ and $\lor$ refer to the propositional truncation of $\Sigma$ and
$+$, and ”merely” denotes a propositional truncation. The following axioms may
be consistently assumed:

  * •

Propositional Resizing,

PR $:\equiv Prop_{U}\simeq Prop_{U^{\prime}}$;

  * •

Law of Excluded Middle,

LEM$:\equiv\prod_{P:U}(isProp(P)\implies(P+\neg P))$;

  * •

Axiom of Choice,

AC$:\equiv\prod_{S:U}\prod_{X:U}\prod_{Y:X\to
U}(isSet(S)\land\prod_{x:X}isSet(Y(x))$

$\implies((\prod_{x:X}\|Y(x)\|)\to\|\prod_{x:X}Y(x)\|))$.

Finally, we recall the following sets of axioms, expressed in the language of
set theory (LST) $\mathscr{L}=\\{\in\\}$:

$\textbf{ZF}^{-}$ = Extensionality + Empty Set + Pairing + Union + Infinity +

Powerset + Separation Scheme + Replacement Scheme

ZF = $\textbf{ZF}^{-}$ \+ Foundation

ZFC = ZF \+ Choice

##  2 Homotopical semantics

###### Definition 1

Let $\mathscr{L}$ be a finite relational language with equality. Assume that
we have a tuple $\mathscr{T}:U$ consisting of a set $T:Set_{U}$ and functions
$R_{T}:T^{n}\to Prop_{U}$ for each n-ary relation symbol $R$ of $\mathscr{L}$.
For $\mathscr{T}$ as above, we define $\llbracket-\rrbracket_{\mathscr{T}}$ on
formulas of $\mathscr{L}$ by induction on their structure:

  * •

$\llbracket x=y\rrbracket_{\mathscr{T}}:\equiv\lambda xy.x=_{T}y$

  * •

$\llbracket R(x_{1},...,x_{k})\rrbracket_{\mathscr{T}}:\equiv R^{n}_{T}$, for
all n-ary relation symbols

  * •

$\llbracket\neg\phi\rrbracket_{\mathscr{T}}:\equiv\lambda\bar{x}.(\llbracket\phi\rrbracket_{\mathscr{T}}(\bar{x})\to\textbf{0})$

  * •

$\llbracket\phi\to\psi\rrbracket_{\mathscr{T}}:\equiv\lambda\bar{x}.(\llbracket\phi\rrbracket_{\mathscr{T}}(\bar{x})\implies\llbracket\psi\rrbracket_{\mathscr{T}}(\bar{x}))$

  * •

$\llbracket\phi\land\psi\rrbracket_{\mathscr{T}}:\equiv\lambda\bar{x}.(\llbracket\phi\rrbracket_{\mathscr{T}}(\bar{x})\land\llbracket\psi\rrbracket_{\mathscr{T}}(\bar{x}))$

  * •

$\llbracket\phi\lor\psi\rrbracket_{\mathscr{T}}:\equiv\lambda\bar{x}.(\llbracket\phi\rrbracket_{\mathscr{T}}(\bar{x})\lor\llbracket\psi\rrbracket_{\mathscr{T}}(\bar{x}))$

  * •

$\llbracket\exists
x\phi(x)\rrbracket_{\mathscr{T}}:\equiv\exists(x:T).\llbracket\phi\rrbracket_{\mathscr{T}}(x)$

  * •

$\llbracket\forall
x\phi(x)\rrbracket_{\mathscr{T}}:\equiv\forall(x:T).\llbracket\phi\rrbracket_{\mathscr{T}}(x)$

We have slightly simplified the situation by assuming FV($\phi)=$ FV($\psi$),
but it is easy to see how this definition works in general. It also follows
that $\llbracket\phi\rrbracket_{\mathscr{T}}:T^{m}\to Prop_{U}$, where
$m=\\#$FV$(\phi)$. Although this translation could be defined for arbitrary
types $T$, we would like $\llbracket\phi\rrbracket_{\mathscr{T}}$ to map into
$Prop_{U}$, and so for all $x,y:T,x=_{T}y$ must be a mere proposition, i.e.
$T$ a set.

###### Definition 2

Let $\mathscr{L}$ and $\mathscr{T}$ be as above. We call $\mathscr{T}$ a _HoTT
$\mathscr{L}$-structure_, and for $\phi\in Form(\mathscr{L})$ such that
$\llbracket\phi\rrbracket_{\mathscr{T}}:T^{k}\to Prop_{U}$ we write

$\mathscr{T}\models\phi$ if and only if
$\forall(t_{1},...,t_{k}:T).\llbracket\phi\rrbracket_{\mathscr{T}}(t_{1},...,t_{k})$
is inhabited.

For $S\subseteq Form(\mathscr{L})$, we write $\mathscr{T}\models S$ if and
only if $\mathscr{T}\models\phi$, for all $\phi\in S$.

This translation provides sound semantics for Intuitionistic Predicate Logic
(IPL).

######  Theorem 2.1 (Soundness for IPL and HoTT)

Let $\mathscr{L},\phi$ be as above and $S\subseteq Form(\mathscr{L})$. Then:

$S\vdash_{IPL}\phi$ implies that for all HoTT $\mathscr{L}$-structures
$\mathscr{T}$ such that $\mathscr{T}\models S$, $\mathscr{T}\models\phi$.

###### Proof

We consider the axioms and rules of IPL given in [3], section 2.5. Their
translations in HoTT are trivially inhabited, and hence a proof in IPL
produces a deduction in HoTT.

This establishes that we may internalise proofs in IPL as deductions in HoTT.
Naturally, one may ask if there exists an analogous completeness theorem. A
potential proof of this could invoke the completeness of IPL with respect to
the Kripke semantics given in [3], and a translation of Kripke structures in
HoTT.

##  3 V in HoTT

Recall the definition of $V$ in section 10.5 of [5]. This is a type in
$U^{\prime}$ with terms:

  * •

set$:\prod_{A:U}(A\to V)\to V$

  * •

setext$:\prod_{A,B:U}\prod_{f:A\to V}\prod_{g:B\to
V}Eq\\_img(f,g)\to\textbf{set}(A,f)=\textbf{set}(B,g)$

  * •

0-trunc$:\prod_{x,y:V}\prod_{p,q:x=y}(p=q)$,

where

$Eq\\_img(f,g):=(\forall(a:A).\exists(b:B).f(a)=g(b))\land(\forall(b:B).\exists(a:A).f(a)=g(b))$

The induction principle for $V$ says that, given $P:V\to Set_{U}$, in order to
construct $\phi:\prod_{x:V}P(x)$, it suffices to give the following.

  * •

For any $f:A\to V$, assume as given $\phi(a)$ for all $a:A$ and construct
$\phi(set(A,f))$.

  * •

For any $f:A\to V$ and $g:B\to V$ satisfying Eq$\\_$img$(f,g)$, assume as
given $\phi(f(a))$ and $\phi(g(b))$ for all $a:A,b:B$ and

$\forall(a:A).\exists(b:B).\exists(p:f(a)=g(b)).\phi(f(a))=_{p}^{P}\phi(g(b)))$

$\land\forall(b:B).\exists(a:A).\exists(p:f(a)=g(b)).\phi(f(a))=_{p}^{P}\phi(g(b)))$,

and construct a dependent path
$\phi($set$(A,f))=_{setext(A,B,f,g)}^{P}\phi($set$(B,g))$.

With this, we recover the $\in$ relation, applying induction to the second
argument.

$x\in set(A,f):\equiv(\exists(a:A).x=f(a))$,

Hence, $(V,\in)$ is an $\in$-structure in the sense of definition 1.2. We call
any mere predicate $P:V\to Prop$ a _class_ , and we say that a class _U-small_
if its codomain is $Prop_{U}$. We also call $P$ a _pure class_ if it is the
image of a $\in$-formula with one free variable, i.e.
$P\equiv\llbracket\phi(x)\rrbracket_{V}:V\to Prop$. We may define a $U$-small
resizing of the identity relation.

###### Definition 3

Define the bisimulation relation $\sim:V\times V\to Prop_{U}$ using induction
on both arguments, and letting

$set(A,f)\sim set(B,g):\equiv(\forall(a:A).\exists(b:B).f(a)\sim g(b))\land$

$(\forall(b:B).\exists(a:A).f(a)\sim g(b))$.

Similarly, we let $\tilde{\in}:V\times V\to Prop_{U}$ be
$(x,set(A,f))\mapsto\exists(a:A).x\sim f(a)$.

###### Lemma 1

For any $u,v:V$ we have $(u=_{V}v)=_{U^{\prime}}(u\sim v)$.

###### Proof

Lemma 10.5.5 in [5].

With this, one proves the following.

###### Lemma 2

For every $u:V$ there is a given $[u]:Set_{U}$ and a function $m_{u}:[u]\to V$
such that $u=set([u],m_{u})$ and $m_{u}$ is monic, i.e. $m\circ f=m\circ
g\implies f=g$.

###### Proof

See [5], Lemma 10.5.6, and [1] section 3.2.

Using the above propositions, we obtain the following.

###### Proposition 1

$(V,\in)\models$ Extensionality + Empty Set + Pairing + Union + Infinity +
Exponentiation + $\in$-induction. Furthermore we have:

  1. 1.

H-Replacement: Given any $r:V\to V$ and $x:V$, there merely exists a $w:V$
such that $y\in w\iff\exists(z:V).z\in x\land y=r(z)$ for all $y:V$.

  2. 2.

U-Separation: Given any $a:V$ and $C:V\to Prop_{U}$, there merely exists a
$w:V$ such that $x\in w\iff x\in a\land C(x)$ for all $x:V$.

###### Proof

Theorem 10.5.8 in [5].

The last two differ from the usual Replacement and Separation. Indeed, the
Replacement scheme says that for all $\phi(x,y)$ with two free variables, we
have

$\forall S(\forall x\exists!y\phi(x,y)\implies\exists w\forall v(v\in
w\iff\exists u\in S\phi(u,v)))$.

We can see that $\phi(x,y)$ plays the role of a class function. It is not
clear, however, that such a class function, which is represented by a formula,
gives rise to an actual function $r:V\to V$, which is needed in the version of
Replacement given above. Thankfully, this works out just fine.

###### Proposition 2

H-Replacement implies $\llbracket\chi\rrbracket_{V}$ for all instances of the
Replacement scheme.

###### Proof

Let $\phi(x,y)$ be a formula with two variables in an instance of Replacement.
We write $P:\equiv\llbracket\phi\rrbracket_{V}:V\times V\to Prop$, and fix
$S:V$. We begin by noting that
$\Theta(x):\equiv\sum_{y:V}(P(x,y)\times\prod_{z:V}(P(x,z)\to z=y))$ is a mere
proposition. Indeed, if $(y_{1},r_{1}),(y_{2},r_{2}):\Theta$ then
$r_{1}=r_{2}$ as $P(x,y)\times\prod_{z:V}(P(x,z)\to z=y)$ is a mere
proposition, and furthermore
$pr_{2}(r_{1})(y_{2})(pr_{1}(r_{2})):y_{1}=y_{2}$. Hence
$(y_{1},r_{1})=(y_{2},r_{2})$. It therefore follows that
$\exists!(y:V).P(x,y)\equiv\|\Theta\|\simeq\Theta$, and so we may obtain
$f:\prod_{x:V}\Theta(x)$ and define $r:V\to V$ as $\lambda x.pr_{1}(f(x))$.
Finally, H-Replacement implies that $\exists(w:V).\forall(v:V).(v\in
w\iff\exists(u\in S).v=r(u))$, but $v=r(u)$ holds if and only if $P(u,v)$, and
so the conclusion follows.

Essentially, the above proof boils down to the fact that mere propositions are
closed under unique existential quantification, i.e. if $P:U\to Prop_{U}$ then
$\exists!(x:U).P(x):\equiv\sum_{x:U}(P(x)\land\prod_{y:U}(P(y)\to x=y))$ is a
mere proposition. Unfortunately, $U$-Separation does not fully correspond to
the Separation scheme. We call a class $C:V\to Prop$ _separable_ if for any
$a:V$ the class $a\cap C:\equiv\\{x\mid x\in a\land C(x)\\}$ is a set in $V$.
$U$-Separation says that $U$-small classes are separable, whereas the
translation of the Separation scheme requires that any pure class be
separable. Since $V:U^{\prime}$, we can see that
$\llbracket\phi(x)\rrbracket_{V}:V\to Prop_{U^{\prime}}$, and so we need
$U^{\prime}$-separability to obtain full Separation. Assuming PR, this is no
longer an issue, and in fact, we may model ZF-.

######  Theorem 3.1 (HoTT + PR)

$(V,\in)\models$ ZF-.

###### Proof

It remains to show that
$\llbracket$Powerset$\rrbracket_{V}\equiv\forall(v:V).\exists(\mathscr{P}(v):V).\forall(x:V).(x\in\mathscr{P}(v)\iff
x\subseteq v)$ is inhabited. Let $\Omega:\equiv Prop_{U_{0}}$, $v:V$, and take
its monic presentation $[v]\rightarrowtail V$. We would like to define a map
$r:(V\to\Omega)\to V$ such that $r(P)\equiv\\{\\{m_{v}(t)\mid t:[v]\land
P(m_{v}(t))\\}\mid P:V\to\Omega\\}$. So, we let
$[v]_{P}:\equiv\sum_{t:[v]}P(m_{v}(t))$, and take r:$\equiv P\mapsto$
set$([v]_{P},m_{v}\circ pr_{1})$. Finally let $\mathscr{P}(v):\equiv$
set$(V\to\Omega,r)$. If $x\subseteq v$: Take $P\equiv\lambda z.z\in
x:V\to\Omega$. Then $r(P)\in\mathscr{P}(v)$ and for all $y:V$ we have that,
$y\in r(P)\iff\exists(a:[v]_{P}).(y=m_{v}\circ
pr_{1}(a))\iff\exists(b:[v])(y=m_{v}(b)\land m_{v}(b)\in x)\iff y\in x$. So
$x=r(P)$ by Extensionality, and hence $x\in\mathscr{P}(v)$. If
$x\in\mathscr{P}(v)$: Then there merely exists $P:V\to\Omega$ such that
$x=r(P)$. Hence, for all $y:V$ we have that $y\in x\iff y\in
r(P)\iff\exists(a:[v]_{P}).(y=m_{u}\circ
pr_{1}(a))\iff\exists(b:[v]).(y=m_{u}(b)\land P(m_{u}(b)))\implies y\in v$.
Hence $x\subseteq v$.

By adding LEM to our type theory, we also obtain Foundation.

######  Theorem 3.2 (HoTT + LEM)

$(V,\in)\models$ ZF.

###### Proof

We ought to show that
$\llbracket$Foundation$\rrbracket_{V}\equiv\forall(v:V).(v\neq\emptyset\implies\exists(x:V).(x\in
v\land x\cap v=\emptyset))$ is inhabited. Take $v:V$, and let
$C:\equiv\lambda(x:V).\neg(x\in v):V\to Prop$. We use the contrapositive of
$\in$-induction with $C$, to obtain an inhabitant of $\exists(v:V).\neg
C(v)\implies\exists(x:V).(\neg C(x)\land\forall(y:V).(y\in x\implies C(a)))$.
Hence, if $v\neq\emptyset$, we may produce $x:V$ with $x\in v$ such that
$\forall y\in x,y\not\in v$, i.e. $x\cap v=\emptyset$.

A reasonable question is whether we could get ZF with weaker assumptions.
Unfortunately the following implies that LEM is necessary.

###### Proposition 3

$\llbracket Foundation\rrbracket_{V}$ implies $LEM_{U}$.

###### Proof

Let $p:Prop_{U}$, and $C:V\to Prop_{U}$ to be $C(x):\equiv(x=0\land p)\lor
x=1$, where $0=\emptyset,1=\\{0\\}$. Technically, this mere proposition lives
in $U^{\prime}$ because we have used equality, but it may be resized to $U$ by
using the bisimulation relation. Using Infinity and $U$-Separation we form the
set $S_{p}:\equiv\\{x\in\omega\mid x=1\lor(x=0\land p)\\}:V$. It follows that
$1\in S_{p}$, so $S_{p}$ is non-empty. Using Foundation, we obtain $z:V$ such
that $z\in S_{p}$ and $z\cap S_{p}=\emptyset$, i.e. $\forall(y\in z).(y\not\in
S_{p})$. It follows by definition of $S_{p}$ that $z=1\lor(z=0\land p)$.
However, $z=1\implies 0\not\in S_{p}\implies\neg p$, and $(z=0\land p)\implies
p$. Hence $\neg p\lor p$.

###### Corollary 1

$(V,\in)\models$ ZF implies LEM.

Finally, assuming AC we obtain a full model of ZFC

######  Theorem 3.3 (HoTT + AC)

$(V,\in)\models$ ZFC.

###### Proof

$\llbracket$Axiom of Choice$\rrbracket_{V}\equiv\forall(x:V).((\forall(y\in
x).\exists(z:V).z\in y)\implies$

$\exists(c\in(\cup x)^{x}).\forall(y\in x).c(y)\in y)$.

So, let $x:V$ and take $A:V\to U^{\prime}$ to be the constant family $y\mapsto
V$, and $P:\prod_{x:V}A(x)\to U^{\prime}$ to be the map $(y,z)\mapsto(y\in
x\implies z\in y)$. Observe that $V$ is a set, $A(y)$ is a set for all $y:V$,
and $P(y,z)$ is a mere proposition for all $y,z:V$. AC therefore gives us that
$(\forall(y:V).\exists(z:V).y\in x\implies z\in
y)\implies(\exists(g:\prod_{y:V}A(y)).\forall(y:V).y\in x\implies g(y)\in y)$.
Hence, supposing that $(\forall(y\in x).\exists(z:V).z\in y)$, we obtain a
$g:\prod_{y:V}A(y)\equiv V\to V$ as above. Thus, we define $g^{\prime}:V\to V$
by $y\mapsto\langle y,g(y)\rangle$ using Pairing. Using Replacement with
$g^{\prime}$ and $x$, we obtain $c:V$ containing exactly the ordered pairs
$\langle y,g(y)\rangle$ for all $y\in x$. We can then see that
$function(c,x,\cup x)$, as by the assumption $y\in x\implies g(y)\in
y\subseteq\cup x$. Hence $c\in(\cup x)^{x}$ and $\forall y\in x,c(y)\equiv
g(y)\in y$.

Still, by assuming LEM or AC in our type theory we lose the computationally
valuable constructive character of HoTT. Hence, we turn to constructive set
theories, which are formulated in IPL.

##  4 Constructive Set Theories

We let $\Sigma:=$Extensionality + Empty Set + Pairing + Union.

###### Definition 4

ECST $:=\Sigma$ \+ Strong Infinity + $\Delta_{0}$-Separation + Replacement,
where

Strong Infinity $:=\exists a(Ind(a)\land\forall b(Ind(b)\implies a\subseteq
b)),$

$Ind(x):=(\emptyset\in x\land\forall y\in x\ y\cup\\{y\\}\in x)$

This is a good candidate since it omits the problematic axioms of ZF, namely
Separation, Foundation, and Powerset. In fact, we shall prove that $(V,\in)$
is a model of ECST in HoTT. We begin by rewriting the proof that $V$ models
$\Delta_{0}$-Separation found in [5] as Corollary 10.5.9.

###### Proposition 4

$(V,\in)\models\Delta_{0}$-Separation.

###### Proof

We call a class $\Delta_{0}$ if it is the image of a $\Delta_{0}$ formula of
set theory. We shall show that $\Delta_{0}$-classes are $U$-small, and hence
separable by Proposition 2.1.9.

Let $\phi(x)$ be a $\Delta_{0}$ formula of set theory, and consider the class
$C:\equiv\llbracket\phi(x)\rrbracket_{V}:V\to Prop_{U^{\prime}}$. We define a
new interpretation of formulas $\llbracket-\rrbracket_{V}^{1}$ by changing the
definition of $\llbracket x=y\rrbracket_{V}^{1}$ to $\lambda xy.x\sim y$, and
interpreting $\phi(x)$ in $(V,\tilde{\in})$. By induction we have that
$\forall(x:V).(\llbracket\psi(x)\rrbracket_{V}(x)\iff\llbracket\psi(x)\rrbracket_{V}^{1}(x))$
for all $\psi(x)\in Form(\in)$, and so $\forall(x:V).(C(x)\iff\tilde{C}(x))$.
Hence $\forall(x:V)(C(x)=\tilde{C}(x))$ by univalence, and so $C=\tilde{C}$ by
function extensionality. Hence, it suffices to show that $\tilde{C}$ is
$U$-small. This shall be done in the metatheory by induction on the structure
of $\phi(x)$.

The base cases $x\sim y:\equiv\llbracket x=y\rrbracket_{V}^{1}$ and $x\
\tilde{\in}\ y:\equiv\llbracket x\in y\rrbracket_{V}^{1}$ are already
$U$-small. Furthermore, $U$ is closed under the mere-propositional operations,
so it remains to verify this for the bounded quantifiers. Indeed, we have that

$\llbracket\exists(x\in
a)\chi(x)\rrbracket_{V}^{1}:\equiv\mid\mid\sum_{x:V}(x\ \tilde{\in}\
a\land\llbracket\chi\rrbracket_{V}^{1}(x))\mid\mid$.

We know that $(x\ \tilde{\in}\ a\land\llbracket\chi\rrbracket_{V}^{1}(x))$ is
$U$-small assuming by induction that $\llbracket\chi\rrbracket_{V}^{1}(x)$ is.
Using the type of members of $a$ as per Lemma 2.2, we obtain that

$\sum_{x:V}(x\ \tilde{\in}\
a\land\llbracket\chi\rrbracket_{V}^{1}(x))=_{U^{\prime}}\sum_{x:[a]}\llbracket\chi\rrbracket_{V}^{1}(x)$,
so

$\llbracket\exists(x\in
a)\chi(x)\rrbracket_{V}^{1}=_{U^{\prime}}\mid\mid\sum_{x:[a]}P(x)\mid\mid$,

which is in $U$, as $U$ is closed under propositional truncation. For the
universal case, we analogously obtain that $\llbracket\forall(y\in
b)\chi(y)\rrbracket_{V}^{1}=\prod_{x:[a]}\llbracket\chi\rrbracket_{V}^{1}$
which is also in $U$.

By tweaking the proof that Infinity holds in $V$, we also obtain Strong
Infinity. Notice that Strong Infinity does not only stipulate the existence of
an inductive set, but of a smallest such one. The witness of this axiom should
clearly play the role of $\omega$. Under Foundation, this is of course
equivalent to regular Infinity but this is not always true. In our case, we
may obtain Strong Infinity via the induction principle of $\mathbb{N}$.

###### Proposition 5

$(V,\in)\models$ Strong Infinity.

###### Proof

The proof of (regular) Infinity is witnessed by $\omega=set(\mathbb{N},I)$,
where $I:\mathbb{N}\to V$ is given by the recursion $I(0):\equiv\emptyset$,
and $I(succ(n)):\equiv I(n)\cup\\{I(n)\\}$. Fix $b:V$ such that
$Ind(b):\equiv\emptyset\in b\land\forall(x\in b).(x\cup\\{x\\}\in b)$ holds.
Since $x\in\omega\iff\exists(n:\mathbb{N}).(x=I(n))$, it suffices to show that
$\forall(n:\mathbb{N}).(I(n)\in\omega\implies I(n)\in b)$. Using the induction
principle of $\mathbb{N}$, we have $I(0):\equiv\emptyset\in b$, and assuming
$I(n)\in b$, we have that $I(succ(n)):\equiv I(n)\cup\\{I(n)\\}$, and so
$I(succ(n))\in b$ by the transitivity of $b$. It follows that
$\forall(x\in\omega).(x\in\beta)$, and since $b$ was arbitrary, $\omega$ is
the least transitive set.

The above two propositions imply the following theorem which appears to be new
in the literature.

###### Theorem 4.1

HoTT proves that $(V,\in)$ is a model of ECST.

Still, ECST does not fully capture the set-theory of $(V,\in)$, as it lacks
Exponentiation and $\in$-induction. We may consider the following which is
independent from ECST.

######  Proposition 6 (ITERω)

The Full Iteration Scheme, which says that for a class $C$, a class function
$F(x,y)$, and $c\in C$, there is a set $\tilde{C}$ and a unique function
$H:\omega\to\tilde{C}$ such that $H(\emptyset)=c_{0}$, and $F(H(x),H(x^{+}))$
for all $x\in\omega$, holds in V.

###### Proof

Take $C:V\to Prop$, $F:V\times V\to Prop$ such that
$\forall(x:V).\exists!(y:V).F(x,y)$ and $c:V$ such that $C(c)$ holds. By
proposition 2.2, we may internalise the class function $F$ to a function
$r:V\to V$ with $F(x,r(x))$ true. Define $f:\mathbb{N}\to V$ by $h(0)\equiv
c,f(succ(n))\equiv r(f(n))$, and take $\tilde{C}:\equiv set(\mathbb{N},f)$.
Likewise, define $h:\mathbb{N}\to V$ by $n\mapsto\langle I(n),f(n)\rangle$,
where $I:\mathbb{N}\to V$ is the map such that $\omega=set(\mathbb{N},I)$.
Taking $H:\equiv set(\mathbb{N},h)$, we see that $H$ is the unique set-
theoretic function such that $F(H(x),H(x^{+}))$ for all $x\in\omega$.

Using this with the class function $x\cup\bigcup x$ we obtain the following.

###### Corollary 2

$(V,\in)\models\forall x(x$ has a transitive closure).

One may ask if for every set $x:V$ we may construct the set $H(x):V$ of sets
hereditarily an image of a set in $x$, i.e. the smallest set such that
whenever $b\in x$ and $f:b\to H(x)$, $Imf\in H(x)$. By clever use of ITERω we
can see that $H(\omega)$ is a set in $V$. The general case is equivalent to
the following axiom, which is independent from all the ones we have examined
thus far.

######  Definition 5 (fREA)

The functional Regular Extension Axiom is the proposition:

$\forall x\exists C(x\subseteq C\land trans(C)\land\forall b\in C\ \forall
f\in C^{b}Imf\in C)$

This cannot be proven with an iteration argument as there might be ”unbounded”
functions $f:b\to x$ for $b\in x$. Nonetheless it does hold in ZF, but the
proof is non-trivial and makes heavy use of Foundation, and hence of LEM.

###### Theorem 4.2

ZF $\vdash$ fREA.

###### Proof

Proposition 4.1 in [2].

######  Corollary 3 (HoTT+LEM)

$(V,\in)\models$ fREA, and hence $H(x):V$ is a set for all $x:V$.

It is still unclear if fREA can be proved without LEM, but it seems unlikely
as it is independent from most constructive set theories. Also, ITERω may be
obtained from ECST+$\in$-induction, and so it is more appropriate to consider
set theories which contain $\in$-induction.

###### Definition 6

IZF $:=\Sigma$ \+ Infinity + Powerset + Separation + $\in$-induction +
Collection, where

Collection $:=\forall a(\forall x\in a\ \exists y\ \theta(x,y)\implies\exists
b\forall x\in a\ \exists y\in b\ \theta(x,y)),b\not\in FV(\theta)$.

###### Definition 7

CZF $:=\textbf{ECST}$ \- Replacement + $\in$-induction + Strong Collection +
Subset Collection, where

Strong Collection $:=$

$\forall a(\forall x\in a\ \exists y\phi(x,y)\implies\exists b(\forall x\in a\
\exists y\in b\phi(x,y)\land\forall y\in b\ \exists x\in a\ \phi(x,y)))$

Subset Collection $:=\forall a\forall b(\exists c\ \forall u(\forall x\in a\
\exists y\in b\psi(x,y,u)\implies$

$\exists d\in c(\forall x\in a\ \exists y\in d\ \psi(x,y,u)\land\forall y\in
d\ \exists x\in a\ \psi(x,y,u))))$,

where the formulas $\phi$ and $\psi$ may have any number of other free
variables.

In contrast to IZF, CZF is amenable to methods from ordinal-theoretic proof
theory. Let us see how CZF relates to ECST.

###### Proposition 7

The following implications hold:

  1. 1.

Strong Collection $\vdash_{IPL}$ Collection $\land$ Replacement

  2. 2.

ECST $\vdash_{IPL}$ Subset Collection $\implies$ Exponentiation

###### Proof

1 is straighforward. For 2, see Theorem 5.1.2 in [3]

It therefore follows that CZF is strictly stronger than ECST. From a classical
perspective, CZF has exactly the same strength as ZF. We write CZFc to
emphasize that we mean CZF with classical logic.

###### Proposition 8

ZF and CZFc prove the same theorems.

###### Proof

Corollary 4.2.8 in [3].

With these, one may conclude the following:

######  Corollary 4 (HoTT + LEM)

$(V,\in)\models$ CZF + IZF.

This observation, although not useful in a constructive context, establishes
that all three Collection axioms are consistent with HoTT. In fact, it appears
that these are independent from HoTT; since they are independent in IPL from
the set of axioms that were shown to hold in HoTT (even in HoTT + PR), their
satisfaction in $V$ purely depends on the ”outer” properties of $V$, i.e. its
constructors and induction principle. These, however, only appear to reflect
properties of $Set_{U}$, where again, these axiom do not seem to hold as is.
To show their independence, one would have to construct a model of HoTT where
these axioms fail in its internal cumulative hierarchy, something that goes
much beyond the purposes of this work.

## References

  * [1] Jeremy Ledent. Modeling set theory in homotopy type theory. (Research Report. https://perso.ens-lyon.fr/jeremy.ledent/internship_report.pdf). 2014\.
  * [2] Michael Rathjen, Robert Lubarsky. On the regular extension axiom and its variants. (Mathematical Logic Quarterly 49) 2003\.
  * [3] Peter Aczel, Michael Rathjen. Notes on constructive set theory. (Technical Report 40). 2001\.
  * [4] Peter Aczel. The Type Theoretic Interpretation of Constructive Set Theory. (In: A. MacIntyre, L. Pacholski, J. Paris (eds.), Logic Colloquium ’77). North-Holland, Amsterdam, 1978.
  * [5] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. (http://homotopytypetheory.org/book). Institute for Advanced Study, 2013.