University of Amsterdam, Amsterdam, the Netherlands<EMAIL_ADDRESS>https://orcid.org/0000-0003-4930-1384 Taichi Uemura [100]Theory of computation
Type theory [100]Theory of computation Denotational semantics This work is
part of the research programme “The Computational Content of Homotopy Type
Theory” with project number 613.001.602, which is financed by the Netherlands
Organisation for Scientific Research (NWO).

###### Acknowledgements.

I would like to thank Benno van den Berg, Martijn den Besten and Andrew Swan
for helpful discussions and comments, and Bas Spitters, Steve Awodey and the
anonymous reviewer for their comments, questions and suggestions.

# Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of
Propositional Resizing

Taichi Uemura

###### Abstract

We construct a model of cubical type theory with a univalent and impredicative
universe in a category of cubical assemblies. We show that this impredicative
universe in the cubical assembly model does not satisfy a form of
propositional resizing.

###### keywords:

Cubical type theory, Realizability, Impredicative universe, Univalence,
Propositional resizing

##  1 Introduction

_Homotopy type theory_ [33] is an extension of Martin-Löf’s dependent type
theory [29] with homotopy-theoretic ideas. The most important features are
Voevodsky’s _univalence axiom_ and _higher inductive types_ which provide a
novel synthetic way of proving theorems of abstract homotopy theory and
formalizing mathematics in computer proof assistants [4].

Ordinary homotopy type theory [33] uses a cumulative hierarchy of universes

$\mathcal{U}_{0}:\mathcal{U}_{1}:\mathcal{U}_{2}:\dots,$

but there is another choice of universes: one _impredicative_ universe in the
style of the Calculus of Constructions [13]. Here we say a universe
$\mathcal{U}$ is impredicative if it is closed under dependent products along
any type family: for any type $A$ and function $B:A\to\mathcal{U}$, the
dependent product $\prod_{x:A}B(x)$ belongs to $\mathcal{U}$. An interesting
use of such an impredicative universe in homotopy type theory is the
_impredicative encoding_ of higher inductive types, proposed by Shulman [35],
as well as ordinary inductive types in polymorphic type theory [19]. For
instance, the unit circle $\mathbb{S}^{1}$ is encoded as
$\prod_{X:\mathcal{U}}\prod_{x:X}x=x\to X$ which has a base point and a loop
on the point and satisfies the recursion principle in the sense of the HoTT
book [33, Chapter 6]. Although the impredicative encoding of a higher
inductive type does not satisfy the induction principle in general, some
truncated higher inductive types have refinements of the encodings satisfying
the induction principle [36, 2].

In this paper we construct a model of type theory with a univalent and
impredicative universe to prove the consistency of that type theory.
Impredicative universes are modeled in the category of _assemblies_ or
_$\omega$ -sets_ [28, 32], while univalent universes are modeled in the
categories of groupoids [21], simplicial sets [26] and cubical sets [5, 6].
Therefore, in order to construct a univalent and impredicative universe, it is
natural to combine them and construct a model of type theory in the category
of internal groupoids, simplicial or cubical objects in the category of
assemblies. There has been an earlier attempt to obtain a univalent and
impredicative universe by Stekelenburg [38] who took a simplicial approach. A
difficulty with this approach is that the category of assemblies does not
satisfy the axiom of choice or law of excluded middle, so it becomes harder to
obtain a model structure on the category of simplicial objects. Another
approach is taken by van den Berg [43] using groupoid-like objects, but his
model has a dimension restriction. Our choice is the cubical objects in the
category of assemblies, which we will call _cubical assemblies_. Since the
model in cubical sets [5, 10] is expressed, informally, in a constructive
metalogic, one would expect that their construction can be translated into the
internal language of the category of assemblies. A similar approach is taken
by Awodey, Frey and Hofstra [1, 15].

Instead of a model of homotopy type theory itself, we construct a model of a
variant of _cubical type theory_ [10] in which the univalence axiom is
provable. Orton and Pitts [30] gave a sufficient condition for modeling
cubical type theory without universes of fibrant types in an elementary topos
equipped with an interval object $\mathbb{I}$. Although the category of
cubical assemblies is not an elementary topos, most of their proofs work in
our setting because they use a dependent type theory as an internal language
of a topos and the category of cubical assemblies is rich enough to interpret
the type theory. For construction of the universe of fibrant types, we can use
the right adjoint to the exponential functor $(\mathbb{I}\to-)$ in the same
way as Licata, Orton, Pitts and Spitters [27].

Voevodsky [45] has proposed the _propositional resizing axiom_ [33, Section
3.5] which implies that every homotopy proposition is equivalent to some
homotopy proposition in the smallest universe. The propositional resizing
axiom can be seen as a form of impredicativity for homotopy propositions.
Since the universe in the cubical assembly model is impredicative, one might
expect that the cubical assembly model satisfies the propositional resizing
axiom. Indeed, for a homotopy proposition $A$, we have an approximation
$A^{*}$ of $A$ by a homotopy proposition in $\mathcal{U}$ defined as

$A^{*}:=\prod_{X:\mathsf{hProp}}(A\to X)\to X,$

where $\mathsf{hProp}$ is the universe of homotopy propositions in
$\mathcal{U}$, and $A$ is equivalent to some homotopy proposition in
$\mathcal{U}$ if and only if the function $\lambda aXh.ha:A\to A^{*}$ is an
equivalence. However, the propositional resizing axiom fails in the cubical
assembly model. We construct a homotopy proposition $A$ such that the function
$A\to A^{*}$ is not an equivalence.

We begin Section 2 by formulating the axioms for modeling cubical type theory
given by Orton and Pitts [30, 31] in a weaker setting. In Section 3 we
describe how to construct a model of cubical type theory under those axioms.
In Section 4 we give a sufficient condition for presheaf models to satisfy
those axioms. As an example of presheaf model we construct a model of cubical
type theory in cubical assemblies in Section 5, and show that the cubical
assembly model does not satisfy the propositional resizing axiom.

##  2 The Orton-Pitts Axioms

We will work in a model $\mathcal{E}$ of dependent type theory with

  * •

dependent product types, dependent sum types, extensional identity types, unit
type, disjoint finite coproducts and propositional truncation;

  * •

a constant type ${}\vdash\mathbb{I}$, called an _interval_ , with two
constants ${}\vdash 0:\mathbb{I}$ and ${}\vdash 1:\mathbb{I}$ called _end-
points_ and two operators $i,j:\mathbb{I}\vdash i\sqcap j:\mathbb{I}$ and
$i,j:\mathbb{I}\vdash i\sqcup j:\mathbb{I}$ called _connections_ ;

  * •

a dependent right adjoint to the exponential functor
$(\mathbb{I}\to-):\mathcal{E}\to\mathcal{E}$;

  * •

a propositional universe ${}\vdash\mathsf{Cof}$ whose inhabitants are called
_cofibrations_ ;

  * •

an impredicative universe ${}\vdash\mathcal{U}$

satisfying the axioms listed in Figure 1.

  1. 1.

$\neg(0=1)$

  2. 2.

$\forall_{i:\mathbb{I}}0\sqcap i=i\sqcap 0=0\land 1\sqcap i=i\sqcap 1=i$

  3. 3.

$\forall_{i:\mathbb{I}}0\sqcup i=i\sqcup 0=i\land 1\sqcup i=i\sqcup 1=1$

  4. 4.

$i:\mathbb{I}\vdash i=0:\mathsf{Cof}$

  5. 5.

$i:\mathbb{I}\vdash i=1:\mathsf{Cof}$

  6. 6.

$\varphi,\psi:\mathsf{Cof}\vdash\varphi\lor\psi:\mathsf{Cof}$

  7. 7.

$\varphi:\mathsf{Cof},\psi:\varphi\to\mathsf{Cof}\vdash\sum_{u:\varphi}\psi
u:\mathsf{Cof}$

  8. 8.

$\varphi:\mathbb{I}\to\mathsf{Cof}\vdash\forall_{i:\mathbb{I}}\varphi
i:\mathsf{Cof}$

  9. 9.

$\forall_{\varphi,\psi:\mathsf{Cof}}(\varphi\leftrightarrow\psi)\to(\varphi=\psi)$

  10. 10.

$\varphi:\mathsf{Cof},A:\varphi\to\mathcal{U},B:\mathcal{U},f:\prod_{u:\varphi}Au\cong
B\vdash\mathsf{iea}(\varphi,f):\sum_{\bar{A}:\mathcal{U}}\\{\bar{f}:\bar{A}\cong
B\mid\forall_{u:\varphi}(Au,fu)=(\bar{A},\bar{f})\\}$

Figure 1:  The Orton-Pitts Axioms

In the rest of the section we explain these conditions in more detail.

The dependent type theory we use is Martin-Löf’s extensional type theory [29].
The notion of model of dependent type theory we have in mind is categories
with families [14] equipped with certain algebraic operators corresponding to
the type formers. A _category with families_ $\mathcal{E}$ consists of:

  * •

a category $\mathcal{E}$ of _contexts_ with a terminal object denoted by
${\cdot}$;

  * •

a presheaf
$\Gamma\mapsto\mathcal{E}(\Gamma):\mathcal{E}^{\operatorname{op}}\to\mathbf{Set}$
of _types_ ;

  * •

a presheaf $(\Gamma,A)\mapsto\mathcal{E}(\Gamma\vdash
A):\mathbf{El}(\mathcal{E}(-))^{\operatorname{op}}\to\mathbf{Set}$ of _terms_
, where $\mathbf{El}(P)$ is the category of elements for a presheaf $P$

such that, for any context $\Gamma\in\mathcal{E}$ and type
$A\in\mathcal{E}(\Gamma)$, the presheaf

$(\mathcal{E}/\Gamma)^{\operatorname{op}}\ni(\sigma:\Delta\to\Gamma)\mapsto\mathcal{E}(\Delta\vdash
A\sigma)\in\mathbf{Set}$

is representable, where $A\sigma$ denotes the element $P(\sigma)(A)\in
P(\Delta)$ for a presheaf $P$, a morphism $\sigma:\Delta\to\Gamma$ and an
element $A\in P(\Gamma)$. We assume that any category with families
$\mathcal{E}$ has a choice of a representing object for this presheaf denoted
by $\pi_{A}:\Gamma.A\to\Gamma$ and called the _context extension_ of $A$. We
also require that, for every context $\Gamma\in\mathcal{E}$, there exist types
$C_{0}\in\mathcal{E}(\cdot),C_{1}\in\mathcal{E}(\cdot.C_{0}),\dots,C_{n}\in\mathcal{E}(\cdot.C_{0}.\dots.C_{n-1})$
and an isomorphism $\cdot.C_{0}.\dots.C_{n}\cong\Gamma$. This means that,
having dependent sum types, every context $\Gamma$ can be thought of a closed
type ${}\vdash\Gamma$. Type formers are modeled by algebraic operators. For
example, to model dependent product types, $\mathcal{E}$ has an operator $\Pi$
that carries triples $(\Gamma,A,B)$ consisting of a context $\Gamma$ and types
$A\in\mathcal{E}(\Gamma)$ and $B\in\mathcal{E}(\Gamma.A)$ to types
$\Pi(\Gamma,A,B)\in\mathcal{E}(\Gamma)$ and a bijection
$l(\Gamma,A,B):\mathcal{E}(\Gamma\vdash\Pi(\Gamma,A,B))\cong\mathcal{E}(\Gamma.A\vdash
B)$. These operators must be stable under base changes, that is, for any
morphism $\sigma:\Delta\to\Gamma$, we have
$\Pi(\Gamma,A,B)\sigma=\Pi(\Delta,A\sigma,B\sigma)$ and
$l(\Gamma,A,B)\sigma=l(\Delta,A\sigma,B\sigma)$. All type-theoretic operations
we introduce are required to be stable under base changes, unless otherwise
stated. Note that there are alternative choices of notions of model of
dependent type theory including categories with attributes [9] and split full
comprehension categories [24]. Whichever model is chosen, we proceed entirely
in its internal language.

In dependent type theory, a type $\Gamma\vdash\varphi$ is said to be a
_proposition_ , written $\Gamma\vdash\varphi\ \mathsf{Prop}$, if
$\Gamma,u_{1},u_{2}:\varphi\vdash u_{1}=u_{2}$ holds. For a proposition
$\Gamma\vdash\varphi$, we say $\varphi$ _holds_ if there exists a (unique)
inhabitant of $\varphi$. For a type $\Gamma\vdash A$, its _propositional
truncation_ [3] is a proposition $\Gamma\vdash\|A\|$ equipped with a
constructor $\Gamma,a:A\vdash|a|:\|A\|$ such that, for every proposition
$\Gamma\vdash\varphi$, the function $\Gamma\vdash\lambda
fa.f(|a|):(\|A\|\to\varphi)\to(A\to\varphi)$ is an isomorphism. Propositions
are closed under empty type, cartesian products and dependent products along
arbitrary types, and we write
$\bot,\top,\varphi\land\psi,\forall_{x:A}\varphi(x)$ for
$\mathbf{0},\mathbf{1},\varphi\times\psi,\prod_{x:A}\varphi(x)$, respectively,
when emphasizing that they are propositions. Also the identity type
$\mathsf{Id}(A,a_{0},a_{1})$ is a proposition because it is extensional, and
often written $a_{0}=a_{1}$. The other logical operators are defined using
propositional truncation as $\varphi\lor\psi:=\|\varphi+\psi\|$ and
$\exists_{x:A}\varphi(x):=\|\sum_{x:A}\psi(x)\|$. One can show that these
logical operations satisfy the derivation rules of first-order intuitionistic
logic. Moreover, the type theory admits subset comprehension defined as

$\Gamma\vdash\\{x:A\mid\varphi(x)\\}:=\sum_{x:A}\varphi(x)$

for a proposition $\Gamma,x:A\vdash\varphi(x)$.

A finite coproduct $A+B$ is said to be _disjoint_ if the inclusions
$\mathsf{inl}:A\to A+B$ and $\mathsf{inr}:B\to A+B$ are monic and
$\forall_{a:A}\forall_{b:B}\mathsf{inl}(a)\neq\mathsf{inr}(b)$ holds. A
proposition $\Gamma\vdash\varphi$ is said to be _decidable_ if
$\Gamma\vdash\varphi\lor\neg\varphi$ holds. If the coproduct
$\mathbf{2}:=\mathbf{1}+\mathbf{1}$ of two copies of the unit type is
disjoint, then it is a _decidable subobject classifier_ : for every decidable
proposition $\Gamma\vdash\varphi$, there exists a unique term $\Gamma\vdash
b:\mathbf{2}$ such that $\Gamma\vdash\varphi\leftrightarrow(b=1)$ holds. For
readability we identify a boolean value $b:\mathbf{2}$ with the proposition
$b=1$.

For a functor $H:\mathcal{E}\to\mathcal{F}$ between the underlying categories
of categories with families $\mathcal{E}$ and $\mathcal{F}$, a _dependent
right adjoint_ [7] to $H$ consists of, for each context $\Gamma\in\mathcal{E}$
and type $A\in\mathcal{F}(H\Gamma)$, a type
$G_{\Gamma}A\in\mathcal{E}(\Gamma)$ and an isomorphism
$\varphi_{A}:\mathcal{F}(H\Gamma\vdash A)\cong\mathcal{E}(\Gamma\vdash
G_{\Gamma}A)$ that are stable under reindexing in the sense that, for any
morphism $\sigma:\Delta\to\Gamma$, we have
$(G_{\Gamma}A)\sigma=G_{\Delta}(A\sigma)$ and
$(\varphi_{A}a)\sigma=\varphi_{A\sigma}(a\sigma)$ for any
$a\in\mathcal{F}(H\Gamma\vdash A)$. One can show that $H$ preserves all
colimits whenever it has a dependent right adjoint. As a consequence, assuming
the exponential functor $(\mathbb{I}\to-)$ has a dependent right adjoint, the
interval $\mathbb{I}$ is connected

$\forall_{\varphi:\mathbb{I}\to\mathbf{2}}(\forall_{i:\mathbb{I}}\varphi
i)\lor(\forall_{i:\mathbb{I}}\neg\varphi i),$

which is postulated in [30] as an axiom.

A _universe_ (à la Tarski) is a type ${}\vdash U$ equipped with a type
$U\vdash\mathsf{el}_{U}$. We often omit the subscript U and simply write
$\mathsf{el}$ for $\mathsf{el}_{U}$ if the universe is clear from the context.
The universe $U$ is said to be _propositional_ if $U\vdash\mathsf{el}_{U}$ is
a proposition. An _impredicative universe_ is a universe $U$ equipped with the
following operations.

  * •

A term $A:U,B:\mathsf{el}(A)\to U\vdash\sum^{U}(A,B):U$ equipped with an
isomorphism $A:U,B:\mathsf{el}(A)\to U\vdash
e:\mathsf{el}(\sum^{U}(A,B))\cong\sum_{x:\mathsf{el}(A)}\mathsf{el}(Bx)$.

  * •

A term $A:U,a_{0},a_{1}:\mathsf{el}(A)\vdash\mathsf{Id}^{U}(A,a_{0},a_{1}):U$
equipped with an isomorphism $A:U,a_{0},a_{1}:\mathsf{el}(A)\vdash
e:\mathsf{el}(\mathsf{Id}^{U}(A,a_{0},a_{1}))\cong(a_{0}=a_{1})$.

  * •

For every type $\Gamma\vdash A$, a term $\Gamma,B:\mathsf{el}(A)\to
U\vdash\prod^{U}(A,B):U$ equipped with an isomorphism
$\Gamma,B:\mathsf{el}(A)\to U\vdash
e:\mathsf{el}(\prod^{U}(A,B))\cong\prod_{x:A}\mathsf{el}(Bx)$.

One might want to require that $\mathsf{el}(\sum^{U}(A,B))$ is equal to
$\sum_{x:\mathsf{el}(A)}\mathsf{el}(Bx)$ on the nose rather than up to
isomorphism, but in the category of assemblies described in Section 5, the
impredicative universe of partial equivalence relations does not satisfy this
equation. For this reason, the distinction between terms $A:U$ and types
$\mathsf{el}(A)$ is necessary, but for readability we often identify a term
$A:U$ with the type $\mathsf{el}(A)$. For example, in Item 10 some
$\mathsf{el}$’s should be inserted formally. Also Item 6 formally means that
there exists a term
$\varphi,\psi:\mathsf{Cof}\vdash\lor^{\mathsf{Cof}}(\varphi,\psi):\mathsf{Cof}$
such that
$\varphi,\psi:\mathsf{Cof}\vdash\mathsf{el}(\lor^{\mathsf{Cof}}(\varphi,\psi))\leftrightarrow(\mathsf{el}(\varphi)\lor\mathsf{el}(\psi))$
holds.

Almost all the axioms in Figure 1 are direct translations of those in [30,
31]. Strictly speaking, Items 4, 5, 6, 7 and 8 are part of structures rather
than axioms in our setting, because $\mathsf{Cof}$ is no longer a subobject of
the subobject classifier. Also Item 10, called the _isomorphism extension
axiom_ , is part of structures. As already mentioned, the connectedness of the
interval $\mathbb{I}$ follows from the existence of the right adjoint to the
exponential functor $(\mathbb{I}\to-)$. We need Item 9, which asserts the
extensionality of the propositional universe $\mathsf{Cof}$, for fibration
structures on identity types. This axiom trivially holds in case that
$\mathsf{Cof}$ is a subobject of the subobject classifier in an elementary
topos. We also note that $\mathsf{Cof}$ is closed under $\bot$, $\top$ and
$\land$ using Items 1, 5 and 7.

##  3 Modeling Cubical Type Theory

We describe how to construct a model of a variant of cubical type theory in
our setting following Orton and Pitts [30]. Throughout the section
$\mathcal{E}$ will be a model of dependent type theory satisfying the
conditions explained in Section 2. Type-theoretic notations in this section
are understood in the internal language of $\mathcal{E}$.

Cubical type theory is an extension of dependent type theory with an _interval
object_ [10, Section 3], the _face lattice_ [10, Section 4.1], _systems_ [10,
Section 4.2], _composition operations_ [10, Section 4.3] and the _gluing
operation_ [10, Section 6]. It also has several type formers including
dependent product types, dependent sum types, _path types_ [10, Section 3]
and, optionally, _identity types_ [10, Section 9.1]. We make some
modifications to the original cubical type theory [10] in the same way as
Orton and Pitts [30]. Major differences are as follows.

  1. 1.

In [10] the interval object $\mathbb{I}$ is a de Morgan algebra, while we only
require that $\mathbb{I}$ is a path connection algebra.

  2. 2.

Due to the lack of de Morgan involution, we need composition operations in
both directions “from $0$ to $1$” and “from $1$ to $0$”.

In this section we will construct from $\mathcal{E}$ a new model of dependent
type theory $\mathcal{E}^{F}$ that supports all operations of cubical type
theory.

###  3.1 The Face Lattice and Systems

The _face lattice_ [10, Section 4.1] is modeled by the propositional universe
$\mathsf{Cof}$. Note that in [10] quantification
$\forall_{i:\mathbb{I}}\varphi$ is not part of syntax and written as a
disjunction of irreducible elements, and plays a crucial role for defining
composition operation for gluing. Since $\mathsf{Cof}$ need not admit
quantifier elimination, we explicitly require Item 8.

We use the following operation for modeling _systems_ [10, Section 4.2] which
allows one to amalgamate compatible partial functions.

######  Proposition 3.1.

One can derive an operation Γ⊢A
Γ⊢φ_i Prop
Γ, u_i : φ_i ⊢a_i(u_i) : A
Γ, u : φ_i, u’ : φ_j ⊢a_i(u) = a_j(u’)
($i$ and $j$ run over $\\{1,\dots,n\\}$) Γ⊢[(u_1 : φ_1) ↦a_1(u_1), …, (u_n :
φ_n) ↦a_n(u_n)] : φ_1 ∨…∨φ_n →A such that
$\Gamma,v:\varphi_{i}\vdash[(u_{1}:\varphi_{1})\mapsto
a_{1}(u_{1}),\dots,(u_{n}:\varphi_{n})\mapsto a_{n}(u_{n})]v=a_{i}(v)$ for
$i=1,\dots,n$.

######  Proof 3.2.

Let $B$ denote the union of images of $a_{i}$’s:

$\Gamma\vdash
B:=\\{a:A\mid(\exists_{u_{1}:\varphi_{1}}a_{1}(u_{1})=a)\lor\dots\lor(\exists_{u_{n}:\varphi_{n}}a_{n}(u_{n})=a)\\}.$

Then $\Gamma\vdash B$ is a proposition because
$\Gamma,u:\varphi_{i},u^{\prime}:\varphi_{j}\vdash a_{i}(u)=a_{j}(u^{\prime})$
for all $i$ and $j$. Hence the function
$[a_{1},\dots,a_{n}]:\varphi_{1}+\dots+\varphi_{n}\to B$ induces a function
$\|\varphi_{1}+\dots+\varphi_{n}\|\to B$.

###  3.2 Fibrations

We regard the type of Boolean values $\mathbf{2}$ as a subtype of the interval
$\mathbb{I}$ via the end-point inclusion
$[0,1]:\mathbf{2}\cong\mathbf{1}+\mathbf{1}\to\mathbb{I}$. We define a term
$e:\mathbf{2}\vdash\bar{e}:\mathbf{2}$ as $\bar{0}=1$ and $\bar{1}=0$.

######  Definition 3.3.

For a type $\Gamma,i:\mathbb{I}\vdash A(i)$, we define a type of _composition
structures_ as

$\Gamma\vdash\mathsf{Comp}^{i}(A(i)):={}\prod_{e:\mathbf{2}}\prod_{\varphi:\mathsf{Cof}}\prod_{f:\varphi\to\prod_{i:\mathbb{I}}A(i)}\prod_{a:A(e)}(\forall_{u:\varphi}fue=a)\to\\{a^{\prime}:A(\bar{e})\mid\forall_{u:\varphi}fu\bar{e}=a^{\prime}\\}.$

In this notation, the variable $i$ is considered to be bound.

######  Definition 3.4.

For a type $\gamma:\Gamma\vdash A(\gamma)$, we define a type of _fibration
structures_ as

${}\vdash\mathsf{Fib}(A):=\prod_{p:\mathbb{I}\to\Gamma}\mathsf{Comp}^{i}(A(pi)).$

A _fibration_ is a type $\Gamma\vdash A$ equipped with a global section
${}\vdash\alpha:\mathsf{Fib}(A)$.

For a fibration structure $\alpha:\mathsf{Fib}(A)$ on a type
$\gamma:\Gamma\vdash A(\gamma)$ and a morphism $\sigma:\Delta\to\Gamma$, we
define a fibration structure $\alpha\sigma:\mathsf{Fib}(A\sigma)$ on
$\delta:\Delta\vdash A(\sigma(\delta))$ as

$\alpha\sigma=\lambda p.\alpha(\sigma\circ
p):\prod_{p:\mathbb{I}\to\Delta}\mathsf{Comp}^{i}(A(\sigma(pi))).$

Thus, for a fibration $(A,\alpha)$ on $\Gamma$, we have its _base change_
$(A\sigma,\alpha\sigma)$ along a morphism $\sigma:\Delta\to\Gamma$. With this
base change operation we get a model $\mathcal{E}^{F}$ of dependent type
theory where

  * •

the contexts are those of $\mathcal{E}$;

  * •

the types over $\Gamma$ are fibrations over $\Gamma$;

  * •

the terms of a fibration $\Gamma\vdash A$ are terms of the underlying type
$\Gamma\vdash A$ in $\mathcal{E}$

together with a forgetful map $\mathcal{E}^{F}\to\mathcal{E}$. In the same way
as Orton and Pitts [30], one can show the following.

######  Theorem 3.5.

The model of dependent type theory $\mathcal{E}^{F}$ supports:

  * •

composition operations, path types and identity types; and

  * •

dependent product types, dependent sum types, unit type and finite coproducts
preserved by the forgetful map $\mathcal{E}^{F}\to\mathcal{E}$.

We also introduce a class of objects that automatically carry fibration
structures.

######  Definition 3.6.

A type ${}\vdash A$ is said to be _discrete_ if $\forall_{f:\mathbb{I}\to
A}\forall_{i:\mathbb{I}}fi=f0$ holds.

######  Proposition 3.7.

If ${}\vdash A$ is a discrete type, then it has a fibration structure.

######  Proof 3.8.

Let $e:\mathbf{2}$, $\varphi:\mathsf{Cof}$, $f:\varphi\to\mathbb{I}\to A$ and
$a:A$ such that $\forall_{u:\varphi}fue=a$. Then $a^{\prime}:=a:A$ satisfies
$\forall_{u:\varphi}fu\bar{e}=a^{\prime}$ by the discreteness.

###  3.3 Path Types and Identity Types

For a type $\Gamma\vdash A$ and terms $\Gamma\vdash a_{0}:A$ and $\Gamma\vdash
a_{1}:A$, we define the _path type_ $\Gamma\vdash\mathsf{Path}(A,a_{0},a_{1})$
to be

$\Gamma\vdash\\{p:\mathbb{I}\to A\mid p0=a_{0}\land p1=a_{1}\\}.$

We also define the _identity type_ $\Gamma\vdash\mathsf{Id}(A,a_{0},a_{1})$ to
be

$\Gamma\vdash\sum_{p:\mathsf{Path}(A,a_{0},a_{1})}\\{\varphi:\mathsf{Cof}\mid\varphi\to\forall_{i:\mathbb{I}}pi=a_{0}\\}$

which is a variant of Swan’s construction [39]. Theorem 3.5 says that, if $A$
has a fibration structure, then so do $\mathsf{Path}(A,a_{0},a_{1})$ and
$\mathsf{Id}(A,a_{0},a_{1})$.

In the model $\mathcal{E}^{F}$, both path types and identity types admit the
following introduction and elimination operations: Γ⊢a : A Γ⊢refl_a : P(A, a,
a) $P$-intro Γ, x_0 : A, x_1 : A, z : P(A, x_0, x_1) ⊢C(z)
Γ, x : A ⊢c(x) : C(refl_x)
Γ⊢a_0 : A
Γ⊢a_1 : A
Γ⊢p : P(A, a_0, a_1) Γ⊢ind_P(A)(C, c, p) : C(p) $P$-elim where $P$ is either
$\mathsf{Path}$ or $\mathsf{Id}$. A difference between them is their
computation rules. Identity types admit the _judgmental_ computation rule like
Martin-Löf’s identity types:

$\Gamma\vdash\mathsf{ind}_{\mathsf{Id}(A)}(C,c,\mathsf{refl}_{a})=c(a)$

for a term $\Gamma\vdash a:A$. On the other hand, path types only admit the
_propositional_ computation rule: for a term $\Gamma\vdash a:A$, one can find
a term

$\Gamma\vdash
H(C,c,a):\mathsf{Path}(C(a),\mathsf{ind}_{\mathsf{Path}(A)}(C,c,\mathsf{refl}_{a}),c(a)).$

Therefore, when interpreting homotopy type theory, which is based on Martin-
Löf’s type theory, we use $\mathsf{Id}(A,a_{0},a_{1})$ rather than
$\mathsf{Path}(A,a_{0},a_{1})$. However, it can be shown that
$\mathsf{Id}(A,a_{0},a_{1})$ and $\mathsf{Path}(A,a_{0},a_{1})$ are
equivalent, and thus we can replace $\mathsf{Id}(A,a_{0},a_{1})$ by simpler
type $\mathsf{Path}(A,a_{0},a_{1})$ when analyzing the model $\mathcal{E}^{F}$
(see, for instance, the definition of homotopy proposition in Section 5.1).

###  3.4 Universes and Gluing

For a type $\gamma:\Gamma\vdash A(\gamma)$, a fibration structure on $A$
corresponds to a term of the type
$p:\mathbb{I}\to\Gamma\vdash\mathsf{C}(A)(p):=\mathsf{Comp}^{i}(A(pi))$. We
define a type $\Gamma\vdash FA:=\mathsf{C}(A)_{\mathbb{I}}$, using the
dependent right adjoint $(-)_{\mathbb{I}}$ to the exponential functor
$(\mathbb{I}\to-)$. By definition a morphism $\sigma:\Delta\to\sum_{\Gamma}FA$
corresponds to a pair $(\sigma_{0},\alpha)$ consisting of a morphism
$\sigma_{0}:\Delta\to\Gamma$ and a fibration structure
${}\vdash\alpha:\prod_{p:\mathbb{I}\to\Delta}\mathsf{Comp}^{i}(A(\sigma_{0}(pi)))$.

Using this construction for the universe
$\mathcal{U}\vdash\mathsf{el}_{\mathcal{U}}$, we have a new universe
$\mathcal{U}^{F}:=\sum_{\mathcal{U}}F(\mathsf{el})$ together with a fibration
$(A,\alpha):\mathcal{U}^{F}\vdash\mathsf{el}_{\mathcal{U}^{F}}(A,\alpha):=\mathsf{el}_{\mathcal{U}}(A)$.
By definition $\mathcal{U}^{F}$ classifies fibrations whose underlying types
belong to $\mathcal{U}$.

######  Theorem 3.9.

The universe $\mathcal{U}^{F}$ is closed under dependent product types along
arbitrary fibrations, dependent sum types and path types. If $\mathsf{Cof}$
belongs to $\mathcal{U}$, then $\mathcal{U}^{F}$ is closed under identity
types.

######  Proof 3.10.

By Theorem 3.5, it suffices to show that $\mathcal{U}$ is closed under those
type constructors, but this is clear by definition.

We describe the _gluing operation_ on the universe $\mathcal{U}^{F}$ following
Orton and Pitts [30].

For a proposition $\Gamma\vdash\varphi$, types $\Gamma,u:\varphi\vdash A(u)$
and $\Gamma\vdash B$ and a function $\Gamma,u:\varphi\vdash f(u):A(u)\to B$,
we define a type $\mathsf{Glue}(\varphi,f)$ to be

$\Gamma\vdash\mathsf{Glue}(\varphi,f):=\sum_{a:\prod_{u:\varphi}A(u)}\\{b:B\mid\forall_{u:\varphi}f(u)(au)=b\\}.$

There is a canonical isomorphism $\Gamma,u:\varphi\vdash
e(u):=\lambda(a,b).au:\mathsf{Glue}(\varphi,f)\cong A(u)$ with inverse
$\lambda a.(\lambda v.a,f(u)a)$.

######  Proposition 3.11.

For $\gamma:\Gamma\vdash\varphi(\gamma):\mathsf{Cof}$,
$\gamma:\Gamma,u:\varphi(\gamma)\vdash A(u)$, $\gamma:\Gamma\vdash B(\gamma)$
and $\gamma:\Gamma,u:\varphi(\gamma)\vdash f(u):A(u)\to B$, if $A$ and $B$ are
fibrations and $f$ is an equivalence, then
$\gamma:\Gamma\vdash\mathsf{Glue}(\varphi(\gamma),f)$ has a fibration
structure preserved by the canonical isomorphism $\Gamma,u:\varphi\vdash
e(u):\mathsf{Glue}(\varphi,f)\cong A(u)$.

######  Proof 3.12.

The construction is similar to the definition of the composition operation for
glue types [10, Section 6.2].

Since the universe $\mathcal{U}$ is closed under type formers used in the
definition of $\mathsf{Glue}(\varphi,f)$, we get a term

$\varphi:\mathsf{Cof},A:\varphi\to\mathcal{U},B:\mathcal{U},f:\prod_{u:\varphi}A(u)\to
B\vdash\mathsf{Glue}(\varphi,f):\mathcal{U}$

such that $\prod_{u:\varphi}\mathsf{Glue}(\varphi,f)\cong A(u)$. However, the
gluing operation in cubical type theory [10, Section 6] requires that,
assuming $u:\varphi$, $\mathsf{Glue}(\varphi,f)$ is equal to $A(u)$ on the
nose rather than up to isomorphism. So we use Item 10 and get a term

$\varphi:\mathsf{Cof},A:\varphi\to\mathcal{U},B:\mathcal{U},f:\prod_{u:\varphi}A(u)\to
B\vdash\mathsf{SGlue}(\varphi,f):\mathcal{U}$

such that $\mathsf{SGlue}(\varphi,f)\cong\mathsf{Glue}(\varphi,f)$ and
$\forall_{u:\varphi}\mathsf{SGlue}(\varphi,f)=A(u)$. By Proposition 3.11 we
also have a term

$\varphi:\mathsf{Cof},A:\varphi\to\mathcal{U}^{F},B:\mathcal{U}^{F},f:\prod_{u:\varphi}A(u)\simeq
B\vdash\mathsf{SGlue}(\varphi,f):\mathcal{U}^{F}$

such that $\mathsf{SGlue}(\varphi,f)\cong\mathsf{Glue}(\varphi,f)$ and
$\forall_{u:\varphi}\mathsf{SGlue}(\varphi,f)=A(u)$. Hence the universe
$\mathcal{U}^{F}$ in the model $\mathcal{E}^{F}$ supports the gluing
operation. The composition operation for universes is defined using the gluing
operation [10, Section 7.1], so we have the following proposition.

######  Proposition 3.13.

${}\vdash\mathcal{U}^{F}$ has a fibration structure.

Since the univalence axiom can be derived from the gluing operation [10,
Section 7], we conclude that $\mathcal{U}^{F}$ is a univalent and
impredicative universe in the model of cubical type theory $\mathcal{E}^{F}$.

##  4 Presheaf Models

In this section we give a sufficient condition for a presheaf category to
satisfy the conditions in Section 2. We will work in a model $\mathcal{S}$ of
dependent type theory with dependent product types, dependent sum types,
extensional identity types, unit type, disjoint finite coproducts and
propositional truncation.

A _category_ in $\mathcal{S}$ consists of:

  * •

a type ${}\vdash\mathbf{C}_{0}$ of _objects_ ;

  * •

a type $c_{0},c_{1}:\mathbf{C}_{0}\vdash\mathbf{C}_{1}(c_{0},c_{1})$ of
_morphisms_ ;

  * •

a term $c:\mathbf{C}_{0}\vdash\mathsf{id}_{c}:\mathbf{C}_{1}(c,c)$ called
_identity_ ;

  * •

a term
$c_{0},c_{1},c_{2}:\mathbf{C}_{0},g:\mathbf{C}_{1}(c_{1},c_{2}),f:\mathbf{C}_{1}(c_{0},c_{1})\vdash
gf:\mathbf{C}_{1}(c_{0},c_{2})$ called _composition_

satisfying the standard axioms of category. We will simply write $\mathbf{C}$
and $\mathbf{C}(c_{0},c_{1})$ for $\mathbf{C}_{0}$ and
$\mathbf{C}_{1}(c_{0},c_{1})$ respectively. The notions of functor and natural
transformation in $\mathcal{S}$ are defined in the obvious way. For a category
$\mathbf{C}$ in $\mathcal{S}$, a _presheaf_ on $\mathbf{C}$ consists of:

  * •

a type $c:\mathbf{C}\vdash A(c)$;

  * •

a term $c_{0},c_{1}:\mathbf{C},\sigma:\mathbf{C}(c_{0},c_{1}),a:A(c_{1})\vdash
a\sigma:A(c_{0})$ called _(right) $\mathbf{C}$-action_

satisfying $a\mathsf{id}=a$ and $a(\sigma\tau)=(a\sigma)\tau$. For presheaves
$A$ and $B$, a _morphism_ $f:A\to B$ is a term $c:\mathbf{C},a:A(c)\vdash
f(a):B(c)$ satisfying
$c_{0},c_{1}:\mathbf{C},\sigma:\mathbf{C}(c_{0},c_{1}),a:A(c_{1})\vdash
f(a\sigma)=f(a)\sigma$. For a presheaf $A$, its _category of elements_ ,
written $\mathbf{El}(A)$, is defined as

  * •

${}\vdash\mathbf{El}(A)_{0}:=\sum_{c:\mathbf{C}_{0}}A(c)$;

  * •

$(c_{0},a_{0}),(c_{1},a_{1}):\mathbf{El}(A)_{0}\vdash\mathbf{El}(A)_{1}((c_{0},a_{0}),(c_{1},a_{1})):=\\{\sigma:\mathbf{C}_{1}(c_{0},c_{1})\mid
a_{1}\sigma=a_{0}\\}$.

There is a projection functor $\pi_{A}:\mathbf{El}(A)\to\mathbf{C}$.

For a category $\mathbf{C}$ in $\mathcal{S}$, we describe the presheaf model
$\mathbf{PSh}(\mathbf{C})$ of dependent type theory. Contexts are interpreted
as presheaves on $\mathbf{C}$. For a context $\Gamma$, types on $\Gamma$ are
interpreted as presheaves on $\mathbf{El}(\Gamma)$. For a type $\Gamma\vdash
A$, terms of $A$ are interpreted as sections of the projection
$\pi_{A}:\mathbf{El}(A)\to\mathbf{El}(\Gamma)$. For a type $\Gamma\vdash A$,
the context extension $\Gamma.A$ is interpreted as the presheaf
$c:\mathbf{C}\vdash\sum_{\gamma:\Gamma(c)}A(c,\gamma)$. This construction is
also used for dependent sum types. The dependent product for a type
$\Gamma.A\vdash B$ is the presheaf

$\displaystyle(c,\gamma):\mathbf{El}(\Gamma)\vdash{}$
$\displaystyle\\{f:\prod_{c^{\prime}:\mathbf{C}}\prod_{\sigma:\mathbf{C}(c^{\prime},c)}\prod_{a:A(c^{\prime},\gamma\sigma)}B(c^{\prime},a)\mid$
$\displaystyle\forall_{c^{\prime},c^{\prime\prime}:\mathbf{C}}\forall_{\sigma:\mathbf{C}(c^{\prime},c)}\forall_{\tau:\mathbf{C}(c^{\prime\prime},c^{\prime})}\forall_{a:A(c^{\prime},\gamma\sigma)}(fc^{\prime}\sigma
a)\tau=fc^{\prime\prime}(\sigma\tau)(a\tau)\\}.$

Extensional identity types, unit type, disjoint finite coproducts and
propositional truncation are pointwise.

###  4.1 Lifting Universes

We describe the Hofmann-Streicher lifting of a universe [20]. Let $\mathbf{C}$
be a category in $\mathcal{S}$ and $U$ a universe in $\mathcal{S}$. We define
a universe $[\mathbf{C}^{\operatorname{op}},U]$ in $\mathbf{PSh}(\mathbf{C})$
as follows. The universe $U$ can be seen as a category whose type of objects
is $U$ and type of morphisms is
$A,B:U\vdash\mathsf{el}_{U}(A)\to\mathsf{el}_{U}(B)$. For an object
$c:\mathbf{C}$, we define $[\mathbf{C}^{\operatorname{op}},U](c)$ to be the
type of functors from $(\mathbf{C}/c)^{\operatorname{op}}$ to $U$. The
$\mathbf{C}$-action on $[\mathbf{C}^{\operatorname{op}},U]$ is given by
precomposition. The type
$[\mathbf{C}^{\operatorname{op}},U]\vdash\mathsf{el}_{[\mathbf{C}^{\operatorname{op}},U]}$
in $\mathbf{PSh}(\mathbf{C})$ is defined as
$(c,A):\mathbf{El}([\mathbf{C}^{\operatorname{op}},U])\vdash\mathsf{el}_{[\mathbf{C}^{\operatorname{op}},U]}(c,A):=\mathsf{el}_{U}(A(\mathsf{id}_{c}))$.

It is easy to show that, if $U$ is an impredicative universe, then dependent
product types, dependent sum types and extensional identity types in $U$ can
be lifted to those in $[\mathbf{C}^{\operatorname{op}},U]$ so that
$[\mathbf{C}^{\operatorname{op}},U]$ is an impredicative universe in
$\mathbf{PSh}(\mathbf{C})$. If $U$ is a propositional universe in
$\mathcal{S}$, then $[\mathbf{C}^{\operatorname{op}},U]$ is a propositional
universe in $\mathbf{PSh}(\mathbf{C})$.

######  Proposition 4.1.

Let $\mathcal{U}$ be an impredicative universe and $\mathsf{Cof}$ a
propositional universe in $\mathcal{S}$. If they satisfy Items 6, 7, 9 and 10,
then so do $[\mathbf{C}^{\operatorname{op}},\mathcal{U}]$ and
$[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$.

######  Proof 4.2.

We only check Item 10. The other axioms are easy to verify.

We have to define a term
$\varphi:[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}],A:\varphi\to[\mathbf{C}^{\operatorname{op}},\mathcal{U}],B:[\mathbf{C}^{\operatorname{op}},\mathcal{U}],f:\prod_{u:\varphi}Au\cong
B\vdash(D(\varphi,f),g(\varphi,f)):\sum_{\bar{A}:[\mathbf{C}^{\operatorname{op}},\mathcal{U}]}\\{\bar{f}:\bar{A}\cong
B\mid\forall_{u:\varphi}(Au,fu)=(\bar{A},\bar{f})\\}$ in
$\mathbf{PSh}(\mathbf{C})$. It corresponds to a natural transformation that
takes an object $c:\mathbf{C}$, functors
$\varphi:(\mathbf{C}/c)^{\operatorname{op}}\to\mathsf{Cof}$,
$A:\mathbf{El}(\varphi)^{\operatorname{op}}\to\mathcal{U}$ and
$B:(\mathbf{C}/c)^{\operatorname{op}}\to\mathcal{U}$ and an isomorphism
$f:A\cong B\pi_{\varphi}$ of presheaves on $\mathbf{El}(\varphi)$ and returns
a pair $(D(c,\varphi,f),g(c,\varphi,f))$ consisting of a functor
$D(c,\varphi,f):(\mathbf{C}/c)^{\operatorname{op}}\to\mathcal{U}$ and an
isomorphism $g(c,\varphi,f):A\cong B$ of presheaves on
$(\mathbf{C}/c)^{\operatorname{op}}$ such that $D(c,\varphi,f)\pi_{\varphi}=A$
and $g(c,\varphi,f)\pi_{\varphi}=f$. Let $\sigma:\mathbf{C}(c^{\prime},c)$ be
a morphism. Then we have $\varphi(\sigma):\mathsf{Cof}$, $\lambda
u.A(\sigma,u):\varphi(\sigma)\to\mathcal{U}$, $B(\sigma):\mathcal{U}$ and an
isomorphism $\lambda u.f(\sigma,u):\prod_{u:\varphi(\sigma)}A(\sigma,u)\cong
B(\sigma)$. By the isomorphism lifting on $\mathcal{U}$, we have
$D(c,\varphi,f)(\sigma):\mathcal{U}$ and an isomorphism
$g(c,\varphi,f)(\sigma):D(c,\varphi,f)(\sigma)\cong B(\sigma)$ such that
$\forall_{u:\varphi(\sigma)}(A(\sigma,u),f(\sigma,u))=(D(c,\varphi,f)(\sigma),g(c,\varphi,f)(\sigma))$.
For the morphism part of the functor $D(c,\varphi,f)$, let
$\tau:\mathbf{C}(c^{\prime\prime},c^{\prime})$ be another morphism. Then we
define $\tau^{*}:D(c,\varphi,f)(\sigma)\to D(c,\varphi,f)(\sigma\tau)$ to be
the composition

${D(c,\varphi,f)(\sigma)}$${B(\sigma)}$${B(\sigma\tau)}$${D(c,\varphi,f)(\sigma\tau).}$$\scriptstyle{g(c,\varphi,f)(\sigma)}$$\scriptstyle{\cong}$$\scriptstyle{\tau^{*}}$$\scriptstyle{g(c,\varphi,f)(\sigma\tau)^{-1}}$$\scriptstyle{\cong}$

By definition $g(c,\varphi,f)$ becomes a natural isomorphism and
$(D(c,\varphi,f)\pi_{\varphi},g(c,\varphi,f)\pi_{\varphi})=(A,f)$. It is easy
to see the naturality of
$(c,\varphi,f)\mapsto(D(c,\varphi,f),g(c,\varphi,f))$.

###  4.2 Intervals

Suppose a category $\mathbf{C}$ in $\mathcal{S}$ has finite products. A _path
connection algebra_ in $\mathbf{C}$ consists of an object
$\mathbb{I}:\mathbf{C}$, morphisms
$\delta_{0},\delta_{1}:\mathbf{C}(1,\mathbb{I})$ called _end-points_ and
morphisms $\mu_{0},\mu_{1}:\mathbf{C}(\mathbb{I}\times\mathbb{I},\mathbb{I})$
called _connections_ satisfying
$\mu_{e}(\delta_{e}\times\mathbb{I})=\mu_{e}(\mathbb{I}\times\delta_{e})=\delta_{e}$
and
$\mu_{e}(\delta_{\bar{e}}\times\mathbb{I})=\mu_{e}(\mathbb{I}\times\delta_{\bar{e}})=\mathsf{id}$
for $e\in\\{0,1\\}$.

For a path connection algebra $\mathbb{I}$ in $\mathbf{C}$, we have a
representable presheaf $\mathbf{y}\mathbb{I}$ on $\mathbf{C}$. Since the
Yoneda embedding is fully faithful and preserves finite products,
$\mathbf{y}\mathbb{I}$ has end-points and connections satisfying Items 2 and
3. The interval $\mathbf{y}\mathbb{I}$ satisfies Item 1 if and only if
$\forall_{c:\mathbf{C}}\delta_{0}!_{c}\neq\delta_{1}!_{c}$ holds, where
$!_{c}:\mathbf{C}(c,1)$ is the unique morphism into the terminal object.

######  Proposition 4.3.

Let $\mathsf{Cof}$ be a propositional universe in $\mathcal{S}$ and suppose
that, for every pair of objects $c,c^{\prime}:\mathbf{C}$, the equality
predicate on $\mathbf{C}(c,c^{\prime})$ belongs to $\mathsf{Cof}$. Then, for
every object $c:\mathbf{C}$, the equality predicate on $\mathbf{y}c$ belongs
to $[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$. In particular,
$\mathbf{y}\mathbb{I}$ and $[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$ in
$\mathbf{PSh}(\mathbf{C})$ satisfy Items 4 and 5.

######  Proof 4.4.

Because equality on a presheaf is pointwise.

######  Proposition 4.5.

For a functor $f:\mathbf{C}\to\mathbf{D}$ between categories in $\mathcal{S}$,
the precomposition functor
$f^{*}:\mathbf{PSh}(\mathbf{D})\to\mathbf{PSh}(\mathbf{C})$ has a dependent
right adjoint $f_{*}$.

######  Proof 4.6.

For a context $\Gamma$ in $\mathbf{PSh}(\mathbf{D})$ and a type
$f^{*}\Gamma\vdash A$ in $\mathbf{PSh}(\mathbf{C})$, the type $\Gamma\vdash
f_{*}A$ is given by the presheaf
$(d,\gamma):\mathbf{El}(\Gamma)\vdash\lim_{(c,\sigma):(f\downarrow
d)}A(c,\gamma\sigma)$.

######  Proposition 4.7.

Suppose that a category $\mathbf{C}$ in $\mathcal{S}$ has finite products. For
an object $c:\mathbf{C}$, the exponential functor
$(\mathbf{y}c\to-):\mathbf{PSh}(\mathbf{C})\to\mathbf{PSh}(\mathbf{C})$ is
isomorphic to $(-\times c)^{*}$.

######  Proof 4.8.

$(\mathbf{y}c\to
A)(c^{\prime})\cong\mathbf{PSh}(\mathbf{C})(\mathbf{y}c^{\prime}\times\mathbf{y}c,A)\cong\mathbf{PSh}(\mathbf{C})(\mathbf{y}(c^{\prime}\times
c),A)\cong A(c^{\prime}\times c)$.

Hence the exponential functor $(\mathbf{y}\mathbb{I}\to-)$ has a dependent
right adjoint. Proposition 4.7 also implies Item 8 for the propositional
universe $[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$. Explicitly,
$\forall_{\mathbf{y}\mathbb{I}}:(-\times\mathbf{y}\mathbb{I})^{*}[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]\to[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$
is a natural transformation that carries a functor
$\varphi:(\mathbf{C}/c\times\mathbb{I})^{\operatorname{op}}\to\mathsf{Cof}$ to
$\lambda\sigma.\varphi(\sigma\times\mathbb{I}):(\mathbf{C}/c)^{\operatorname{op}}\to\mathsf{Cof}$.

In summary, we have:

######  Theorem 4.9.

Suppose:

  * •

$\mathcal{S}$ is a model of dependent type theory with dependent product
types, dependent sum types, extensional identity types, unit type, disjoint
finite coproducts and propositional truncation;

  * •

$\mathsf{Cof}$ is a propositional universe and $\mathcal{U}$ is an
impredicative universe satisfying Items 6, 7, 9 and 10;

  * •

$\mathbf{C}$ is a category in $\mathcal{S}$ with finite products and the
equality on $\mathbf{C}(c,c^{\prime})$ belongs to $\mathsf{Cof}$ for every
pair of objects $c,c^{\prime}:\mathbf{C}$;

  * •

$\mathbb{I}$ is a path connection algebra in $\mathbf{C}$;

  * •

$\mathbf{y}\mathbb{I}$ satisfies Item 1.

Then the presheaf model $\mathbf{PSh}(\mathbf{C})$ together with propositional
universe $[\mathbf{C}^{\operatorname{op}},\mathsf{Cof}]$, impredicative
universe $[\mathbf{C}^{\operatorname{op}},\mathcal{U}]$ and interval
$\mathbf{y}\mathbb{I}$ satisfies all the axioms in Figure 1.

###  4.3 Decidable Subobject Classifier

An example of the propositional universe $\mathsf{Cof}$ in Theorem 4.9 is the
decidable subobject classifier $\mathbf{2}$ which always satisfies Items 6, 7
and 9.

######  Proposition 4.10.

In a model of dependent type theory with dependent product types, dependent
sum types, extensional identity types, unit type, disjoint finite coproducts
and propositional truncation, any universe $\mathcal{U}$ satisfies Item 10
with $\mathsf{Cof}=\mathbf{2}$.

######  Proof 4.11.

Let
$\varphi:\mathbf{2},A:\varphi\to\mathcal{U},B:\mathcal{U},f:\prod_{u:\varphi}Au\cong
B$. We define $\mathsf{iea}(\varphi,f)$ by case analysis on
$\varphi:\mathbf{2}$ as $\mathsf{iea}(0,f):=(B,\mathsf{id})$ and
$\mathsf{iea}(1,f):=(A{*},f{*})$ where ${*}$ is the unique element of a
singleton type.

###  4.4 Categories of Cubes

We present examples of internal categories $\mathbf{C}$ with a path connection
algebra $\mathbb{I}$ satisfying the hypotheses of Theorem 4.9 with
$\mathsf{Cof}=\mathbf{2}$. Obvious choices of $\mathbf{C}$ are the category of
free de Morgan algebras [10] and various syntactic categories of the language
$\\{0,1,\sqcap,\sqcup\\}$ [8], but some inductive types and quotient types are
required to construct these categories in dependent type theory. Although the
motivating example of $\mathcal{S}$, the category of assemblies described in
Section 5, has inductive types and finite colimits, quotients are not well-
behaved in general and we need to be careful in using quotients. Instead, we
give examples definable only using natural numbers.

Suppose $\mathcal{S}$ is a model of dependent type theory with dependent
product types, dependent sum types, extensional identity types, unit type,
disjoint finite coproducts, propositional truncation and natural numbers. We
define a type of finite types $n:\mathbb{N}\vdash\mathsf{Fin}_{n}$ to be
$\mathsf{Fin}_{n}=\\{k:\mathbb{N}\mid k<n\\}$. We define a category
$\mathbf{B}$ as follows. Its object of objects is $\mathbb{N}$. The morphisms
$m\to n$ are functions
$(\mathsf{Fin}_{m}\to\mathbf{2})\to(\mathsf{Fin}_{n}\to\mathbf{2})$. In the
category $\mathbf{B}$, the terminal object is $0:\mathbb{N}$ and the product
of $m$ and $n$ is $m+n$. One can show, by induction, that every
$\mathbf{B}(m,n)$ has decidable equality. $\mathbf{B}$ has a path connection
algebra $1:\mathbb{N}$ together with end-points
$0,1:(\mathsf{Fin}_{0}\to\mathbf{2})\to(\mathsf{Fin}_{1}\to\mathbf{2})$ and
connections
$\mathsf{min},\mathsf{max}:(\mathsf{Fin}_{1}\to\mathbf{2})\times(\mathsf{Fin}_{1}\to\mathbf{2})\to(\mathsf{Fin}_{1}\to\mathbf{2})$.
One can show that the category $\mathbf{B}$ satisfies the hypotheses of
Theorem 4.9. Moreover, any subcategory of $\mathbf{B}$ that has the same
finite products and contains the path connection algebra $1$ satisfies the
same condition. An example is the wide subcategory $\mathbf{B}_{\mathsf{ord}}$
of $\mathbf{B}$ where the morphisms are order-preserving functions
$(\mathsf{Fin}_{m}\to\mathbf{2})\to(\mathsf{Fin}_{n}\to\mathbf{2})$.

###  4.5 Constant and Codiscrete Presheaves

We show some properties of constant and codiscrete presheaves which will be
used in Section 5. Let $\mathcal{S}$ be a model of dependent type theory
satisfying the hypotheses of Theorem 4.9. For an object $A\in\mathcal{S}$, we
define the _constant presheaf_ $\Delta A$ to be $\Delta A(c):=A$ with the
trivial $\mathbf{C}$-action.

######  Proposition 4.12.

Every constant presheaf $\Delta A$ is discrete.

######  Proof 4.13.

For every $c:\mathbf{C}$, we have $(\mathbf{y}\mathbb{I}\to\Delta
A)(c)\cong\Delta A(c\times\mathbb{I})=A$ by Proposition 4.7.

For a type $\Gamma\vdash A$ in $\mathcal{S}$, we define the _codiscrete
presheaf_ $\Delta\Gamma\vdash\nabla A$ to be $\nabla
A(c,\gamma):=\mathbf{C}(1,c)\to A(\gamma)$ with composition as the
$\mathbf{C}$-action.

######  Proposition 4.14.

Suppose that $\mathsf{Cof}=\mathbf{2}$. Then for every type $\Gamma\vdash A$
in $\mathcal{S}$, the type $\Delta\Gamma\vdash\nabla A$ has a fibration
structure.

######  Proof 4.15.

Since $\Delta\Gamma$ is discrete, it suffices to show that $\nabla A(\gamma)$
has a fibration structure for every $\gamma:\Gamma$. Thus we may assume that
$\Gamma$ is the empty context. We construct a term

$\alpha:\prod_{e:\mathbf{2}}\prod_{\varphi:[\mathbf{C}^{\operatorname{op}},\mathbf{2}]}\prod_{f:\varphi\to\mathbb{I}\to\nabla
A}\prod_{a:\nabla A}(\forall_{u:\varphi}fue=a)\to\\{\bar{a}:\nabla
A\mid\forall_{u:\varphi}fu\bar{e}=\bar{a}\\}$

in $\mathbf{PSh}(\mathbf{C})$. It corresponds to a natural transformation that
takes an object $c:\mathbf{C}$, an element $e:\mathbf{2}$, a functor
$\varphi:(\mathbf{C}/c)^{\operatorname{op}}\to\mathbf{2}$, a natural
transformation
$f:\int_{c^{\prime}\in\mathbf{C}}(\sum_{\sigma:\mathbf{C}(c^{\prime},c)}\varphi(\sigma))\times\mathbf{C}(c^{\prime},\mathbb{I})\to\nabla
A(c^{\prime})$ and an element $a:\nabla A(c)$ such that
$\forall_{c^{\prime}:\mathbf{C}}\forall_{\sigma:\mathbf{C}(c^{\prime},c)}\forall_{u:\varphi(\sigma)}f(\sigma,u,e)=a\sigma$
and returns an element $\alpha(e,\varphi,f,a):\nabla A(c)$ such that
$\forall_{c^{\prime}:\mathbf{C}}\forall_{\sigma:\mathbf{C}(c^{\prime},c)}\forall_{u:\varphi(\sigma)}f(\sigma,u,\bar{e})=\alpha(e,\varphi,f,a)\sigma$.
We define $\alpha(e,\varphi,f,a):\mathbf{C}(1,c)\to A$ as

$\alpha(e,\varphi,f,a)(\sigma):=\left\\{\begin{array}[]{ll}f(\sigma,u,\bar{e})(\mathsf{id}_{1})&\text{if
$u:\varphi(\sigma)$ is found}\\\ a(\sigma)&\text{otherwise}\end{array}\right.$

for $\sigma:\mathbf{C}(1,c)$. Then by definition
$\forall_{c^{\prime}:\mathbf{C}}\forall_{\sigma:\mathbf{C}(c^{\prime},c)}\forall_{u:\varphi(\sigma)}f(\sigma,u,\bar{e})=\alpha(e,\varphi,f,a)\sigma$.

######  Proposition 4.16.

Suppose that $\mathbf{C}(1,\mathbb{I})$ only contains $0$ and $1$, namely
$\forall_{\sigma:\mathbf{C}(1,\mathbb{I})}\sigma=0\lor\sigma=1$. Then for
every type $\Gamma\vdash A$ in $\mathcal{S}$, there exists a term

$\Delta\Gamma\vdash p:\prod_{a_{0},a_{1}:\nabla A}\mathsf{Path}(\nabla
A,a_{0},a_{1})$

in $\mathbf{PSh}(\mathbf{C})$.

######  Proof 4.17.

We may assume that $\Gamma$ is the empty context. The term $p$ corresponds to
a natural transformation that takes an object $c:\mathbf{C}$, elements
$a_{0},a_{1}:\nabla A(c)$ and a morphism $i:\mathbf{C}(c,\mathbb{I})$ and
returns an element $p(a_{0},a_{1},i):\nabla A(c)$ such that
$p(a_{0},a_{1},0)=a_{0}$ and $p(a_{0},a_{1},1)=a_{1}$. We define
$p(a_{0},a_{1},i):\mathbf{C}(1,c)\to A$ as

$p(a_{0},a_{1},i)(\sigma):=\left\\{\begin{array}[]{ll}a_{0}(\sigma)&\text{if
$i\sigma=0$}\\\ a_{1}(\sigma)&\text{if $i\sigma=1$}\end{array}\right.$

for $\sigma:\mathbf{C}(1,c)$. Then by definition $p(a_{0},a_{1},0)=a_{0}$ and
$p(a_{0},a_{1},1)=a_{1}$.

##  5 A Failure of Propositional Resizing in Cubical Assemblies

An _assembly_ , also called an _$\omega$ -set_, is a set $A$ equipped with a
non-empty set $E_{A}(a)$ of natural numbers for every $a\in A$. When $n\in
E_{A}(a)$, we say $n$ is a _realizer_ for $a$ or $n$ _realizes_ $a$. A
morphism $f:A\to B$ of assemblies is a function $f:A\to B$ between the
underlying sets such that there exists a partial recursive function $e$ such
that, for any $a\in A$ and $n\in E_{A}(a)$, the application $en$ is defined
and belongs to $E_{B}(f(a))$. In that case we say $f$ is _tracked_ by $e$ or
$e$ is a _tracker_ of $f$. We shall denote by $\mathbf{Asm}$ the category of
assemblies and morphisms of assemblies. Note that assemblies can be defined in
terms of partial combinatory algebras instead of natural numbers and partial
recursive functions [44], and that the rest of this section works for
assemblies on any non-trivial partial combinatory algebra.

The category $\mathbf{Asm}$ is a model of dependent type theory. Contexts are
interpreted as assemblies. Types $\Gamma\vdash A$ are interpreted as families
of assemblies $(A(\gamma)\in\mathbf{Asm})_{\gamma\in\Gamma}$ indexed over the
underlying set of $\Gamma$. Terms $\Gamma\vdash a:A$ are interpreted as
sections $a\in\prod_{\gamma\in\Gamma}A(\gamma)$ such that there exists a
partial recursive function $e$ such that, for any $\gamma\in\Gamma$ and $n\in
E_{\Gamma}(\gamma)$, the application $en$ is defined and belongs to
$E_{A(\gamma)}(a(\gamma))$. For a type $\Gamma\vdash A$, the context extension
$\Gamma.A$ is interpreted as an assembly
$(\sum_{\gamma\in\Gamma}A(\gamma),(\gamma,a)\mapsto\\{\langle n,m\rangle\mid
n\in E_{\Gamma}(\gamma),m\in E_{A(\gamma)}(a)\\})$ where $\langle n,m\rangle$
is a fixed effective encoding of tuples of natural numbers. It is known that
$\mathbf{Asm}$ supports dependent product types, dependent sum types,
extensional identity types, unit type, disjoint finite coproducts and natural
numbers. See, for example, [44, 28, 25]. For a family of assemblies $A$ over
$\Gamma$, the propositional truncation $\|A\|$ is the family

$\|A\|(\gamma)=\left\\{\begin{array}[]{lr}\\{{*}\\}&\text{if
$A(\gamma)\neq\emptyset$}\\\ \emptyset&\text{if
$A(\gamma)=\emptyset$}\end{array}\right.$

with realizers $E_{\|A\|(\gamma)}(*)=\bigcup_{a\in
A(\gamma)}E_{A(\gamma)}(a)$.

It is also well-known that $\mathbf{Asm}$ has an impredicative universe
$\mathbf{PER}$. It is an assembly whose underlying set is the set of partial
equivalence relations, namely symmetric and transitive relations, on
$\mathbb{N}$ and the set of realizers of $R$ is $E_{\mathbf{PER}}(R)=\\{0\\}$.
The type $\mathbf{PER}\vdash\mathsf{el}_{\mathbf{PER}}$ is defined as
$\mathsf{el}_{\mathbf{PER}}(R)=\mathbb{N}/R$, the set of $R$-equivalence
classes on $\\{n\in\mathbb{N}\mid R(n,n)\\}$ with realizers
$E_{\mathbb{N}/R}(\xi)=\xi$. The universe $\mathbf{PER}$ classifies _modest
families_. An assembly $A$ is said to be _modest_ if $E_{A}(a)$ and
$E_{A}(a^{\prime})$ are disjoint for distinct $a,a^{\prime}\in A$. By
definition $\mathbb{N}/R$ is modest for every $R\in\mathbf{PER}$. Conversely,
for a modest assembly $A$, one can define a partial equivalence relation $R$
such that $A\cong\mathbb{N}/R$. For the impredicativity of $\mathbf{PER}$, see
[23, 28, 25].

The category $\mathbf{Asm}$ satisfies the hypotheses of Theorem 4.9 with
impredicative universe $\mathbf{PER}$, propositional universe $\mathbf{2}$ and
the internal category $\mathbf{B}_{\mathsf{ord}}$ defined in Section 4.4. We
will refer to the presheaf model of cubical type theory generated by these
structures as the _cubical assembly model_.

###  5.1 Propositional Resizing

In cubical type theory, a type $\Gamma\vdash A$ is a _homotopy proposition_ if
the type $\Gamma,a_{0},a_{1}:A\vdash\mathsf{Path}(A,a_{0},a_{1})$ has an
inhabitant. For a universe $\mathcal{U}$, we define the universe of homotopy
propositions as

$\mathsf{hProp}_{\mathcal{U}}:=\sum_{A:\mathcal{U}}\prod_{a_{0},a_{1}:A}\mathsf{Path}(A,a_{0},a_{1}).$

Following the HoTT book [33], we regard $\mathsf{hProp}_{\mathcal{U}}$ as a
subtype of $\mathcal{U}$.

The _propositional resizing axiom_ [33, Section 3.5] asserts that, for nested
universes $\mathcal{U}:\mathcal{U}^{\prime}$, the inclusion
$\mathsf{hProp}_{\mathcal{U}}\to\mathsf{hProp}_{\mathcal{U}^{\prime}}$ is an
equivalence. When $\mathcal{U}$ is an impredicative universe, we define

$\displaystyle A:\mathsf{hProp}_{\mathcal{U}^{\prime}}$ $\displaystyle\vdash
A^{*}:=\prod_{X:\mathsf{hProp}_{\mathcal{U}}}(A\to X)\to
X:\mathsf{hProp}_{\mathcal{U}}$ $\displaystyle
A:\mathsf{hProp}_{\mathcal{U}^{\prime}}$ $\displaystyle\vdash\eta_{A}:=\lambda
a.\lambda Xf.fa:A\to A^{*}.$

If $\eta_{A}$ is an equivalence for any
$A:\mathsf{hProp}_{\mathcal{U}^{\prime}}$, then the inclusion
$\mathsf{hProp}_{\mathcal{U}}\to\mathsf{hProp}_{\mathcal{U}^{\prime}}$ is an
equivalence by univalence. Conversely, if the inclusion
$\mathsf{hProp}_{\mathcal{U}}\to\mathsf{hProp}_{\mathcal{U}^{\prime}}$ is an
equivalence, then one can find $A^{\prime}:\mathsf{hProp}_{\mathcal{U}}$ and
$e:A\simeq A^{\prime}$ from $A:\mathsf{hProp}_{\mathcal{U}^{\prime}}$. Then we
have a function $\lambda\alpha.e^{-1}(\alpha A^{\prime}e):A^{*}\to A$, and
thus $\eta_{A}$ is an equivalence because both $A$ and $A^{*}$ are homotopy
propositions. Note that the construction $A\mapsto(A^{*},\eta_{A})$ works for
any homotopy proposition $A$ and is independent of the choice of the upper
universe $\mathcal{U}^{\prime}$. Therefore, we can formulate the propositional
resizing axiom in cubical type theory with an impredicative universe as
follows.

######  Axiom 1.

For every homotopy proposition $\Gamma\vdash A$, the function
$\Gamma\vdash\eta_{A}:A\to A^{*}$ is an equivalence.

We will show that the cubical assembly model does not satisfy 1.

######  Remark 5.1.

We focus on resizing propositions into the impredicative universe. The cubical
assembly model also has predicative universes, assuming the existence of
Grothendieck universes in the metatheory. It remains an open question whether
the predicative universes in the cubical assembly model satisfy the
propositional resizing axiom.

###  5.2 Uniform Objects

The key idea to a counterexample to propositional resizing is the
orthogonality of modest and _uniform_ assemblies [44]: if $X$ is modest and
$A$ is uniform and well-supported, then the map $\lambda xa.x:X\to(A\to X)$ is
an isomorphism. Since the impredicative universe $\mathbf{PER}$ classifies
modest assemblies, $\prod_{X:\mathbf{PER}}(A\to X)\to X$ is always inhabited
for a uniform, well-supported assembly $A$. We extend the notion of uniformity
for internal presheaves in $\mathbf{Asm}$.

An assembly $A$ is said to be _uniform_ if $\bigcap_{a\in A}E_{A}(a)$ is non-
empty. We say an internal presheaf $A$ on an internal category $\mathbf{C}$ is
_uniform_ if every $A(c)$ is uniform. An internal presheaf $A$ on $\mathbf{C}$
is said to be _well-supported_ if the unique morphism into the terminal
presheaf is regular epi. For an internal presheaf $A$, the following are
equivalent:

  * •

$A$ is well-supported;

  * •

$\|A\|$ is the terminal presheaf;

  * •

there exists a partial recursive function $e$ such that, for any
$c\in\mathbf{C}_{0}$ and $n\in E_{\mathbf{C}_{0}}(c)$, there exists an $a\in
A(c)$ such that $en$ is defined and belongs to $E_{A}(a)$.

By definition a modest assembly cannot distinguish elements with a common
realizer, while elements of a uniform assembly have a common realizer. Thus a
modest assembly “believes a uniform assembly has at most one element”.
Formally, the following proposition holds.

######  Proposition 5.2.

Let $\mathbf{C}$ be a category in $\mathbf{Asm}$. For a uniform internal
presheaf $A$ on $\mathbf{C}$ and an internal functor
$X:\mathbf{C}^{\operatorname{op}}\to\mathbf{PER}$, the precomposition function

$i^{*}:(\|A\|\to X)\to(A\to X)$

is an isomorphism, where $i:A\to\|A\|$ is the constructor for propositional
truncation. In particular, if, in addition, $A$ is well-supported, then the
function $\lambda xa.x:X\to(A\to X)$ is an isomorphism.

######  Proof 5.3.

Since $i$ is regular epi, $i^{*}$ is a monomorphism. Hence it suffices to show
that $i^{*}$ is regular epi. Let $k_{c}$ denote a common realizer of $A(c)$,
namely $k_{c}\in\bigcap_{a\in A(c)}E(a)$. Let $c\in\mathbf{C}_{0}$ be an
object and $x:\mathbf{y}c\times A\to X$ a morphism of presheaves tracked by
$e$. We have to show that there exists a morphism
$\hat{x}:\mathbf{y}c\times\|A\|\to X$ such that
$\hat{x}\circ(\mathbf{y}c\times i)=x$ and that a tracker of $\hat{x}$ is
computable from the code of $e$. For any $\sigma:c^{\prime}\to c$ and
$a,a^{\prime}\in A(c^{\prime})$, we have $enk_{c^{\prime}}\in
E(x(\sigma,a))\cap E(x(\sigma,a^{\prime}))$ for some $n\in E(\sigma)$. Since
$X(c^{\prime})$ is modest, we have $x(\sigma,a)=x(\sigma,a^{\prime})$. Hence
$x$ induces a morphism of presheaves $\hat{x}:\mathbf{y}c\times\|A\|\to X$
tracked by $e$ such that $\hat{x}\circ(\mathbf{y}c\times i)=x$.

######  Theorem 5.4.

Let $\Gamma\vdash A$ be a type in the cubical assembly model. Suppose that $A$
is uniform and well-supported as an internal presheaf on $\mathbf{El}(\Gamma)$
and does not have a section. Then the function $\Gamma\vdash\eta:A\to A^{*}$
is not an equivalence.

######  Proof 5.5.

By Proposition 5.2, we see that $A^{*}=\prod_{X:\mathsf{hProp}}(A\to X)\to X$
has an inhabitant while $A$ does not have an inhabitant by assumption.

######  Theorem 5.6.

Let $\Gamma\vdash A$ be a type in $\mathbf{Asm}$. Suppose that $A$ is uniform
and well-supported but does not have a section. Then the function
$\Delta\Gamma\vdash\eta:\nabla A\to(\nabla A)^{*}$ is not an equivalence.

######  Proof 5.7.

By Theorem 5.4, it suffices to show that the type $\Delta\Gamma\vdash\nabla A$
is uniform and well-supported but does not have a section. For the uniformity,
let $k_{\gamma}$ be a common realizer of $A(\gamma)$ for $\gamma\in\Gamma$.
For any object $c\in\mathbf{C}$ and element $\gamma\in\Gamma$, the code of the
constant function $n\mapsto k_{\gamma}$ is a common realizer of $\nabla
A(c,\gamma)=\mathbf{C}(1,c)\to A(\gamma)$.

For the well-supportedness, let $e$ be a partial recursive function such that,
for any $\gamma$ and $n\in E_{\Gamma}(\gamma)$, there exists an $a\in
A(\gamma)$ such that $en$ is defined and belongs to $E_{A(\gamma)}(a)$. Then
the function $f$ mapping $(n,x)$ to the code of the function $y\mapsto ex$
realizes that $\nabla A$ is well-supported. Indeed, for any $c\in\mathbf{C}$,
$n\in E_{\mathbf{C}}(c)$, $\gamma\in\Gamma$ and $x\in E_{\Gamma}(\gamma)$, the
code $f(n,x)$ realizes the constant function $\mathbf{C}(1,c)\ni\sigma\mapsto
a\in A(\gamma)$ for some $a\in A(\gamma)$ such that $ex\in E_{A(\gamma)}(a)$.

Finally $\nabla A$ does not have a section because $\nabla A(1)\cong A$ and
$A$ does not have a section.

###  5.3 The Counterexample

We define an assembly $\Gamma$ to be
$(\mathbb{N},n\mapsto\\{m\in\mathbb{N}\mid m>n\\})$ and a family of assemblies
$A$ on $\Gamma$ as $A(n)=(\\{m\in\mathbb{N}\mid m>n\\},m\mapsto\\{n,m\\})$.
Then $A$ is uniform because every $A(n)$ has a common realizer $n$. The
identity function realizes that $A$ is well-supported. To see that $A$ does
not have a section, suppose that a section $f\in\prod_{n\in\Gamma}A(n)$ is
tracked by a partial recursive function $e$. Then for any $m>n$, we have
$em\in\\{n,f(n)\\}$. This implies that $m\leq e(m+1)\leq f(0)$ for any $m$, a
contradiction. Note that this construction of $\Gamma\vdash A$ works for any
non-trivial partial combinatory algebra $C$ because natural numbers can be
effectively encoded in $C$.

Since $\mathbf{B}_{\mathsf{ord}}(1,\mathbb{I})\cong\mathbf{2}$ only contains
end-points, the type $\Delta\Gamma\vdash\nabla A$ in the cubical assembly
model is a fibration and homotopy proposition by Propositions 4.14 and 4.16,
while by Theorem 5.6 the function $\Delta\Gamma\vdash\eta:\nabla A\to(\nabla
A)^{*}$ is not an equivalence. Hence the propositional resizing axiom fails in
the cubical assembly model.

##  6 Conclusion and Future Work

We have formulated the axioms for modeling cubical type theory in an
elementary topos given by Orton and Pitts [30] in a weaker setting and
explained how to construct a model of cubical type theory in a category
satisfying those axioms. As a striking example, we have constructed a model of
cubical type theory with an impredicative and univalent universe in the
category of cubical assemblies which is not an elementary topos. It has turned
out that this impredicative universe in the cubical assembly model does not
satisfy the propositional resizing axiom.

There is a natural question: can we construct a model of type theory with a
univalent and impredicative universe satisfying the propositional resizing
axiom? One possible approach to this question is to consider a full
subcategory of the category of cubical assemblies in which every homotopy
proposition is equivalent to some modest family. Benno van den Berg [43]
constructed a model of a variant of homotopy type theory with a univalent and
impredicative universe of $0$-types that satisfies the propositional resizing
axiom. Roughly speaking he uses a category of degenerate trigroupoids in the
category of _partitioned assemblies_ [44], and thus the category of cubical
partitioned assemblies is a candidate for such a full subcategory. However,
the model given in [43] only supports weaker forms of identity types and
dependent product types, and it is unclear whether it can be seen as a model
of ordinary homotopy type theory.

Higher inductive types are another important feature of homotopy type theory.
One can construct some higher inductive types including propositional
truncation in the cubical assembly model [42], internalizing the construction
of higher inductive types in cubical sets [12] using $W$-types with reductions
[41]. An open question, raised by Steve Awodey, is whether these higher
inductive types are equivalent to their impredicative encodings.

The cubical assembly model is a realizability-based model of type theory with
higher dimensional structures, but it does not seem to be what should be
called a _realizability $\infty$-topos_, a higher dimensional analogue of a
realizability topos [44]. One problem is that, in the cubical assembly model,
realizers seem to play no role in its internal cubical type theory, because
the existence of a realizer of a homotopy proposition does not imply the
existence of a section of it. Indeed, the cubical assembly model does not
satisfy Church’s Thesis [42] which holds in the effective topos [22]. One can
nevertheless find a left exact localization of the cubical assembly model in
which Church’s Thesis holds [42].

Our construction of models of cubical type theory is a syntactic one following
Orton and Pitts [30]. The original idea of using the internal language of a
topos to construct models of cubical type theory was proposed by Coquand [11].
There are also semantic and categorical approaches. Frumin and van den Berg
[16] presented a way of constructing a model structure on a full subcategory
of an elementary topos with a path connection algebra, which is essentially
same as the model structure on the category of fibrant cubical sets described
by Spitters [37]. Since they make no essential use of subobject classifiers,
we conjecture that one can construct a model structure on a full subcategory
of a suitable locally cartesian closed category with a path connection
algebra. Sattler [34], based on his earlier work with Gambino [17], gave a
construction of a right proper combinatorial model structure on a suitable
category with an interval object. Although Gambino and Sattler use Garner’s
small object argument [18] which requires the cocompleteness of underlying
categories, their construction is expected to work for non-cocomplete
categories such as the category of cubical assemblies using Swan’s small
object argument over codomain fibrations [40, 41].

## References

  * [1] Steve Awodey.  Impredicative encodings in HoTT, 2017.  Talk at the workshop “Computer-aided mathematical proof”.  URL: http://www.newton.ac.uk/seminar/20170711090010001.
  * [2] Steve Awodey, Jonas Frey, and Sam Speight.  Impredicative Encodings of (Higher) Inductive Types.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 76–85, New York, NY, USA, 2018. ACM.  doi:10.1145/3209108.3209130.
  * [3] Steven Awodey and Andrej Bauer.  Propositions As [Types].  J. Log. and Comput., 14(4):447–471, 8 2004.  doi:10.1093/logcom/14.4.447.
  * [4] Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.  The HoTT Library: A Formalization of Homotopy Type Theory in Coq.  In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164–172, New York, NY, USA, 2017. ACM.  doi:10.1145/3018610.3018615.
  * [5] Marc Bezem, Thierry Coquand, and Simon Huber.  A Model of Type Theory in Cubical Sets.  In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107–128, Dagstuhl, Germany, 2014. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  doi:10.4230/LIPIcs.TYPES.2013.107.
  * [6] Marc Bezem, Thierry Coquand, and Simon Huber.  The Univalence Axiom in Cubical Sets.  Journal of Automated Reasoning, 63(2):159–171, Aug 2019.  doi:10.1007/s10817-018-9472-6.
  * [7] Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters.  Modal Dependent Type Theory and Dependent Right Adjoints, 2019.  arXiv:1804.05236v3.
  * [8] Ulrik Buchholtz and Edward Morehouse.  Varieties of Cubical Sets.  In Peter Höfner, Damien Pous, and Georg Struth, editors, Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings, pages 77–92. Springer International Publishing, Cham, 2017.  doi:10.1007/978-3-319-57418-9_5.
  * [9] J.W. Cartmell.  Generalised algebraic theories and contextual categories.  PhD thesis, Oxford University, 1978.
  * [10] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.  Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.  In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  doi:10.4230/LIPIcs.TYPES.2015.5.
  * [11] Thierry Coquand.  Internal version of the uniform Kan filling condition, 2015.  URL: http://www.cse.chalmers.se/~coquand/shape.pdf.
  * [12] Thierry Coquand, Simon Huber, and Anders Mörtberg.  On Higher Inductive Types in Cubical Type Theory.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 255–264, New York, NY, USA, 2018. ACM.  doi:10.1145/3209108.3209197.
  * [13] Thierry Coquand and Gérard Huet.  The Calculus of Constructions.  Information and Computation, 76(2):95 – 120, 1988.  doi:10.1016/0890-5401(88)90005-3.
  * [14] Peter Dybjer.  Internal Type Theory.  In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs: International Workshop, TYPES ’95 Torino, Italy, June 5–8, 1995 Selected Papers, pages 120–134. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996.  doi:10.1007/3-540-61780-9_66.
  * [15] Jonas Frey.  Towards a realizability model of homotopy type theory, 2017.  Talk at CT 2017.  URL: http://www.mat.uc.pt/~ct2017/slides/frey_j.pdf.
  * [16] Dan Frumin and Benno van den Berg.  A homotopy-theoretic model of function extensionality in the effective topos.  Mathematical Structures in Computer Science, pages 1–27, 2018.  doi:10.1017/S0960129518000142.
  * [17] Nicola Gambino and Christian Sattler.  The Frobenius condition, right properness, and uniform fibrations .  Journal of Pure and Applied Algebra, 221(12):3027 – 3068, 2017\.  doi:10.1016/j.jpaa.2017.02.013.
  * [18] Richard Garner.  Understanding the Small Object Argument.  Applied Categorical Structures, 17(3):247–285, 6 2009.  doi:10.1007/s10485-008-9137-4.
  * [19] Jean-Yves Girard, Yves Lafont, and Paul Taylor.  Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 1989.  URL: http://www.paultaylor.eu/stable/Proofs+Types.html.
  * [20] Martin Hofmann and Thomas Streicher.  Lifting Grothendieck Universes, 1997.  URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  * [21] Martin Hofmann and Thomas Streicher.  The groupoid interpretation of type theory.  In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83–111. Oxford Univ. Press, New York, 1998.
  * [22] J.M.E. Hyland.  The Effective Topos.  In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165 – 216. Elsevier, 1982.  doi:10.1016/S0049-237X(09)70129-6.
  * [23] J.M.E. Hyland.  A small complete category.  Annals of Pure and Applied Logic, 40(2):135 – 165, 1988.  doi:10.1016/0168-0072(88)90018-8.
  * [24] Bart Jacobs.  Comprehension categories and the semantics of type dependency.  Theoretical Computer Science, 107(2):169 – 207, 1993.  doi:10.1016/0304-3975(93)90169-T.
  * [25] Bart Jacobs.  Categorical Logic and Type Theory.  Elsevier Science, 1st edition, 1999.
  * [26] Chris Kapulkin and Peter LeFanu Lumsdaine.  The Simplicial Model of Univalent Foundations (after Voevodsky), 2018\.  arXiv:1211.2851v5.
  * [27] Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters.  Internal Universes in Models of Homotopy Type Theory.  In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  doi:10.4230/LIPIcs.FSCD.2018.22.
  * [28] Giuseppe Longo and Eugenio Moggi.  Constructive natural deduction and its “$\omega$-set” interpretation.  Mathematical Structures in Computer Science, 1(2):215–254, 1991\.  doi:10.1017/S0960129500001298.
  * [29] Per Martin-Löf.  An Intuitionistic Theory of Types: Predicative Part.  Studies in Logic and the Foundations of Mathematics, 80:73 – 118, 1975.  doi:10.1016/S0049-237X(08)71945-1.
  * [30] Ian Orton and Andrew M. Pitts.  Axioms for Modelling Cubical Type Theory in a Topos.  In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1–24:19, Dagstuhl, Germany, 2016. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  doi:10.4230/LIPIcs.CSL.2016.24.
  * [31] Ian Orton and Andrew M. Pitts.  Axioms for Modelling Cubical Type Theory in a Topos.  Logical Methods in Computer Science, 14, Dec 2018.  doi:10.23638/LMCS-14(4:23)2018.
  * [32] Wesley Phoa.  An introduction to fibrations, topos theory, the effective topos and modest sets.  Technical Report ECS-LFCS-92-208, The University of Edinburgh, 2006.  URL: http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/.
  * [33] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  http://homotopytypetheory.org/book/, Institute for Advanced Study, 2013.
  * [34] Christian Sattler.  The Equivalence Extension Property and Model Structures, 2017.  arXiv:1704.06911v4.
  * [35] Michael Shulman.  Higher Inductive Types via Impredicative Polymorphism, 2011.  URL: https://homotopytypetheory.org/2011/04/25/higher-inductive-types-via-impredicative-polymorphism/.
  * [36] Sam Speight.  Impredicative Encodings of Inductive Types in Homotopy Type Theory.  Master’s thesis, Carnegie Mellon University, 2017.  URL: http://www.cs.ox.ac.uk/people/sam.speight/publications/sams-hott-thesis.pdf.
  * [37] Bas Spitters.  Cubical sets and the topological topos, 2016.  arXiv:1610.05270v1.
  * [38] Wouter Pieter Stekelenburg.  Constructive Simplicial Homotopy, 2016.  arXiv:1604.04746v1.
  * [39] Andrew W. Swan.  An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof.  Journal of Logic & Analysis, 8:1–35, 2016.  doi:10.4115/jla.2016.8.1.
  * [40] Andrew W. Swan.  Lifting Problems in Grothendieck Fibrations, 2018.  arXiv:1802.06718v1.
  * [41] Andrew W. Swan.  $W$-Types with Reductions and the Small Object Argument, 2018.  arXiv:1802.07588v1.
  * [42] Andrew W. Swan and Taichi Uemura.  On Church’s Thesis in Cubical Assemblies, 2019.  arXiv:1905.03014v1.
  * [43] Benno van den Berg.  Univalent polymorphism, 2018.  arXiv:1803.10113v2.
  * [44] Jaap van Oosten.  Realizability: An Introduction to Its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics.  Elsevier Science, San Diego, USA, 2008.
  * [45] Vladimir Voevodsky.  A universe polymorphic type system, 2012.  URL: https://ncatlab.org/ufias2012/files/Universe+polymorphic+type+sytem.pdf.

##  Appendix A Details of Composition for Gluing and Universe

We give explicit definitions of composition operations for gluing and
universes described in Section 3.4.

Before that, we introduce some notations. for a fibration
$\Gamma,i:\mathbb{I}\vdash A(i)$, one can derive the _composition operation_
Γ⊢e : 2
Γ⊢φ: Cof
Γ, i : I⊢f(i) : φ→A(i)
Γ⊢a : A(e)
Γ, u : φ⊢f(e)u = a Γ⊢comp_e^i(A(i), f(i), a) : A(¯e) such that
$\Gamma,u:\varphi\vdash f(\bar{e})u=\mathsf{comp}_{e}^{i}(A(i),f(i),a)$.
Concretely, for a fibration structure $\alpha:\mathsf{Fib}(A)$, we define

$\gamma:\Gamma\vdash\mathsf{comp}_{e}^{i}(A(i),f(i),a):=\alpha(\lambda
i.(\gamma,i),e,\varphi,\lambda ui.f(i)u,a).$

In the notation $\mathsf{comp}_{e}^{i}(A(i),f(i),a)$, the variable $i$ is
considered to be bound. Usually we use the composition operation in the form
of

$\mathsf{comp}_{e}^{i}(A(i),[(u_{1}:\varphi_{1})\mapsto
g_{1}(u_{1},i),\dots,(u_{n}:\varphi_{n})\mapsto g_{n}(u_{n},i)],a)$

with a system $[(u_{1}:\varphi_{1})\mapsto
g_{1}(u_{1},i),\dots,(u_{n}:\varphi_{n})\mapsto
g_{n}(u_{n},i)]:\varphi_{1}\lor\dots\lor\varphi_{n}\to A(i)$.

###  A.1 Some Derived Notions and Operations

We recall some notions and operations derivable in cubical type theory without
gluing and universes.

Composition operations are preserved by function application [10, Section
5.2]: one can derive an operation Γ, i : I⊢h(i) : A(i) →B(i)
Γ⊢e : 2
Γ⊢φ: Cof
Γ, i : I⊢f(i) : φ→A(i)
Γ⊢a : A(e)
Γ, u : φ⊢f(e)u = a Γ⊢pres_e^i(h(i), f(i), a) : Path(B(¯e), c_1, c_2) such that
$\Gamma,u:\varphi,j:\mathbb{I}\vdash
h(\bar{e})(f(\bar{e})u)=\mathsf{pres}_{e}^{i}(h(i),f(i),a)j$, where
$c_{1}=\mathsf{comp}_{e}^{i}(B(i),h(i)\circ f(i),h(e)a)$ and
$c_{2}=h(\bar{e})(\mathsf{comp}_{e}^{i}(A(i),f(i),a))$.

Equivalences are characterized by a kind of extension property [10, Section
5.3]: for fibrations $\Gamma\vdash A$ and $\Gamma\vdash B$, one can derive an
operation Γ⊢f : A ≃B
Γ⊢e : 2
Γ⊢φ: Cof
Γ⊢b : B
Γ⊢p : φ→∑_a : APath(B, b, fa) Γ⊢equiv(f, p, b) : ∑_a : APath(B, b, fa) such
that $\Gamma,u:\varphi\vdash pu=\mathsf{equiv}(f,p,b)$.

For a fibration $\Gamma,i:\mathbb{I}\vdash A(i)$, we define a function called
_transport_ $\Gamma,e:\mathbf{2}\vdash\mathsf{tp}_{e}^{i}(A(i)):A(e)\to
A(\bar{e})$ to be
$\mathsf{tp}_{e}^{i}(A(i))a=\mathsf{comp}_{e}^{i}(A(i),[],a)$. This function
$\mathsf{tp}_{e}^{i}(A(i))$ is an equivalence [10, Section 7.1].

###  A.2 Gluing

######  Proof A.1 (Proof of Proposition 3.11).

Let $p:\mathbb{I}\to\Gamma$, $e:\mathbf{2}$, $\psi:\mathsf{Cof}$,
$g:\psi\to\prod_{i:\mathbb{I}}\prod_{u:\varphi(pi)}A(u)$,
$h:\psi\to\prod_{i:\mathbb{I}}B(pi)$, $a:\prod_{u:\varphi(pe)}A(u)$ and
$b:B(pe)$, and suppose
$\forall_{v:\psi}\forall_{i:\mathbb{I}}\forall_{u:\varphi(pi)}f(u)(gviu)=hvi$,
$\forall_{u:\varphi(pe)}f(u)(au)=b$ and $\forall_{v:\psi}gve=a\land hve=b$. We
have to find elements $\bar{a}:\prod_{u:\varphi(p\bar{e})}A(u)$ and
$\bar{b}:B(p\bar{e})$ such that
$\forall_{u:\varphi(p\bar{e})}f(u)(\bar{a}u)=\bar{b}$ and
$\forall_{v:\psi}gv\bar{e}=\bar{a}\land hv\bar{e}=\bar{b}$. We define

$\displaystyle\bar{b}_{1}$
$\displaystyle:=\mathsf{comp}_{e}^{i}(B(pi),[(v:\psi)\mapsto
hvi],b):B(p\bar{e})$ $\displaystyle\delta$
$\displaystyle:=\forall_{i:\mathbb{I}}\varphi(pi):\mathsf{Cof}$
$\displaystyle\bar{a}_{1}$ $\displaystyle:=\lambda
w.\mathsf{comp}_{e}^{i}(A(wi),[(v:\psi)\mapsto
gvi(wi)],a(we)):\prod_{w:\delta}A(w\bar{e})$ $\displaystyle q$
$\displaystyle:\prod_{w:\delta}\mathsf{Path}(\bar{b}_{1},f(w\bar{e})(\bar{a}_{1}w))$
$\displaystyle qw$
$\displaystyle:=\mathsf{pres}_{e}^{i}(f(wi),[(v:\psi)\mapsto gvi(wi)],a(we))$
$\displaystyle\bar{a}$ $\displaystyle:\prod_{u:\varphi(p\bar{e})}A(u)$
$\displaystyle q_{2}$
$\displaystyle:\prod_{u:\varphi(p\bar{e})}\mathsf{Path}(\bar{b}_{1},f(u)(\bar{a}u))$
$\displaystyle(\bar{a}u,q_{2}u)$
$\displaystyle:=\mathsf{equiv}(f(u),[(w:\delta)\mapsto(\bar{a}_{1}w,qw),(v:\psi)\mapsto(gv\bar{e}u,\lambda
i.\bar{b}_{1})],\bar{b}_{1})$ $\displaystyle\bar{b}$
$\displaystyle:=\mathsf{comp}_{0}^{i}(B(p\bar{e}),[(u:\varphi(p\bar{e}))\mapsto
q_{2}ui,(v:\psi)\mapsto hv\bar{e}],\bar{b}_{1}):B(p\bar{e})$

Then one can derive that $\bar{b}=q_{2}u1=f(u)(\bar{a}u)$ for
$u:\varphi(p\bar{e})$ and that $\bar{a}=gv\bar{e}$ and $\bar{b}=hv\bar{e}$ for
$v:\psi$. Moreover, for every $w:\prod_{i:\mathbb{I}}\varphi(pi)$, we have
$\bar{a}(w\bar{e})=\bar{a}_{1}w=\mathsf{comp}_{e}^{i}(A(wi),[(v:\psi)\mapsto
gvi(wi)],a(we))$ which means the preservation of fibration structure by the
function $\Gamma,u:\varphi\vdash\lambda(a,b).au:\mathsf{Glue}(\varphi,f)\to
A(u)$.

###  A.3 Universes

######  Proof A.2 (Proof of Proposition 3.13).

Let $e:\mathbf{2}$, $\varphi:\mathsf{Cof}$,
$f:\varphi\to\mathbb{I}\to\mathcal{U}^{F}$ and $B:\mathcal{U}^{F}$ such that
$\forall_{u:\varphi}fue=B$. We have to find a $\bar{B}:\mathcal{U}^{F}$ such
that $\forall_{u:\varphi}fu\bar{e}=\bar{B}$. Let $A:=\lambda
u.fu\bar{e}:\varphi\to\mathcal{U}^{F}$. We have an equivalence $g:=\lambda
u.\mathsf{tp}_{\bar{e}}^{i}(fui):\prod_{u:\varphi}Au\simeq B$. Let
$\bar{B}:=\mathsf{SGlue}(\varphi,g):\mathcal{U}^{F}$, then
$\forall_{u:\varphi}fu\bar{e}=Au=\bar{B}$.