# Constructive Sheaf Models of Type Theory

Thierry Coquand, Fabian Ruch, and Christian Sattler

(Computer Science Department, University of Gothenburg)

## Introduction

Despite being relatively recent, the notion of (pre)sheaf model has a rich and
intricate history which mixes different intuitions coming from topology, logic
and algebra. Eilenberg and Zilber [14] used a presheaf model (simplicial sets)
to represent geometrical objects, and the intuition is geometrical: we think
of the objects $I,J,\dots$ of the base category as basic “shapes”; a presheaf
$A$ is then given by a family of sets $A(I)$ of objects of each shape $I$,
which are related by the restriction maps $A(I)\rightarrow A(J)$. A little
later, but independently, Beth [7] and Kripke [20] used a sheaf and a presheaf
model over trees, respectively, to provide a formal semantics for
intuitionistic logic. Their motivations were logical, and the intuition is of
a temporal nature instead: we think of the objects of the node of the tree as
“stages of knowledge” and of the ordering as “increase in knowledge”. Scott
[27] described a presheaf model of higher-order logic and pointed out the
potential interest for the semantics of -calculus. This was refined by Martin
Hofmann [16] who provided a presheaf model of dependent type theory with
universes. Hofmann’s presheaf model was subsequently used in an essential way
in works on constructive semantics of type theory with univalent universes [9,
10, 22].

The generalization of such presheaf models of dependent type theory, and
especially of universes, to a sheaf model semantics is however non-trivial.
The problem in generalising this semantics for universes comes essentially
from the fact that the collection of sheaves does not form a sheaf in any
natural way: if we are given locally sheaves that are compatible, one can
patch them together but not in a unique way, only unique up to isomorphism.
This problem was the motivation for the introduction of stacks and a more
subtle notion of patching of sheaves (cf. [15, Section 3.3]), and in general
patching of mathematical structures. The generalization of this to patching of
higher structures was the content of the first part of Joyal’s letter to
Grothendieck [17]. One contribution of the present paper is to provide a
constructive version of this notion111Joyal’s argument was using non-
constructive reasoning in simplicial sets and then Barr’s theorem (see [5]).
The present paper can be developed directly in the constructive framework of
CZF with universes introduced by Aczel [1]. by describing a sheaf model
semantics of type theory with univalence [35, 34]. This uses in a crucial way
the fact that we have a constructive interpretation of univalence as in [9,
22], which can be relativized to any presheaf model. The main point is then
that the operation sending an object to its object of descent data (a
compatible collection of elements of its restrictions) defines a left exact
modality (see [34, 23, 24]), which can then be used to build internally models
of univalent type theory [23].

This work opens the possibility of generalising works of sheaf models of
intuitionistic logic as in [33] to sheaf models of univalent type theory. It
extends the previous work in [11] to a complete model of univalence, and has
no restrictions for representing (higher) data types. We give only one
application (independence of countable choice), but we expect for instance
that results such as in [21] can be generalized as well, and that we can give
a constructive account of works such as in [30, 37]. The present semantics (in
a preliminary version) has already been used by Weaver and Licata [36] for
building a constructive model of directed univalence.

This paper is organized as follow. We first introduce the notion of lex
operation as an operation acting on types and families of types. A descent
data operation is then a lex operation which defines a left exact modality
[34, 23, 24]. These two notions are formulated purely syntactically in the
framework of type theory. We show next how to instantiate these operations for
cubical presheaves. In this setting, we can understand the notion of being
modal for a descent data operation as a generalization of the sheaf condition,
where the compatibility requirements are expressed up to path equality instead
of being expressed as strict equalities. We then provide some examples and the
application to the unprovability of countable choice. In an appendix we
explain how some of our results about descent data operations can be
generalized to accessible left exact modalities.

##  1 Abstract notion of descent data

In this article, we take terminology in type theory with potentially both
strict and homotopical meaning to have the strict meaning by default. For
example, equality (denoted by the symbol ${=}$) refers to the strict equality
(as opposed to identity or path types), isomorphisms refer to strictly
invertible maps, and pullbacks refer to strict pullbacks.

We use the following notations. We write $\mathbf{1}$ for the unit type and
$():\mathbf{1}$ for its unique element. Given a type $A$ and a family $B$ of
types over $A$, we write $\sum_{A}B$ for their sum type and $\prod_{A}B$ for
their product type. The pairing operation is denoted by $(a,b):\sum_{A}B$ for
$a:A$ and $b:B\,a$. The projection maps are denoted by $\pi_{1}$ and
$\pi_{2}$. We write $\mathsf{id}_{A}$ for the identity function on $A$ and
$g\circ f$ for the composition of $f\colon A\to B$ and $g\colon B\to C$. If
$B$ is a family of types over $A$ and $f\colon A^{\prime}\rightarrow A$, we
also write $B\circ f$ for the family of types over $A^{\prime}$ obtained from
$B$ by reindexing along $f$.

###  1.1 Lex operation

The concept of lex operations is defined for a dependent type theory with only
unit type, dependent sums, dependent product and universes. In particular,
path types are not needed. Intuitively, a lex operation is an endofunctor on
the category of types and functions (compatible with substitution) which
preserves the unit type and dependent projections of sum types up to
isomorphism.

A lex operation222The notion of lex operation appears implicitly in a natural
way when describing the rules of inductive data types [12]. If we have a
family $D_{a}$ of lex operations indexed over $a:A$, we can consider the
inductive type $T$ with constructor
$\mathsf{sup}:\prod_{a:A}(D_{a}T\rightarrow T)$ and elimination rule
$\mathsf{rec}\,f:\prod_{T}P$ for
$f:\prod_{a:A}\prod_{u:D_{a}T}(\tilde{D}_{a}P\,u\rightarrow
P(\mathsf{sup}_{a}\,u))$. We can then write the computation rule
$\mathsf{rec}\,f\,(\mathsf{sup}_{a}\,u)=f_{a}\,u\,(\tilde{D}_{a}(\mathsf{rec}\,f)\,u)$
For justifying the use of such inductive definitions, we need some
“accessibility” assumption on the functor $D$, which will be satisfied in the
examples. In the special case where $D_{a}X$ is $X^{Ba}$ for $B$ a family of
over $A$ we recover the $W$-type $W_{A}B$. is given by an operation $D$ on
types and functions forming a functor: we have $Df:DA\rightarrow DB$ if
$f:A\rightarrow B$ with $D(g\circ f)=Dg\circ Df$ and
$D(\mathsf{id}_{A})=\mathsf{id}_{DA}$.

The operation $D$ should also preserve the unit type $\mathbf{1}$ up to
isomorphism. Specifically we have an element $\langle\rangle$ in $D\mathbf{1}$
and $x=\langle\rangle$ if $x$ is in $D\mathbf{1}$.

Furthermore, $D$ should preserve dependent projections of sum types up to
isomorphism. We assert this by an operation on families of types: $\tilde{D}B$
is family of types over $DA$ if $B$ is a family of types over $A$. This should
be natural in $A$ together with operations ensuring that $D(\sum_{A}B)$ is
naturally isomorphic to $\sum_{DA}{\tilde{D}B}$ over $DA$. Naturality in $A$
means $\tilde{D}(B\circ f)=\tilde{D}B\circ
Df:D{A^{\prime}}\rightarrow\mathcal{U}$ for $f:A^{\prime}\rightarrow A$. The
natural isomorphism between $D(\sum_{A}B)$ and $\sum_{DA}{\tilde{D}B}$ over
$DA$ is given by an operation $\tilde{D}s:\prod_{DA}{\tilde{D}B}$ on sections
$s:\prod_{A}B$ satisfying $\tilde{D}(s\circ f)=\tilde{D}s\circ
Df:\prod_{D{A^{\prime}}}\tilde{D}(B\circ f)$ and a pairing operation $\langle
u,v\rangle:D(\sum_{A}B)$ for elements $u:DA$ and $v:(\tilde{D}B)\,u$
satisfying

$\displaystyle(D\pi_{1})\langle u,v\rangle$ $\displaystyle=u$
$\displaystyle(\tilde{D}\pi_{2})\langle u,v\rangle$ $\displaystyle=v$
$\displaystyle\langle(D\pi_{1})\,w,(\tilde{D}\pi_{2})\,w\rangle$
$\displaystyle=w$

where $w:D(\sum_{A}B)$.

We also assume that universes reflect these operations. This means we have
$DA:\mathcal{U}$ if $A:\mathcal{U}$ and $\tilde{D}B:DA\rightarrow\mathcal{U}$
if $B:A\rightarrow\mathcal{U}$ and $A$ a type (crucially, $A$ need not be in
$\mathcal{U}$ here).

The canonical example of a lex operation is exponentiation with a fixed type
$R$ (assumed to be in all universes). We define $DA=A^{R}$,
$(\tilde{D}B)u=\prod_{x:R}\,B(u\,x)$, and
$(\tilde{D}s)u=\lambda_{x:R}\,s(u\,x)$. The pairing is given by $\langle
u,v\rangle=\lambda_{x:R}\,(u\,x,v\,x)$.

######  Remark 1.1.

Let $\mathcal{U}$ be a universe. The action of the operation $\tilde{D}$ on
$\mathcal{U}$-small families is uniquely determined by the universal case
$L=\tilde{D}\,\mathsf{id}_{\mathcal{U}}:D\mathcal{U}\to\mathcal{U}$: we have
(and can define) $\tilde{D}B=L\circ DB$ with $DB:DA\rightarrow D\mathcal{U}$
for $B:A\rightarrow\mathcal{U}$. This corresponds to the “escaping” function
in Section 2.5 of [26]. We can thus describe the action of $\tilde{D}$ on
$\mathcal{U}$-small families and associated operations by requiring that $D$
applied to the “universal $\mathcal{U}$-small fibration”
$\sum_{X:\mathcal{U}}X\to\mathcal{U}$ is isomorphic to a “$\mathcal{U}$-small
fibration” (a projection of a type in $\mathcal{U}$), and that $D$ preserves
pullbacks of this map.

######  Proposition 1.2.

Any lex operation $D$ is uniquely pointed.333We owe this observation to Dan
Licata.

###### Proof.

We define $\eta_{A}\,a=(D\epsilon_{a})\,\langle\rangle$ with
$\epsilon_{a}=\lambda_{x:\mathbf{1}}\,a$. We then have for $f:A\rightarrow B$

$(Df)(\eta_{A}\,a)=(Df\circ
D\epsilon_{a})\,\langle\rangle=(D\epsilon_{f\,a})\,\langle\rangle=\eta_{B}(f\,a)$

Note furthermore that this natural transformation $\eta_{A}$ is uniquely
determined, since we should have $\eta_{\mathbf{1}}\,()=\langle\rangle$ and so
$\eta_{A}\,a=\eta_{A}(\epsilon_{a}\,())=(D\epsilon_{a})(\eta_{\mathbf{1}}\,())=(D\epsilon_{a})\,\langle\rangle$.
∎

######  Remark 1.3.

For $T:\mathcal{U}$, the map
$(\tilde{D}\epsilon_{T})\,\langle\rangle\rightarrow\sum_{D\mathbf{1}}\tilde{D}\epsilon_{T}\rightarrow
D(\sum_{\mathbf{1}}\epsilon_{T})\rightarrow DT$ is an isomorphism, as a
composition of isomorphisms. As a consequence, the map

$(\tilde{D}B)(\eta_{A}\,a)\longrightarrow D(B\,a)\qquad
v\longmapsto(D\pi_{2})\langle\langle\rangle,v\rangle$

is an isomorphism for a type $A$, a family $B$ over $A$, and $a:A$.

Note that $\eta_{A}\,a=\lambda_{x:R}\,a$ for the example $DA=A^{R}$ where the
lex operation is exponentiation. The isomorphisms of Remark 1.3 are identities
in this example.444This assumes that function types are implemented via
dependent products. In fact, this will happen for all the example lex
operations we will consider in this article.

######  Remark 1.4.

Recall our assumption that universes reflect the operation $D$ on types and
the operation $\tilde{D}$ on families. Remark 1.3 shows that only the
reflection of $\tilde{D}$ is essential. If $D$ is not reflected, we can define
an isomorphic operation $D^{\prime}A=\tilde{D}(\epsilon_{A})\,\langle\rangle$
on types that is reflected. The remaining structure of $D$ transports across
the isomorphism to define a lex operation $D^{\prime}$.

######  Remark 1.5.

Let $\mathcal{E}$ be a category with families [13] modelling our type theory.
A lex operation in $\mathcal{E}$ can be defined from a pseudomorphism of cwfs
with universes [18] from $\mathcal{E}$ to itself that is pointed as an
endofunctor. When working externally with a model, this is a convenient way of
constructing a lex operation in it. Note that the given pointing is then
reconstructed by Proposition 1.2.

######  Remark 1.6.

For readers familiar with Martin Hofmann’s semantic methodology [16], we note
a concise description of lex operations expressed internally in presheaves
over the category of contexts. The object Type of types has the structure of a
cwf with universes (context extension is given by sum types). Up to the
discussion of Remark 1.4, a lex operation is a pseudomorphism of cwfs with
universes from Type to itself. This definition can be written in the language
of two-level type theory [3].

###  1.2 $D$-modal types

The notion of lex operation is defined at the level of “pure” dependent type
theory, without assuming any notion of path types. In presence of path types,
we automatically have the following preservation property.

######  Theorem 1.7.

Let $D$ be a lex operation. Then $D$ preserves equivalences.

###### Proof.

Note that if $f_{0}$ and $f_{1}$ are path equal then so are $Df_{0}$ and
$Df_{1}$ by path induction. It follows that if $f$ and $g$ are inverses, then
so are $Df$ and $Dg$. ∎

Avigad et al. [4] explain how to build a fibration category from a model of
dependent type theory. Theorem 1.7 implies that any lex operation defines an
endomorphism of the associated fibration category. A lex operation preserves
all finite homotopy limits (e.g., contractible types, homotopy pullbacks,
homotopy equalizers, homotopy fibers, …).

In presence of path types, we can also define the following important notion
of modal types.

######  Definition 1.8.

A type $A$ is called $D$-modal if the unit map $\eta_{A}:A\rightarrow DA$ is
an equivalence.

######  Proposition 1.9.

If $A$ is $D$-modal and $B$ is a family of types over $A$, then $B$ is a
family of $D$-modal types over $A$ if, and only if, $T=\sum_{A}B$ is
$D$-modal.

###### Proof.

Let $f$ be the map $T\rightarrow\sum_{DA}{\tilde{D}B},\
(a,b)\mapsto(\eta_{A}\,a,\eta_{B\,a}\,b)$. Since $\eta_{A}$ is an equivalence,
each map $\eta_{B\,a}$ is an equivalence if, and only if, the map $f$ is an
equivalence [34]. But $f$ is an equivalence if and only if $\eta_{T}$ is an
equivalence. ∎

###  1.3 Abstract notion of descent data

######  Theorem 1.10.

The following conditions are equivalent, for a lex operation $D$

  1. 1.

$D$ defines a modality as axiomatized in [23, 24]

  2. 2.

the map $D\eta_{A}$ is an equivalence, and $D\eta_{A}$ and $\eta_{DA}$ are
path equal

###### Proof.

The first condition implies the second using the results in [23, 24].

Conversely, assume that the map $D\eta_{A}$ is an equivalence, and $D\eta_{A}$
and $\eta_{DA}$ are path equal. Then $\eta_{DA}$ is an equivalence as well and
each type $DA$ is $D$-modal. Proposition 1.9 shows that $D$-modal types are
closed by dependent sum types. We thus only have to prove that the map

$F:(DA\rightarrow B)\longrightarrow(A\rightarrow B)\qquad f\longmapsto
f\circ\eta_{A}$

is an equivalence if $B$ is $D$-modal [23].

Let $p_{B}$ be a map $DB\rightarrow B$ such that $p_{B}\circ\eta_{B}$ is path
equal to $\mathsf{id}_{B}$. We define a map

$G:(A\rightarrow B)\longrightarrow(DA\rightarrow B)\qquad u\longmapsto
p_{B}\circ Du$

We then have $F(Gu)=p_{B}\circ Du\circ\eta_{A}=p_{B}\circ\eta_{B}\circ u$
which is path equal to $u$ and $G(Ff)=p_{B}\circ D(f\circ\eta_{A})=p_{B}\circ
Df\circ D\eta_{A}$ which is path equal to $p_{B}\circ
Df\circ\eta_{DA}=p_{B}\circ\eta_{B}\circ f$ which is path equal to $f$. Hence
$G$ is an inverse to $F$ and $F$ is an equivalence. ∎

######  Definition 1.11.

A descent data operation is a lex operation $D$ satisfying the equivalent
conditions of Theorem 1.10.

Note that the first condition of Theorem 1.10 is a (homotopy) proposition. The
second condition is the one which will be convenient to verify for the main
examples.

We write $\mathsf{isMod}_{D}(A)$ for the type (proposition) expressing that
$A$ is $D$-modal.

###  1.4 Closure properties

Let $D$ be a descent data operation.

######  Lemma 1.12.

For the map $\eta_{A}:A\rightarrow DA$ to be an equivalence, it is enough to
have a patch function $p_{A}:DA\rightarrow A$ such that $p_{A}\circ\eta_{A}$
is path equal to the identity of $A$.

###### Proof.

If $p_{A}$ is such a patch function, we have
$\mathsf{id}_{DA}=D(\mathsf{id}_{A})=D(p_{A}\circ\eta_{A})=Dp_{A}\circ
D\eta_{A}$ which is path equal to $Dp_{A}\circ\eta_{DA}=\eta_{A}\circ p_{A}$.
Hence $p_{A}$ is an inverse of $\eta_{A}$ and $\eta_{A}$ is an equivalence. ∎

######  Lemma 1.13.

For $B$ a family of types over $A$ and any $u:DA$, the type $(\tilde{D}B)\,u$
is $D$-modal.

###### Proof.

Since $D(\sum_{A}B)$ is $D$-modal, so is the isomorphic type
$\sum_{DA}{\tilde{D}B}$. Using Proposition 1.9, we have that $(\tilde{D}B)\,u$
is a $D$-modal type for any $u:DA$. ∎

######  Proposition 1.14.

The type $\mathcal{U}_{D}=\sum_{\mathcal{U}}\mathsf{isMod}_{D}$ is a $D$-modal
type.

###### Proof.

Consider the diagram

$\textstyle{D\mathcal{U}_{D}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tilde{D}\pi_{1}}$$\textstyle{\mathcal{U}_{D}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta}$$\scriptstyle{\pi_{1}}$$\textstyle{\mathcal{U}\hbox
to0.0pt{.\hss}}$

It commutes up to homotopy since $(\tilde{D}\pi_{1})(\eta\,X)$ is isomorphic
to $D(\pi_{1}\,X)$ by Remark 1.3, which is path equal to $\pi_{1}\,X$ for any
$X:\mathcal{U}_{D}$ by univalence(!). Note also that $\pi_{1}$ is an embedding
since $\mathsf{isMod}_{D}$ is a family of propositions.

Since $(\tilde{D}\pi_{1})\,A$ is $D$-modal by Lemma 1.13 for any
$A:D\mathcal{U}_{D}$, the map
$\tilde{D}\pi_{1}:D\mathcal{U}_{D}\rightarrow\mathcal{U}$ factorizes through
$\pi_{1}:\mathcal{U}_{D}\rightarrow\mathcal{U}$ and the corresponding map
$D\mathcal{U}_{D}\rightarrow\mathcal{U}_{D}$ is a left inverse of
$\eta:\mathcal{U}_{D}\rightarrow D\mathcal{U}_{D}$ since $\pi_{1}$ is an
embedding. Hence $\mathcal{U}_{D}$ is $D$-modal by Lemma 1.12. ∎

###  1.5 Model associated to a descent data operation

We can now define an internal translation which provides a new model of
univalent type theory with higher inductive types for any descent data
operation $D$, following the work in [23]. A type $A,p$ of the new model is a
type $A$ together with a proof $p$ that this type is $D$-modal, while an
element of a pair $A,p$ is an element of $A$.

In order to interpret the type of natural numbers with the desired computation
rules (not covered in [23]), we need to use the following higher inductive
type:555To justify the use of such inductive definitions, we need some
accessibility assumption on the functor $D$ that will be satisfied in the
examples.

$\displaystyle\mathsf{zero}$ $\displaystyle:$ $\displaystyle\mathsf{Nat}$
$\displaystyle\mathsf{succ}$ $\displaystyle:$
$\displaystyle\mathsf{Nat}\rightarrow\mathsf{Nat}$
$\displaystyle\mathsf{patch}$ $\displaystyle:$ $\displaystyle
D\,\mathsf{Nat}\rightarrow\mathsf{Nat}$ $\displaystyle\mathsf{linv}$
$\displaystyle:$
$\displaystyle\textstyle\prod_{x:\mathsf{Nat}}\mathsf{patch}(\eta_{\mathsf{Nat}}\,x)=_{\mathsf{Nat}}x$

This is equivalent to the type $DN$ where $N$ is the usual inductive type with
constructors $\mathsf{zero}$ and $\mathsf{succ}$, but the type $DN$ does not
satisfy the required computation rules.

The same idea applies to the interpretation of other inductive types such as
the $W$-type.

It also works for higher inductive types. For instance the suspension of a
type $A$ will be defined as

$\displaystyle\mathsf{north},\mathsf{south}$ $\displaystyle:$ $\displaystyle
T$ $\displaystyle\mathsf{merid}$ $\displaystyle:$
$\displaystyle{A}\rightarrow\mathsf{north}=_{T}\mathsf{south}$
$\displaystyle\mathsf{patch}$ $\displaystyle:$ $\displaystyle DT\rightarrow T$
$\displaystyle\mathsf{linv}$ $\displaystyle:$
$\displaystyle\textstyle\prod_{z:T}\mathsf{patch}(\eta_{T}\,z)=_{T}z$

Note that having $D$ defined as a strict functor is essential for such
definitions.

###  1.6 Generalization to a family of descent data operations

More generally, if we have a family of descent data operations $D_{S}$ indexed
by a given type $S:\mathsf{C}$, with corresponding maps
$\eta^{S}_{A}:A\rightarrow D_{S}A$, we can consider
$\mathsf{isMod}_{\mathsf{C}}(A)$ to be the proposition
$\prod_{S:\mathsf{C}}\mathsf{isMod}_{D_{S}}(A)$ and $\mathcal{U}(\mathsf{C})$
which is $\sum_{\mathcal{U}}\mathsf{isMod}_{\mathsf{C}}$. We use the slightly
shorter notation $\mathcal{U}_{S}$ to denote the previously defined type
$\mathcal{U}_{D_{S}}=\sum_{\mathcal{U}}\mathsf{isMod}_{D_{S}}$

We let the preorder $D_{1}\leqslant D_{2}$ on descent data operations mean
that any $D_{1}$-modal type is $D_{2}$-modal. We say that $\mathsf{C}$ is
filtered if we have $\exists_{S:\mathsf{C}}.\,D_{S}\leqslant D_{S_{1}}\wedge
D_{S}\leqslant D_{S_{2}}$ for any $S_{1},S_{2}:\mathsf{C}$.666Existence is
defined as the propositional truncation of the dependent sum type [34].

######  Theorem 1.15.

If $\mathsf{C}$ is filtered then $\mathcal{U}(\mathsf{C})$ satisfies
$\mathsf{isMod}_{\mathsf{C}}$.

###### Proof.

For any $D_{S}\leqslant D_{S_{1}}$ in $\mathsf{C}$, $\mathcal{U}_{S}$ is
$D_{S}$-modal by Proposition 1.14 and so $D_{S_{1}}$-modal, and hence
$\eta^{S_{1}}:\mathcal{U}_{S}\rightarrow D_{S_{1}}\mathcal{U}_{S}$ has an
inverse. It follows that the map
$\tilde{D}_{S_{1}}\pi_{1}:D_{S_{1}}\mathcal{U}_{\mathsf{C}}\rightarrow\mathcal{U}$
factorizes through $\mathcal{U}_{S}\rightarrow\mathcal{U}$ and hence that for
any $A:D_{S_{1}}\mathcal{U}_{\mathsf{C}}$ the type
$(\tilde{D}_{S_{1}}\pi_{1})\,A$ is $D_{S}$-modal.

If $\mathsf{C}$ is filtered, this implies that the type
$(\tilde{D}_{S_{1}}\pi_{1})\,A$ is $D_{S_{2}}$-modal for any $S_{2}$ in
$\mathsf{C}$. Hence the map
$\tilde{D}_{S_{1}}\pi_{1}:D_{S_{1}}\mathcal{U}_{\mathsf{C}}\rightarrow\mathcal{U}$
factorizes through $\mathcal{U}_{\mathsf{C}}\rightarrow\mathcal{U}$ and the
corresponding map
$\tilde{D}_{S_{1}}\mathcal{U}_{\mathsf{C}}\rightarrow\mathcal{U}_{\mathsf{C}}$
is a left inverse of $\mathcal{U}_{\mathsf{C}}\rightarrow
D_{S_{1}}\mathcal{U}_{\mathsf{C}}$. Hence $\mathcal{U}(\mathsf{C})$ is
$D_{S_{1}}$-modal for any $S_{1}$ in $\mathsf{C}$ by Lemma 1.12. ∎

This shows that for a family of descent data operations satisfying the
hypothesis of Theorem 1.15, we still get a model of univalent type theory
(with higher inductive types), interpreting a type as a type together with a
proof that this type is modal for each descent data operation. Of all type
formers, only the universe has to deal with interaction between the elements
of the given family of descent data operations.

###  1.7 Example

If $R$ is a proposition, then for the lex operation defined by $DA=A^{R}$ the
two maps $D\eta_{A}$ and $\eta_{DA}$ are path equal equivalences and hence
exponentiation defines a descent data operation in that case.

The next Section will define a new kind of descent data operation for any
presheaf model.

##  2 Cubical presheaf models

###  2.1 Cubical models

Cubical models are presheaf models of univalent type theory specified by two
parameters, an _interval object_ $\mathbb{I}$ and a _cofibration classifier_
$\Phi$. Formally, we say that a _cubical model_ is a presheaf category with
the following structure, as in Orton and Pitts [22].

  * •

The interval object $\mathbb{I}$ is connected and has distinct points $0$ and
$1$. Exponentiation with $\mathbb{I}$ has a right adjoint. We also assume that
$\mathbb{I}$ has the structure of a bounded distributive lattice.777This
assumption simplifies one of our arguments (Proposition 3.9). However, our
results also apply to the Cartesian variation of cubical models of Angiuli et
al. [2]). There, one removes this hypothesis and instead adds that the
diagonal $\mathbb{I}\to\mathbb{I}\times\mathbb{I}$ is a cofibration.

  * •

The universal cofibration $\top\colon 1\to\Phi$ is a levelwise decidable
inclusion. In the internal language of presheaves, we will work with $\Phi$ as
a universe of certain propositions and leave the decoding function (given by
equality with $\top:\Phi$) implicit. Isomorphic cofibrations are equal.888This
assumption is not strictly speaking necessary, but simplifies the theory. The
interval endpoint inclusions $0,1\colon 1\to\mathbb{I}$ are cofibrations.
Cofibrations are closed under finite union (finite disjunction), composition
(dependent conjunction), and universal quantification over $\mathbb{I}$.

It is then known, following the work in [9, 22, 10], how to define a model of
univalent type theory with higher inductive types.

###  2.2 Presheaves in cubical models

For the remainder of this Section, we fix a cubical model given by presheaves
over a small category $\mathcal{B}$. We refer to this as the _base model_ (for
example, it can be cubical sets). We write $I,J,K,\dots$ for the objects of
$\mathcal{B}$. We have the interval object by $\mathbb{I}_{\mathcal{B}}$ and
the cofibration classifier $\Phi_{\mathcal{B}}$.

Let ${\mathcal{C}}$ be another small category. We write $X,Y,Z,\dots$ for its
objects. We describe possibilities for turning presheaves over
${\mathcal{C}}\times\mathcal{B}$ into a cubical model. For the interval object
$\mathbb{I}$, we simply take $\mathbb{I}(X,I)=\mathbb{I}_{\mathcal{B}}(I)$.
For the cofibration classifier, we have two reasonable options:

  1. 1.

The first example is simply to take $\Phi(X,I)=\Phi_{\mathcal{B}}(I)$.

  2. 2.

The second example is to define an element $\psi$ of $\Phi_{\mathsf{lw}}(X,I)$
to be a family $\psi_{f}$ in $\Phi_{\mathcal{B}}(I)$ for $f\colon Y\rightarrow
X$ such that $\psi_{f}\leqslant\psi_{g}$ if furthermore $g\colon Z\rightarrow
Y$. We then define the restriction operation $\psi(f,l)$ to be the family
$\psi(f,l)_{g}=\psi_{fg}l$ for $f\colon Y\rightarrow X$ and $g\colon
Z\rightarrow Y$.

The motivation for the second example is that if $\Phi_{\mathcal{B}}(I)$ is
the collection of (decidable) sieves on $I$, then $\Phi_{\mathsf{lw}}(X,I)$
becomes the collection of (decidable) sieves on $(X,I)$.999Classically, this
corresponds to having all monomorphisms as cofibrations.

The interval object $\mathbb{I}$ and any of the choices $\Phi$ and
$\Phi_{\mathsf{lw}}$ fit all the requirements listed in Subsection 2.1. This
turns presheaves over ${\mathcal{C}}\times\mathcal{B}$ into a cubical model.
In particular, we get a model of univalent type theory (and higher inductive
types). We are going to analyse the model obtained using the choice $\Phi$ for
the cofibration classifier and then indicate how to adapt these results for
$\Phi_{\mathsf{lw}}$.

In this model, a context $\Gamma$ is interpreted by a presheaf over
${\mathcal{C}}\times\mathcal{B}$ so a family of sets $\Gamma(X,I)$ with
suitable restriction maps $\rho\mapsto\rho(f,l)$ with $f:Y\rightarrow X$ in
${\mathcal{C}}$ and $l:J\rightarrow I$ in $\mathcal{B}$.

A dependent type $A$ over $\Gamma$ is then given by a presheaf over the
category of elements of $\Gamma$: for any $\rho$ in $\Gamma(X,I)$ we have a
set $A\rho$ with suitable restriction maps $A\rho\rightarrow A\rho(f,l)$
denoted by $u\mapsto u(f,l)$ together with a filling operation (see [9, 22]).
We write $\hbox{\sf Type}(\Gamma)$ for the collection of all types with a
composition operation over $\Gamma$. The set ${\sf Elem}(\Gamma,A)$ is then
the set of sections: a family $a\rho$ in $A\rho$ such that
$(a\rho)(f,l)=a(\rho(f,l))$ for any $\rho$ in $\Gamma(X,I)$ and $f,l$ map of
codomain $X,I$.

Given a constructive Grothendieck universe $U$ (see [1]) containing
$\mathcal{B}$ and ${\mathcal{C}}$, we write $\hbox{\sf Type}_{U}(\Gamma)$ for
the set of $U$-types, such that each set $A\rho$ is in $U$. The presheaf
$\hbox{\sf Type}_{U}$ is then represented by a fibrant type $\mathcal{U}$,
which is univalent [9].

###  2.3 Internal language description

This was an external description of the presheaf model. It is also possible to
describe this model using the internal logic of the presheaf topos over
${\mathcal{C}}\times\mathcal{B}$ as in [22, 10] but also using the internal
logic of the presheaf topos over $\mathcal{B}$. We will use both descriptions.

In the internal logic of the presheaf topos over $\mathcal{B}$, a context of
the presheaf model over ${\mathcal{C}}$ is interpreted as a family of “spaces”
$\Gamma(X)$ with restriction maps $\rho\mapsto\rho f$ for $f:Y\rightarrow X$.
(Each space $\Gamma(X)$ is itself a presheaf over $\mathcal{B}$ with
$\Gamma(X)(I)=\Gamma(X,I)$.) A dependent type $A$ over $\Gamma$ is given by a
family of spaces $A\rho$ for $\rho$ in $\Gamma(X)$ with restriction maps
$u\mapsto uf$. The presheaf $\Phi$ of cofibration is the constant presheaf
$\Phi(X)=\Phi_{\mathcal{B}}$. The interval $\mathbb{I}$ is the constant
interval $\mathbb{I}(X)=\mathbb{I}_{\mathcal{B}}$.

It will be convenient to introduce the following notation: if $\gamma$ is an
element of $\Gamma(X)^{\mathbb{I}}$ and $f:Y\rightarrow X$, we write $\gamma
f^{+}$ in $\Gamma(Y)^{\mathbb{I}}$ for $\lambda_{i}\,\gamma(i)f$. Similarly if
$u(i)$ is a section in $A\gamma(i)$ we write $uf^{+}$ for
$\lambda_{i}\,u(i)f$.

A filling operation (see [22, 10]) for $A$ is given by an operation $c_{A}$
which takes as argument $\gamma$ in $\Gamma(X)^{\mathbb{I}_{\mathcal{B}}}$ and
$\psi$ in $\Phi(X)=\Phi_{\mathcal{B}}$ and a family of elements $u(i)$ in
$A\gamma(i)f$ on the extent $\psi\vee i=0$. (There is a dual operation with
$i=1$ instead.) It produces an element $c_{A}(X,\gamma,\psi,u)(i)$ in
$A\gamma(i)$ such that

  1. 1.

$c_{A}(X,\gamma,\psi,u)(i)=u(i)$ on $\psi\vee i=0$,

  2. 2.

$c_{A}(X,\gamma,\psi,u)(i)f=c_{A}(Y,\gamma f^{+},\psi,uf^{+})(i)$ for
$f:Y\rightarrow X$.

Given such an operation, we also call $A$ _fibrant_ (note this is structure
rather than property).

If $A$ is a type over $\Gamma$, we get a family of dependent types $A(X)$ over
$\Gamma(X)$, each of them having a filling operation, but furthermore these
filling operations commute with the restriction maps.

Similarly an extension operation for $A$, witnessing that $A$ is contractible
(see [9]), is given by an operation $e_{A}$ which takes as argument $\rho$ in
$\Gamma(X)$ and a partial element $u$ on the extent $\psi$ and produces an
element $e_{A}(X,\rho,\psi,u)$ in $A\rho$ such that

  1. 1.

$e_{A}(X,\rho,\psi,u)=u$ on $\psi$,

  2. 2.

$e_{A}(X,\rho,\psi,u)f=e_{A}(Y,\rho f,\psi,uf)$ for $f:Y\rightarrow X$.

Given such an operation, we also call $A$ _trivially fibrant_ (again, this is
structure rather than property).

If $A$ is contractible, each $A(X)$ is a contractible family of types over
$\Gamma(X)$. But conversely, it may be that each $A(X)$ has an extension
operation $e_{A}(X)$ which does not commute with restriction (see Subsection
2.4). Similarly, a map $\sigma:A\rightarrow B$ which is an equivalence defines
a family of equivalences $\sigma_{X}:A(X)\rightarrow B(X)$ but it may be that
each map $\sigma_{X}$ is an equivalence, without $\sigma$ being an
equivalence.

######  Remark 2.1.

We have a canonical map from $\Phi$ to $\Phi_{\mathsf{lw}}$ sending
$\psi:\Phi(X)$ to the constant family on $\psi$. This map commutes (up to
isomorphism) with the decoding to propositions. It follows that there is a
natural map from extension operations for $\Phi$ to extension operations for
$\Phi_{\mathsf{lw}}$, and the same holds for filling operations. It follows
that a (contractible) type for the cubical presheaf model for $\Phi$ is
naturally also a (contractible) type for the cubical presheaf model for
$\Phi_{\mathsf{lw}}$.

######  Remark 2.2.

Let ${\mathcal{C}}$ be a groupoid. Then for $\psi:\Phi_{\mathsf{lw}}(X)$ and
$f:Y\to X$, we have
$\psi_{\mathsf{id}_{X}}\leq\psi_{f}\leq\psi_{ff^{-1}}=\psi_{\mathsf{id}_{X}}.$
It follows that $\psi$ is the constant family on $\psi_{\mathsf{id}_{X}}$.
Thus, the map $\Phi\to\Phi_{\mathsf{lw}}$ from Remark 2.1 is invertible. It
follows that the cubical presheaf models for $\Phi$ and $\Phi_{\mathsf{lw}}$
are the same. We thank Emily Riehl for this observation.

###  2.4 Examples

Let $\mathcal{B}$ be a concrete cube category, for instance the Cartesian [2],
distributive lattice, or de Morgan one [22, 9]. Then we have a nerve functor
from groupoids to cubical sets in the sense of presheaves over $\mathcal{B}$.
In this way, we can see any groupoid as a cubical set with a canonical filling
operation.

For the first example, let ${\mathcal{C}}$ be the group $\mathbb{Z}/(2)$. Let
$\tau$ be the non-trivial element of this group. A context is a space with an
involutive action $\rho\mapsto\rho\tau$. A dependent type $A$ over $\Gamma$
has also an involutive action $A\rho\rightarrow A\rho\tau$ denoted by
$u\mapsto u\tau$ with a filling operation which is equivariant, meaning
$c_{A}(\gamma,\psi,u)(i)\tau=c_{A}(\gamma\tau^{+},\psi,u\tau^{+})(i)$. Let $A$
be the groupoid with two isomorphic objects swapped by $\tau$. Then $A$ is
pointwise contractible, but is not contractible in the presheaf model, since
it has no global point. Another way to describe this example is that the
unique map $A\rightarrow\mathbf{1}$ is a pointwise equivalence, but is not an
equivalence.

For the second example, let ${\mathcal{C}}$ be the poset on objects $\bot,0,1$
with $\bot<0$ and $\bot<1$. We define a global type $A$ as follows. We take
$A(0)$ and $A(1)$ to consist of a single object $a_{0}$ and $a_{1}$,
respectively. We take $A(\bot)$ to consist of an isomorphism between the
restrictions of $a_{0}$ and $a_{1}$. Then $A$ is levelwise contractible (i.e.,
$A(\bot),A(0),A(1)$ are contractible), but $A$ is not contractible since it
has no global point.

We note that the second example is fixed by working with the cofibration
classifier $\Phi_{\mathsf{lw}}$. However, as explained by Remark 2.2, this
does not apply to the first example.

##  3 Homotopy descent data

###  3.1 A lex operation

In this Subsection, we work in the internal language of the presheaf topos
over $\mathcal{B}$. We first define a lex operation on presheaf types, and
then show that this lex operation extends to types with a filling operation.

For any $A$ presheaf over $\Gamma$ we define $EA$ presheaf over $\Gamma$. An
element $u$ of $(EA)\rho$, for $\rho$ in $\Gamma(X)$ is given by a family of
elements $u(f)$ in $A\rho f$ for $f:Y\rightarrow X$. We define the restriction
$uf$ in $(EA)\rho f$ by $uf(g)=u(fg)$ if $f:Y\rightarrow X$ and
$g:Z\rightarrow Y$.

If $B$ is presheaf over $\Gamma.A$, we define $\tilde{E}(B)$ presheaf over
$\Gamma.{EA}$. If $\rho$ is in $\Gamma(X)$ and $u$ is in $(EA)\rho$, then
$\tilde{E}(B)(\rho,u)$ is the space of families $v(f)$ in $B(\rho f,u(f))$.

We define a natural transformation $\alpha:A\rightarrow EA$ by $(\alpha
a)(f)=af$.

Next, we extend the action of $E$ to types with a filling operation. Actually,
we define a filling operation $E(c_{A})$ on $EA$ assuming only that $c_{A}$ is
a pointwise filling operation on $A$.

######  Proposition 3.1.

We can define a filling operation $E(c_{A})$ on $EA$ if $c_{A}$ is a pointwise
filling operation on $A$, in a way which commutes with substitution.

###### Proof.

We assume that $A$ has a pointwise filling operation $c_{A}(X)$. We define
then, for $f:Y\rightarrow X$

$E(c_{A})(X,\gamma,\psi,u)(i)(f)=c_{A}(Y)(\gamma f^{+},\psi,uf^{+})(i)$

We can then check for $f:Y\rightarrow X$ and $g:Z\rightarrow Y$

$c_{EA}(X,\gamma,\psi,u)(i)f(g)=c_{A}(Z)(\gamma(fg)^{+},\psi,u(fg)^{+})(i)=c_{EA}(Y,\gamma
f^{+},\psi,uf^{+})(i)(g)$

and hence $c_{EA}$ is natural in $X$.

We can also define $\langle\rangle$ in $E\mathbf{1}$ by $\langle\rangle(f)=()$
and $\langle u,v\rangle:E(\sum_{A}B)\rho$ by $\langle
u,v\rangle(f)=(u(f),v(f))$ for $u$ in $(EA)\rho$ and $v$ in
$(\tilde{E}B)(\rho,u)$, and check that all conditions for a lex operations are
satisfied.

Any universe $\mathcal{U}$ reflects the operations $E$ and $\tilde{E}$ since
the Grothendieck universe $U$ used to construct $\mathcal{U}$ was assumed to
contain ${\mathcal{C}}$. ∎

######  Proposition 3.2.

If $A$ is pointwise contractible then $EA$ is contractible.

###### Proof.

We assume that $A$ has a pointwise extension operation $e_{A}(X)$. We define
then, for $f:Y\rightarrow X$

$e_{EA}(X,\rho,\psi,u)(f)=e_{A}(Y)(\rho f,\psi,uf)$

We can then check for $f:Y\rightarrow X$ and $g:Z\rightarrow Y$

$e_{EA}(X,\rho,\psi,u)f(g)=e_{A}(Z)(\rho fg,\psi,ufg)=e_{EA}(Y,\rho
f,\psi,uf)(g)$

and hence $e_{EA}$ is an extension operation for $EA$ natural in $X$. ∎

In general, $E$ may not be a descent data operation, since $EA$ does not need
to be $E$-modal. The next Subsection will use the lex operation $E$ to define
a descent data operation.

###  3.2 Homotopy descent data

In this Subsection, unless explicitly stated, we work in the internal language
of the presheaf model over ${\mathcal{C}}\times\mathcal{B}$. Starting from the
lex operation $E$, we define a new lex operation $D$. As before, we first
define $D$ on presheaves, and then show that it extends to a lex operation on
presheaves with a filling operation. On presheaves with a filling operation,
$D$ will be a descent data operation.

We let $\mathsf{P}_{n}$ be the subpresheaf of $\mathbb{I}^{n+1}$ of elements
$(i_{0},i_{1},\dots,i_{n})$ satisfying $i_{0}=1\vee\dots\vee i_{n}=1$.

Let $s_{k}:\mathbb{I}^{n+1}\rightarrow\mathbb{I}^{n}$ be the map which omits
the $k$th component, for $k=0,\dots,n$. Note that $s_{k}\vec{i}$ is in
$\mathsf{P}_{n-1}$ if $\vec{i}$ is in $\mathsf{P}_{n}$ and $i_{k}=0$.

######  Definition 3.3.

An element of $DA$ is given by a family $u(\vec{i})$ in $E^{n+1}A$ defined on
$\mathsf{P}_{n}$ and satisfying the compatibility conditions101010It is
suggestive to think of the elements of $DA$ as choice sequences [33] extended
in a spatial rather than temporal dimension.
$u(\vec{i})=E^{k}(\alpha)u(s_{k}\vec{i})$ on $i_{k}=0$.

For instance we have

$\displaystyle u(0,i_{1},i_{2})$ $\displaystyle=\alpha u(i_{1},i_{2})$
$\displaystyle u(i_{0},0,i_{2})$ $\displaystyle=E(\alpha)u(i_{0},i_{2})$
$\displaystyle u(i_{0},i_{1},0)$ $\displaystyle=E^{2}(\alpha)u(i_{0},i_{1})$

We have an element $u(\vec{1})$ in each $E^{n+1}A$. We have a path $u(1,i)$
between $\alpha\,u(1)$ and $u(1,1)$ and a path $u(i,1)$ between
$E(\alpha)\,u(1)$ and $u(1,1)$ in $E^{2}A$. But, in general, we need further
higher coherence conditions.

We define $\eta_{A}:A\rightarrow DA$ by
$(\eta_{A}\,a)(i_{0},i_{1},\dots,i_{n})=\alpha^{n+1}a$.

If $A$ is a family of types over $\Gamma$ we define $DA$ family of types over
$\Gamma$ by $(DA)\rho=D(A\rho)$.

######  Proposition 3.4.

If $A$ is a family of types with a pointwise filling operation, then $DA$ has
a filling operation.

###### Proof.

We use that each $E^{n+1}A$ has a (uniform) filling operation by Proposition
3.1 hence is a family of types in the model over
${\mathcal{C}}\times\mathcal{B}$. We assume given $\gamma$ in
$\Gamma^{\mathbb{I}}$ and $\psi$ in $\Phi$ and a partial element $u_{j}$ in
$(DA)\gamma(j)$ defined over $\psi\vee j=0$. We explain how to define a total
extension $v_{j}$ in $(DA)\gamma(j)$. For this we define $v_{j}(\vec{i})$ in
$E^{n+1}A$ by induction on $n$. Since $E^{n+1}A$ has a filling operation, we
apply this filling operation to the partial element equal to $u_{j}(\vec{i})$
on $\psi\vee j=0$ and equal to $E^{k}(\alpha)\,{v_{j}}(s_{k}(\vec{i}))$ if
$i_{k}=0$. ∎

######  Corollary 3.5.

$D$ defines a lex operation. ∎

A similar argument as the one for Proposition 3.4 using Proposition 3.2
instead proves the following.

######  Proposition 3.6.

  1. (i)

If $A$ is a pointwise contractible family of types over $\Gamma$, then $DA$ is
contractible.

  2. (ii)

If $B$ is a pointwise contractible family of types over a family of types $A$
over $\Gamma$, then $\tilde{D}B$ is contractible over $DA$. ∎

######  Corollary 3.7.

Let $\sigma:A\to B$ be map between fibrant families of types over $\Gamma$. If
$\sigma$ is pointwise an equivalence, then $D\sigma$ is an equivalence.

###### Proof.

The fiber $\mathsf{fib}(\sigma)$ defines a pointwise contractible family of
types over $B$. Hence $\tilde{D}\mathsf{fib}(\sigma)$ is contractible over
$DB$. Since $D$ is a lex operation, $\mathsf{fib}(D\sigma)$ is contractible
over $DB$ and $D\sigma$ is an equivalence. ∎

######  Proposition 3.8.

Let $A$ be a fibrant family of types over $\Gamma$. Then $\eta_{A}$ is
pointwise an equivalence and $D\eta_{A}$ is an equivalence.

###### Proof.

For this Proposition, we work in the presheaf model over $\mathcal{B}$. If
$\vec{f}$ is a composable chain of arrows we write $\langle\vec{f}\rangle$ for
its composition.

Let $A$ be a type over $\Gamma$. For $\rho$ in $\Gamma(X)$, an element $u$ of
$(DA)\rho$ is a family of elements $u(\vec{i})(\vec{f})$ in
$A\rho\langle\vec{f}\rangle$ satisfying the compatibility conditions. For $a$
in $A\rho$ the element $\eta_{A}\,a$ is the family of element

$(\eta_{A}\,a)(\vec{i})(\vec{f})=a\langle\vec{f}\rangle$

We define an inverse $G:DA(X)\to A(X)$ of $\eta_{A}(X)$ by taking $Gu$ to be
the element $u(1)(\mathsf{id}_{X})$. We then have $G(\eta_{A}\,a)=a$. The
element $\eta_{A}\,(G\,u)$ satisfies

$(\eta_{A}\,(G\,u))(\vec{i})(\vec{f})=(G\,u)\langle\vec{f}\rangle=u(1)(\mathsf{id})\langle\vec{f}\rangle=u(1,\vec{0})(\mathsf{id},\vec{f})$

Define the element $\tilde{u}$ in $(DA)\rho$ by
$\tilde{u}(\vec{i})(\vec{f})=u(1,\vec{i})(\mathsf{id},\vec{f})$. We can define
a homotopy

$u_{k}(\vec{i})(\vec{f})=u(1,k\wedge\vec{i})(\mathsf{id},\vec{f})$

between $\eta_{A}\,(G\,u)$ and $\tilde{u}$ and we can define a homotopy

$v_{k}(\vec{i})(\vec{f})=u(k,\vec{i})(\mathsf{id},\vec{f})$

between $u$ and $\tilde{u}$.111111At this point that we use that the object I
in $\mathcal{B}$ has lattice operations but one could however instead define a
homotopy in a more complex way by induction on the dimension for Cartesian
cubes. The same remark applies for the proof of the next Proposition. By
composition, there is a path between $u$ and $\eta_{A}\,(G\,u)$ and $G$ is an
inverse of $\eta_{A}(X)$.

This shows that $\eta_{A}$ is pointwise an equivalence. Then $D\eta_{A}$ is an
equivalence by Corollary 3.7. ∎

One way to understand the definition of $D$ from $E$ is the following. Being a
pointed endofunctor, $E$ defines a cosemisimplicial diagram starting from
$EA$, and $DA$ is a strict way to realize the homotopy limit of this diagram
using a $\mathsf{P}$-weighted limit. We can think of $\mathsf{P}$ as a
cofibrant resolution of the constant diagram on $1$. A remark is that $E$, and
hence each $E^{l}$, preserves the $\mathsf{P}$-weighted limit defining $D$. In
particular, an element of $E^{l}(DA)$ is determined by a family $u(\vec{i})$
in $E^{l+n+1}A$ satisfying $u(\vec{i})=E^{l+k}(\alpha)\,u(s_{k}\vec{i})$ on
$i_{k}=0$.

######  Proposition 3.9.

Let $A$ be a fibrant family of types over $\Gamma$. We can build a path
between $\eta_{DA}$ and $D\eta_{A}$.

###### Proof.

An element of $(D^{2}A)\rho$ is given by a family $v(\vec{i})(\vec{j})$ in
$E^{n+m+2}A$ satisfying the conditions

  1. 1.

$v(\vec{i})(\vec{j})=E^{k}(\alpha)\,v(s_{k}\vec{i})(\vec{j})$ on $i_{k}=0$

  2. 2.

$v(\vec{i})(\vec{j})=E^{n+1+l}(\alpha)\,v(\vec{i})(s_{l}\vec{j})$ on $j_{l}=0$

Given $u$ in $(DA)\rho$ we define an element $\tilde{u}$ in $(D^{2}A)\rho$ by
$\tilde{u}(\vec{i})(\vec{j})=u(\vec{i},\vec{j})$.

We compute, for $u$ in $(DA)\rho$

$(\eta_{DA}\,u)(\vec{i})(\vec{j})=\alpha^{n+1}\,u(\vec{j})={u}(\vec{0},\vec{j})$

and we have a homotopy connecting this map to $\tilde{u}$ by defining

$v_{k}(\vec{i})(\vec{j})=u(\vec{i}\wedge k,\vec{j}).$

We also have

$((D\eta_{A})\,u)(\vec{i})(\vec{j})=E^{n+1}(\alpha^{m+1})\,u(\vec{i})={u}(\vec{i},\vec{0})$

and we have a homotopy connecting this map to $\tilde{u}$ by defining

$w_{k}(\vec{i})(\vec{j})=u(\vec{i},k\wedge\vec{j})$

By composition, we have a path between $D\eta_{A}$ and $\eta_{DA}$. ∎

######  Corollary 3.10.

$D$ defines a descent data operation.

###### Proof.

By Propositions 3.8 and 3.9. ∎

Note that a direct consequence of Corollary 3.7 is the following
strictification result.

######  Theorem 3.11.

Let $A$ and $B$ be fibrant families of types over $\Gamma$ that are $D$-modal.
Then any pointwise equivalence $\sigma:A\to B$ is an equivalence. ∎

Let us note the following consequence of Proposition 3.8.

######  Corollary 3.12.

The following conditions are equivalent:

  1. 1.

all fibrant families of types are $D$-modal,

  2. 2.

all pointwise equivalences between fibrant families of types are equivalences,

  3. 3.

all fibrant families of types that are pointwise contractible are
contractible.

###### Proof.

The direction from condition 1 to condition 2 is Theorem 3.11. In the reverse
direction, given a fibrant family of types $A$, recall that $\eta_{A}$ is a
pointwise equivalence by Proposition 3.8. Then $\eta_{A}$ is an equivalence
and hence $D$-modal. Condition 3 is a special case of condition 2. The reverse
direction holds since a (pointwise) equivalence can be described as a map with
(pointwise) contractible fibers. ∎

The way from which we get $D$ from $E$ can also be applied to the lex
operation $EA=A^{R}$, where $R$ is an arbitrary type. This amounts to give a
map which is coherently constant as defined by Kraus [19] and so a map
$\left\|R\right\|\rightarrow A$ from the propositional truncation of $R$ to
$A$ [19].

Our development actually provides a way to recover this result in the cubical
setting. Indeed, an element of $DA$ is a sequence of elements
$u(\vec{i})(\vec{x})$ in $A$ for $\vec{i}$ in $\mathsf{P}_{n}$ and $\vec{x}$
in $R^{n+1}$ with $u(\vec{i})(\vec{x})=u(s_{k}\vec{i})(s_{k}\vec{x})$ on
$i_{k}=0$. Given an element $x$ in $R$, we can build a left inverse $p_{A}$ of
$\eta_{A}:A\rightarrow DA$ by taking $p_{A}u=u(1)(x)$. Hence we get an element
of $R\rightarrow\mathsf{isEquiv}(\eta_{A})$, and so of
$\left\|R\right\|\rightarrow\mathsf{isEquiv}(\eta_{A})$ which provides a
factorization of a coherently constant map $R\rightarrow A$ through
$R\rightarrow\left\|R\right\|$.

###  3.3 Case of a monoid

We consider the special case where the base category is a monoid $M$. If
$\vec{x}$ is a sequence $(x_{0},\dots,x_{n})$, we write $t_{k}\vec{x}$ for the
sequence where we omit $x_{k}$ and replace $x_{k+1}$ by $x_{k}x_{k+1}$ for
$k<n$ and $t_{n}\vec{x}$ is the sequence where we omit $x_{n}$. A type in the
presheaf model is a type $A$ with an $M$-action, and an element of $DA$ is
then a family of elements $u(\vec{i})(\vec{x})$ in $A$ with $\vec{i}$ in
$\mathsf{P}_{n}$ and $\vec{x}$ in $M^{n+1}$ satisfying the compatibility
conditions

  1. 1.

$u(\vec{i})(\vec{x})=u(s_{k}\vec{i})(t_{k}\vec{x})$ on $i_{k}=0$ for $k<n$ and

  2. 2.

$u(\vec{i})(\vec{x})=u(s_{n}\vec{i})(t_{n}\vec{x})x_{n}$ on $i_{n}=0$

We define the $M$-action on $DA$ by
$ux(\vec{i})(x_{0},\dots,x_{n})=u(\vec{i})(xx_{0},\dots,x_{n})$.

As a special case, let $M$ be the walking idempotent. Let $e^{2}=e$ be the
non-trivial idempotent element of $M$. Here is an example of a non-modal type
which is pointwise contractible, but not contractible. Let $\Gamma$ be the set
with elements $\rho_{1},\rho_{2}$ and $\rho$ with $\rho_{1}e=\rho_{2}e=\rho$.
We let $A$ be the following type. We let $A\rho_{1}$ be the point $a_{1}$ and
$A\rho_{2}$ be the point $a_{2}$ and $A\rho$ be the groupoid with two
isomorphic objects $u_{1},u_{2}$ with $a_{i}e=u_{i}$ for $i=1,2$. The type $A$
is then pointwise contractible but it has no global point.121212If $a$ is such
a point, we should have $a\rho_{i}=a_{i}$ and then $(a\rho_{i})e=u_{i}$ and
$a(\rho_{1}e)=a(\rho_{2}e)=a\rho$ which is not possible since $u_{1},u_{2}$
are distinct.

###  3.4 Generalization to a Grothendieck topology

A Grothendieck topology $\mathsf{J}$ on the category ${\mathcal{C}}$ defines a
set $\mathsf{C}(X,I)=\mathsf{J}(X)$ and we have a family $E_{S}$ indexed by
$S:\mathsf{C}$ defined as follows. Let $\rho$ be in $\Gamma(X)$, and $S$ is in
$\Gamma\rightarrow\mathsf{C}$, so that $S\rho$ is in
$\mathsf{C}(X)=\mathsf{J}(X)$, which is a set of sieves on $X$.

An element of $(E_{S}A)\rho$ is now a family $u(f)$ in $A\rho f$ with $f$ in
$S\rho$. We define in this way a family of lex operations $E_{S}$ and an
associated family of descent data operations $D_{S}$ indexed by
$S:\mathsf{C}$.

Note that if $S_{1}\rho$ is a subset of $S_{2}\rho$ for all $\rho$, then we
have a canonical projection map $D_{S_{2}}A\rightarrow D_{S_{1}}A$ that
coheres with the pointings. If $A$ is $D_{S_{1}}$-modal a left inverse of
$\eta^{S_{1}}_{A}$ composed with this projection map is a left inverse of
$\eta^{S_{2}}_{A}$. Hence a $D_{S_{1}}$-modal type is also $D_{S_{2}}$-modal
and we have $D_{S_{1}}\leqslant D_{S_{2}}$ for the preorder defined in
Subsection 1.6. Since $\mathsf{J}$ is a Grothendieck topology, the family
$D_{S}$ over $S:\mathsf{C}$ is filtered. Thus, we can apply Theorem 1.15 to
obtain a model of univalent type theory with higher inductive types. This can
be seen as constructively modelling higher sheaves over $\mathsf{J}$ in the
cubical model over $\mathcal{B}$.

The next Proposition will be used for building such a sheaf model where
countable choice does not hold. The proof is similar to the one of Proposition
3.4.

######  Proposition 3.13.

If $A$ in $\hbox{\sf Type}(\Gamma)$ and $S$ in $\Gamma\rightarrow\mathsf{C}$
and $A$ is $D_{S}$-modal and $\rho$ in $\Gamma(X)$ and $A\rho f$ is
(pointwise) contractible for each $f$ in $S\rho$ then we can find a uniform
extension operation $e_{A\rho}(f,\psi,u)$ in $A\rho f$ for all $f:Y\rightarrow
X$ and $u$ partial element in $A\rho f$ of extent $\psi$. ∎

By uniform, we mean that we have

$e_{A\rho}(f,\psi,u)g=e_{A\rho}(fg,\psi,ug)$

in $A\rho fg$ for any $g:Z\rightarrow Y$.

###  3.5 A model with the negation of countable choice

Using in an essential way the notion of homotopy descent data, we build a
model of univalent type theory with higher inductive types with a countable
family of sets $E_{n}$ such that each the homotopy propositional truncation
$\left\|E_{n}\right\|$ is inhabited, but $\left\|\prod_{n:N}E_{n}\right\|$ is
not globally inhabited.

We consider the following space, corresponding to the lattice generated by
formal elements $X_{n}$ and $L_{n}$ with the relations $X_{0}=1$,
$X_{n}=L_{n}\vee X_{n+1}$ and $L_{n+1}=L_{n}\wedge X_{n+1}$. Using Proposition
3.13 one can show the following result.

######  Proposition 3.14.

The type $\left\|L_{0}+X_{n}\right\|$ is contractible for all $n$ while
$L_{0}$ is the homotopy propositional truncation of
$\prod_{n:N}(L_{0}+X_{n})$. ∎

######  Corollary 3.15.

There exists a model of univalent type theory with higher inductive types
where countable choice does not hold. ∎

As stressed in [32], it is yet unknown how to build a model of univalent type
theory and higher inductive types satisfying countable choice in a
constructive metatheory. (Countable choice holds in a classical metatheory in
the simplicial set model.)

##  4 Variation with another notion of cofibration

We explain how to modify the definition of filling operation if we work with
the other notion of cofibration classified by $\Phi_{\mathsf{lw}}$. Recall
that an element of $\Phi_{\mathsf{lw}}(X)$ is no longer constant, but is given
by a family of elements $\psi_{f}$ in $\Phi_{\mathcal{B}}$ for $f:Y\rightarrow
X$ and satisfying $\psi_{f}\leqslant\psi_{fg}$ if $g:Z\rightarrow Y$.

All the main results above still hold for this new notion of cofibration,
suitably modified. The notion of filling operation for $A$ is given by an
operation $c_{A}$ which takes as argument $\gamma$ in
$\Gamma(X)^{\mathbb{I}_{\mathcal{B}}}$ and $\psi$ in $\Phi_{\mathcal{B}}(X)$
and a family of elements $u(i)$ in $A\gamma(i)f$ on the extent $\psi_{f}\vee
i=0$ such that $u_{f}(i)g=u_{fg}(i)$ for $g:Z\rightarrow Y$ on the extent
$\psi_{f}\vee i=0$. (There is a dual operation with $i=1$ instead.) It
produces an element $c_{A}(X,\gamma,\psi,u)(i)$ in $A\gamma(i)$ such that

  1. 1.

$c_{A}(X,\gamma,\psi,u)(i)f=u_{f}(i)$ on $\psi_{f}\vee i=0$,

  2. 2.

$c_{A}(X,\gamma,\psi,u)(i)f=c_{A}(Y,\gamma^{\prime},\psi f,u^{\prime})(i)$
with $\gamma^{\prime}(i)=\gamma(i)f$ and $u^{\prime}_{g}(i)=u_{fg}(i)$ on the
extent $\psi_{fg}\vee i=0$ for $g:Z\rightarrow Y$.

For instance, Proposition 3.1 becomes the following result.

######  Lemma 4.1.

If $A$ has a pointwise filling operation $c_{A}(X)$ then $EA$ has a filling
operation.

###### Proof.

We take $\gamma$ in $\Gamma(X)^{\mathbb{I}_{\mathcal{B}}}$ and $u_{f}(i)$ in
$(EA)\gamma(i)f$ on the extent $\psi_{f}\vee i=0$ and we define
$v(i)=c_{EA}(X,\gamma,\psi,u)(i)$ in $(EA)\gamma(i)$. For $f:Y\rightarrow X$,
we take (filling at level $Y$)

$v(i)(f)=c_{A}(Y)(\gamma^{\prime},\psi^{\prime},u^{\prime})$

where $\gamma^{\prime}(i)=\gamma(i)f$ and $\psi^{\prime}=\psi_{f}$ and
$u^{\prime}(i)=u_{f}(i)(\mathsf{id}_{Y})$ in $A\gamma(i)f$ on the extent
$\psi_{f}\vee i=0$. ∎

Let us give some examples.

The first example is when ${\mathcal{C}}$ is the poset $0\leqslant 1$. In this
case, a global type $A$ is given by two spaces with a map $A(1)\rightarrow
A(0)$. An element of $\Phi_{\mathsf{lw}}(0)$ is an element of
$\Phi_{\mathcal{B}}$ while an element of $\Phi_{\mathsf{lw}}(1)$ is a pair
$\psi_{1},\psi_{0}$ of elements of $\Phi_{\mathcal{B}}$ with
$\psi_{1}\leqslant\psi_{0}$. One can check that $A$ is fibrant exactly if
$A(0)$ is fibrant and $A(1)\to A(0)$ is a fibration, and a similar
characterization holds in the relative situation (for a type $A$ over
$\Gamma$) and for trivial fibrations. Using condition 3 of Corollary 3.12, one
sees that every type in the model is $D$-modal. The model coincides with the
Reedy presheaf model described in [29] over the direct category
${\mathcal{C}}$ in the model of univalent type theory given by the base model.
More generally, this will be the case for an arbitrary direct category
${\mathcal{C}}$ for which the inclusion of objects into morphisms given by
identities is decidable.

The second example is the walking retract ${\mathcal{C}}$ generated by maps
$f\colon 0\to 1$ and $g\colon 1\to 0$ satisfying $gf=\mathsf{id}_{0}$. Note
that ${\mathcal{C}}$ is the idempotent splitting of the walking idempotent
monoid $\mathcal{M}$ considered in Subsection 3.3. This makes the cubical
presheaf models (for both $\Phi$ and $\Phi_{\mathsf{lw}}$) over
${\mathcal{C}}$ and $\mathcal{M}$ equivalent. Level $0$ in the model over
${\mathcal{C}}$ correspond to the fixpoints of the action of $e$ in the model
over $\mathcal{M}$. Taking $\Phi_{\mathsf{lw}}$ as the cofibration classifier,
the model of modal types gives a model for pointed families in a cubical
model. It is homotopically correct in the sense that the equivalences are
levelwise.

One might ask if types in the above model are already $D$-modal, similar to
what happens for the poset $0\leqslant 1$. More generally, one might attempt
to generalize from a direct category ${\mathcal{C}}$ to a Reedy category
${\mathcal{C}}$ that is elegant [6]; the walking retract is an example of an
elegant Reedy category, with coface map $f$ and codegeneracy map $g$. Taking
$\Phi_{\mathsf{lw}}$ as the cofibration classifier, one might ask if the
(trivial) fibrations are given by the (trivial) Reedy fibrations; as before,
this would imply that every type in the model is $D$-modal. An equivalent
condition is that the levelwise cofibrations (classified by
$\Phi_{\mathsf{lw}}$) are also the Reedy cofibrations. This holds true in
classical situations where cofibrations and monomorphisms coincide and gives
rise to the classical model [28] over an elegant Reedy category.

Unfortunately, this fails to hold in our constructive setting. Ultimately,
this is because the inclusions $A(X)\to A(Y)$ are not generally cofibrations
for a global type $A$ and a codegeneracy map $Y\to X$ in ${\mathcal{C}}$. For
the case of the walking retract, this is the inclusion $A(0)\to A(1)$. In
terms of a global type $A$ in the model over the walking monoid $\mathcal{M}$,
it is the inclusion of fixpoints of the action of $e$ on $A$. For a
counterexample, let $S$ be a discrete space with non-decidable equality in one
of the concrete cubical models listed in Subsection 2.4. Take $A=S\times S$
with the action of $e$ given by swapping.

##  5 Related and future work

Shulman [31] shows that all $(\infty,1)$-toposes have strict univalent
universes, using a classical metatheory. This work does not cover however
(yet) higher inductive types and cumulativity of universes. There are close
connections between Shulman’s work and ours, which we plan to explore in
future work. His work inspired some results about pointwise weak equivalences
in Subsection 3.2, in particular Corollary 3.7.

Once we have a presheaf model of univalence with homotopical features such as
ours, it is now understood (see e.g. [25, 8]) how to define a Quillen model
structure whose (trivial) fibrations coincide with the (contractible) types.
For the model of $D$-modal types, we expect that, similar to [31], that the
weak equivalences are the levelwise weak equivalences and the fibrations are a
variation131313We define a family of types to be injectively fibrant if it
lifts against cofibrations that are levelwise trivial cofibrations. of the
injective fibrations. We leave this to future work.

Instead of parameterizing our construction over an external category
${\mathcal{C}}$, we could start from a internal category ${\mathcal{C}}$ in
presheaves over $\mathcal{B}$. Note that the category of presheaves over an
internal category in presheaves is still a presheaf category. Compared to the
construction of [31] (which instantiates at this level of generality), we seem
to need less fibrancy assumptions on this internal category. We leave this
generalization to future work.

## Acknowledgements

Many thanks to Mathieu Anel, Steve Awodey, Martín Escardó, Eric Finster, Dan
Licata, Emily Riehl, Mike Shulman, Bas Spitters and Matthew Weaver for many
discussions and remarks.

##  Appendix A General results for lex modalities

Some of our results hold for modalities in the sense of [24] that are not
necessarily presented in a strict manner by a lex operation. The main example
is the case of accessible modalities, which are implemented using higher
inductive types that rarely give rise to a lex operation. The purpose of this
Appendix is to prove these more general statements. We work in the homotopy
type theory setting of [24]. Universes are assumed univalent and closed under
dependent sums, dependent products, identity types. For statements involving
accessible modalities, we also assume closure under higher inductive types.

In this Appendix, we take terminology with potentially both strict and
homotopical meaning to have the homotopical meaning by default. This is
opposed to the rest of the article, where we default to the strict meaning.
For example, equality refers to the identity type, and pullbacks refer to
homotopy pullbacks (expressed using the identity type).

We write $\mathsf{Modality}(\mathcal{U})$ for the type of modalities on a
universe $\mathcal{U}$. Recall from [24] that
$M:\mathsf{Modality}(\mathcal{U})$ has an underlying subuniverse141414By a
subuniverse of $\mathcal{U}$, we mean a subobject of $\mathcal{U}$, i.e. a
predicate on $\mathcal{U}$. This is formally a map
$\mathcal{U}\to\mathsf{Prop}$ where $\mathsf{Prop}$ is the universe of
(homotopy) propositions. It is not to be confused with a subuniverse in the
set-theoretic sense in a model where universes are built out of sets. We note
that the size of the propositions in $\mathsf{Prop}$ here does not matter for
us; one choice is propositions in $\mathcal{U}$, but one could allow also a
larger universe.  of $\mathcal{U}$, the $M$-modal types $\mathcal{U}_{M}$.
Subuniverses of $\mathcal{U}$ carry an evident poset structure. Following [24,
Subsection 3.2], we obtain a poset structure also on
$\mathsf{Modality}(\mathcal{U})$.

######  Definition A.1.

Let $\mathcal{U}$ be a universe contained in a universe
$\mathcal{U}^{\prime}$. A modality $M^{\prime}$ on $\mathcal{U}^{\prime}$ is
an _extension_ of a modality $M$ on $\mathcal{U}$ if every $M$-modal type in
$\mathcal{U}$ is $M^{\prime}$-modal in $\mathcal{U}^{\prime}$ and for
$X:\mathcal{U}$, the canonical map $M^{\prime}X\to MX$ is invertible.

The above conditions mean that a $\mathcal{U}$-small type is $M$-modal exactly
if it is $M^{\prime}$-modal and $M$-connected exactly if it is
$M^{\prime}$-connected. In terms of the stable factorization systems
$(\mathcal{L},\mathcal{R})$ and $(\mathcal{L}^{\prime},\mathcal{R}^{\prime})$
corresponding to $M$ and $M^{\prime}$, this means that $\mathcal{L}$ and
$\mathcal{R}$ are the restrictions of $\mathcal{L}^{\prime}$ and
$\mathcal{R}^{\prime}$ to maps between $\mathcal{U}$-small types. For this,
recall [24, Subsection 1.2] that the left and right classes of the stable
factorization system corresponding to a modality are the connected and modal
maps, which are defined by having connected and modal fibers, respectively.

We write $\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$ for the type of
pairs $(M,M^{\prime})$ with $M$ a modality on $\mathcal{U}$ and $M^{\prime}$
an extension of $M$ to $\mathcal{U}^{\prime}$. The poset structures on
$\mathsf{Modality}(\mathcal{U})$ and $\mathsf{Modality}(\mathcal{U}^{\prime})$
extend to a poset structure on
$\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$.

The following statement makes precise that up to (essential) size issues, a
modality is lex exactly if the universe of modal types is modal. In
particular, a “size-polymorphic” modality (acting compatibly on all universes)
whose action on maps preserves smallness of fibers is lex exactly if universes
of modal types are modal. This generalizes Proposition 1.14 to modalities; the
smallness condition on fibers mirrors the dependent action $\tilde{D}$ on
$\mathcal{U}$-small types we require for a lex operation $D$. For
$M:\mathsf{Modality}(\mathcal{U})$, we denote by $\mathcal{U}_{M}$ the
subuniverse of $\mathcal{U}$ of $M$-modal types.

######  Proposition A.2.

For $(M,M^{\prime}):\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$:

  1. (i)

if $M^{\prime}$ is lex and preserves maps with $\mathcal{U}$-small fibers,
then $\mathcal{U}_{M}$ is $M^{\prime}$-modal;

  2. (ii)

if $\mathcal{U}_{M}$ is $M^{\prime}$-modal, then $M$ is lex and $M^{\prime}$
preserves maps with $\mathcal{U}$-small fibers.

###### Proof.

For part (i), let $M^{\prime}$ be lex and preserve maps with
$\mathcal{U}$-small fibers. To show that $\mathcal{U}_{M}$ is
$M^{\prime}$-modal, it suffices to construct a left inverse to
$\eta^{M^{\prime}}_{\mathcal{U}_{M}}$ ([24, Lemma 1.20]). By univalence of
$\mathcal{U}_{M}$, this means to find an extension

$\textstyle{\textstyle\sum_{X:\mathcal{U}_{M}}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
$\mathcal{U}$-small and $M$-modal fibers
$\textstyle{\mathcal{U}_{M}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta^{M^{\prime}}_{\mathcal{U}_{M}}}$$\textstyle{M^{\prime}\mathcal{U}_{M}\hbox
to0.0pt{.\hss}}$

We use the naturality square of $\eta^{M^{\prime}}$ at the left map. The
square is a pullback because $M^{\prime}$ is lex. The right map has
$\mathcal{U}$-small fibers by assumption and has $M$-modal fibers because it
is $M^{\prime}$-modal as it goes between $M^{\prime}$-modal types.

For part (ii), assume that $\mathcal{U}_{M}$ is $M^{\prime}$-modal. Then
$\mathcal{U}_{M}$ is right orthogonal against $M^{\prime}$-connected types, in
particular $M$-connected types. This verifies condition (xiii) of [24, Theorem
3.1], making $M$ lex. It remains to show that $M^{\prime}$ preserves maps with
$\mathcal{U}$-small fibers. Given such a map, we factor it using $M$ as an
$M^{\prime}$-connected map followed by a map with fibers in $\mathcal{U}_{M}$.
Since $M^{\prime}$ sends $M^{\prime}$-connected maps to equivalences, it
remains to show, given $Y:X\to\mathcal{U}_{M}$, that $M^{\prime}(\sum_{X}Y)\to
M^{\prime}X$ has $\mathcal{U}$-small fibers. Since $\mathcal{U}_{M}$ is
$M^{\prime}$-modal, it is right orthogonal against $X\to M^{\prime}X$. Thus,
$Y:X\to\mathcal{U}_{M}$ extends uniquely to a map
$Y^{\prime}:M^{\prime}X\to\mathcal{U}_{M}$. Looking at the classified maps, we
obtain the following commuting diagram:

$\textstyle{\textstyle\sum_{X}Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\textstyle\sum_{z:M^{\prime}X}Y^{\prime}(z)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta^{M^{\prime}}_{X}}$$\textstyle{M^{\prime}X\hbox
to0.0pt{.\hss}}$

Since the right map has $M$-modal (hence also $M^{\prime}$-modal) fibers, it
is $M^{\prime}$-modal. The top map is a pullback of $\eta^{M^{\prime}}_{X}$,
hence $M^{\prime}$-connected. Since

$\textstyle\sum_{X}Y\longrightarrow\textstyle\sum_{z:M^{\prime}X}Y^{\prime}(z)\longrightarrow
M^{\prime}X$

and

$\textstyle\sum_{X}Y\longrightarrow
M^{\prime}(\textstyle\sum_{X}Y)\longrightarrow M^{\prime}X$

are ($M^{\prime}$-connected, $M^{\prime}$-modal)-factorizations of the same
map, they coincide. This shows that the map $M^{\prime}(\sum_{X}Y)\to
M^{\prime}X$ is equal to $\sum_{z:M^{\prime}X}Y^{\prime}(z)\to M^{\prime}X$,
hence has $\mathcal{U}$-small fibers. ∎

Recall from [24, Subsection 2.3] that accessible modalities admit canonical
extensions to larger universes. If the accessible modality is lex, we observe
that it satisfies the technical condition on smallness of fibers of
Proposition A.2. This means that part (i) of that statement can also be
regarded as a generalization of the direction from condition (i) to condition
(iii) in [24, Theorem 3.11].

######  Corollary A.3.

Let $M$ be an accessible lex modality on a universe $\mathcal{U}$. Let
$M^{\prime}$ be its extension to a universe $\mathcal{U}^{\prime}$ containing
$\mathcal{U}$. The $M^{\prime}$ preserves maps with $\mathcal{U}$-small
fibers.

###### Proof.

This follows from part (ii) of Proposition A.2 since $\mathcal{U}_{M}$ is
$M^{\prime}$-modal by [24, Theorem 3.11]. ∎

Let $M:I\to\mathsf{Modality}(\mathcal{U})$ be a family of modalities. We write

$\mathcal{U}(M)=\textstyle\sum_{X:\mathcal{U}}\textstyle\prod_{i:I}\,\text{$X$
is $M_{i}$-{}modal}.$ (1)

for the meet of the subuniverses of modal types of $M_{i}$ over $i:I$. We call
a given meet $\bigwedge M$ of $M$ _structural_ if it is preserved under the
forgetful functor to the poset of subuniverses. This means that its
subuniverse of modal types is $\mathcal{U}(M)$. By [24, Theorem 3.11, part
(i)], $M$ has a structural meet exactly if $\mathcal{U}_{M}$ admits a
reflection in $\mathcal{U}$. In that case, $\bigwedge M$ is given by the
reflection operation.

Given a family
$(M,M^{\prime}):I\to\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$, we
say that a given meet of $(M,M^{\prime})$ is structural if it is sent to
structural meets of $M$ and $M^{\prime}$ by the forgetful functors. Note that
$(M,M^{\prime})$ has a structural meet exactly if $M$ and $M^{\prime}$ have
structural meets $\bigwedge M$ and $\bigwedge M^{\prime}$, respectively, and
$\bigwedge M^{\prime}$ is an extension of $\bigwedge M$ to
$\mathcal{U}^{\prime}$. This unfolds to the following conditions:

  * •

the subuniverse $\mathcal{U}_{M}$ of $\mathcal{U}$ admits a reflection $L$,

  * •

the subuniverse $\mathcal{U}^{\prime}_{M^{\prime}}$ of $\mathcal{U}^{\prime}$
admits a reflection $L^{\prime}$,

  * •

for $X:\mathcal{U}$, the canonical map $L^{\prime}X\to LX$ is invertible.

When considering diagrams in a poset, we will restrict our attention to shapes
that are themselves posets. Note that in any poset, the limit of a (poset-
indexed) diagram coincides with the meet over the object components of the
diagram. Nonetheless, it is useful to speak about limits of diagrams because
this allows us to constrain the relations between the inputs objects.

A poset $I$ is _filtered_ if it is merely inhabited and for any two elements
$x_{0},x_{1}:I$, there merely exists $y:I$ with $x_{0},x_{1}\leq y$. It is
_cofiltered_ if $I^{\mathsf{op}}$ is filtered. The following statement
generalizes Theorem 1.15 to modalities.

######  Proposition A.4.

Let $(M,M^{\prime}):I\to\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$
be a $\mathcal{U}$-small cofiltered diagram. If $\mathcal{U}_{M_{i}}$ is
$M^{\prime}_{i}$-modal for all $i:I$, then
$\mathcal{U}(M):\mathcal{U}^{\prime}$ belongs to
$\mathcal{U}^{\prime}(M^{\prime})$.

###### Proof.

Given $i:I$, we have to show that $\mathcal{U}(M)$ is $M^{\prime}_{i}$-modal.
Because $I$ is cofiltered, we have

$\mathcal{U}(M)=\mathcal{U}\big{\lparen}(M_{j})_{j\leq i}\big{\rparen},$

so it suffices to show that $\mathcal{U}\big{\lparen}(M_{j})_{j\leq
i}\big{\rparen}$ is $M^{\prime}_{i}$-modal. By assumption,
$\mathcal{U}_{M_{j}}$ is $M^{\prime}_{j}$-modal, hence $M^{\prime}_{i}$-modal
for $j\leq i$. We now use that a type $X$ over $\mathcal{U}_{M_{i}}$
($M^{\prime}_{i}$-modal) is $M^{\prime}_{i}$-modal exactly if the map
$X\to\mathcal{U}_{M_{i}}$ is $M^{\prime}_{i}$-modal. Given that
$\mathcal{U}_{M_{j}}\to\mathcal{U}_{M_{i}}$ is $M^{\prime}_{i}$-modal for
$j\leq i$, it suffices to show that $\mathcal{U}\big{\lparen}(M_{j})_{j\leq
i}\big{\rparen}\to\mathcal{U}_{M_{i}}$ is $M^{\prime}_{i}$-modal. Observe that
the fibers of the latter embedding are products of the fibers of the former
embeddings. So the claim holds since modal types are closed under product
([24, Lemma 1.26]). ∎

######  Corollary A.5.

Let $(M,M^{\prime}):I\to\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$
be a $\mathcal{U}$-small cofiltered diagram with a structural meet $(\bigwedge
M,\bigwedge M^{\prime})$. If $\mathcal{U}_{M_{i}}$ is $M^{\prime}_{i}$-modal
for all $i:I$, then $\mathcal{U}_{\bigwedge M}$ is $\bigwedge
M^{\prime}$-modal.

###### Proof.

This is a direct consequence of Proposition A.4 and the definition of
structural meet. ∎

The following statement says that, up to the same size issues of Proposition
A.2, lex modalities are closed under structural cofiltered limits of
modalities. In particular, structural cofiltered limits of “size-polymorphic”
modalities whose actions on maps preserve smallness of fibers preserve left
exactness.

######  Corollary A.6.

In the situation of Corollary A.5, if $M^{\prime}_{i}$ is lex for $i:I$ and
preserves maps with $\mathcal{U}$-small fibers, then $\bigwedge M$ is lex and
$\bigwedge M^{\prime}$ preserves maps with $\mathcal{U}$-small fibers.

###### Proof.

This is the combination of Proposition A.2 and Corollary A.5. ∎

Finally, we specialize to the important case of accessible modalities.

######  Corollary A.7.

Let $M:I\to\mathsf{Modality}(\mathcal{U})$ be a $\mathcal{U}$-small cofiltered
diagram. If $M_{i}$ is lex and accessible for all $i:I$, then the meet
$\bigwedge M$ exists and also has these properties.

###### Proof.

Let $\mathcal{U}^{\prime}$ be a universe containing $\mathcal{U}$. Let
$(M,M^{\prime}):I\to\mathsf{Modality}(\mathcal{U}<\mathcal{U}^{\prime})$ be
the extension of $M$ given by [24, Theorem 3.36]. By [24, Theorem 3.29], the
meet of $(M,M^{\prime})$ exists, is structural, and $\bigwedge M$ is again
accessible. By [24, Theorem 3.11], $\mathcal{U}_{M_{i}}$ is
$M^{\prime}_{i}$-modal for $i:I$. Applying Corollary A.5,
$\mathcal{U}_{\bigwedge M}$ is $\bigwedge M^{\prime}$-modal. By [24, Theorem
3.29], this makes $\bigwedge M$ is lex. ∎

## References

  * [1] Peter Aczel.  On relating type theories and set theories.  In Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus, editors, Types for Proofs and Programs, International Workshop TYPES ’98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers, volume 1657 of Lecture Notes in Computer Science, pages 1–18. Springer, 1998.
  * [2] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata.  Cartesian cubical type theory.  Draft, December 2017.
  * [3] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler.  Two-level type theory and applications.  CoRR, abs/1705.03307, 2017.
  * [4] Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine.  Homotopy limits in type theory.  Math. Struct. Comput. Sci., 25(5):1040–1070, 2015.
  * [5] Michael Barr.  Toposes without points.  J. Pure Appl. Algebra, 5:265–280, 1974.
  * [6] Julia E. Bergner and Charles Rezk.  Reedy categories and the $\varTheta$-construction.  Math. Z., 274(1-2):499–514, 2013.
  * [7] Evert W. Beth.  Semantic Construction of Intuitionistic Logic.  Medededlingen der koninklijke Nederlandse Akademie van Wetenschappen, afd. Letterkunde. Nieuwe Reeks, Deel 19, No. 11. N. V. Noord-Hollandsche Uitgevers Maatschappij, Amsterdam, 1956.
  * [8] Simon Pierre Boulier.  Extending type theory with syntactic models. (Etendre la théorie des types à l’aide de modèles syntaxiques).  PhD thesis, Ecole nationale supérieure Mines-Télécom Atlantique Bretagne Pays de la Loire, France, 2018.
  * [9] 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, May 18-21, 2015, Tallinn, Estonia, volume 69 of LIPIcs, pages 5:1–5:34. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [10] Thierry Coquand, Simon Huber, and Anders Mörtberg.  On higher inductive types in cubical type theory.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255–264. ACM, 2018.
  * [11] Thierry Coquand, Bassel Mannaa, and Fabian Ruch.  Stack semantics of type theory.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–11. IEEE Computer Society, 2017.
  * [12] Thierry Coquand and Christine Paulin.  Inductively defined types.  In Per Martin-Löf and Grigori Mints, editors, COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer, 1988.
  * [13] 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, volume 1158 of Lecture Notes in Computer Science, pages 120–134. Springer, 1995.
  * [14] Samuel Eilenberg and J. A. Zilber.  Semi-simplicial complexes and singular homology.  Ann. of Math. (2), 51:499–513, 1950.
  * [15] A. Grothendieck.  Éléments de géométrie algébrique. I. Le langage des schémas.  Inst. Hautes Études Sci. Publ. Math., 4:228, 1960.
  * [16] Martin Hofmann.  Syntax and semantics of dependent types.  In Semantics and logics of computation (Cambridge, 1995), volume 14 of Publ. Newton Inst., pages 79–130. Cambridge Univ. Press, Cambridge, 1997.
  * [17] André Joyal.  Lettre à Grothendieck, 1984.
  * [18] Ambrus Kaposi, Simon Huber, and Christian Sattler.  Gluing for type theory.  In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 25:1–25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [19] Nicolai Kraus.  Truncation levels in homotopy type theory.  PhD thesis, University of Nottingham, UK, 2015.
  * [20] Saul A. Kripke.  Semantical analysis of intuitionistic logic. I.  In Formal Systems and Recursive Functions (Proc. Eighth Logic Colloq., Oxford, 1963), pages 92–130. North-Holland, Amsterdam, 1965.
  * [21] Bassel Mannaa and Thierry Coquand.  Dynamic Newton-Puiseux theorem.  J. Logic & Analysis, 5, 2013.
  * [22] 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, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 24:1–24:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  * [23] Kevin Quirin.  Lawvere-Tierney sheafification in Homotopy Type Theory. (Faisceautisation de Lawvere-Tierney en théorie des types homotopiques).  PhD thesis, École des mines de Nantes, France, 2016.
  * [24] Egbert Rijke, Michael Shulman, and Bas Spitters.  Modalities in homotopy type theory.  CoRR, abs/1706.07526, 2017.
  * [25] Christian Sattler.  The equivalence extension property and model structures.  CoRR, abs/1704.06911, 2017.
  * [26] Urs Schreiber and Michael Shulman.  Quantum gauge field theory in cohesive homotopy type theory.  In Ross Duncan and Prakash Panangaden, editors, Proceedings 9th Workshop on Quantum Physics and Logic, QPL 2012, Brussels, Belgium, 10-12 October 2012, volume 158 of EPTCS, pages 109–126, 2012.
  * [27] Dana S. Scott.  Relating theories of the $\lambda$-calculus.  In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 403–450. Academic Press, London-New York, 1980\.
  * [28] Michael Shulman.  The univalence axiom for elegant reedy presheaves, 2013.
  * [29] Michael Shulman.  Univalence for inverse diagrams and homotopy canonicity.  Mathematical Structures in Computer Science, 25(5):1203–1277, 2015\.
  * [30] Michael Shulman.  Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.  Mathematical Structures in Computer Science, 28(6):856–941, 2018\.
  * [31] Michael Shulman.  All $(\infty,1)$-toposes have strict univalent universes.  CoRR, abs/1904.07004, 2019.
  * [32] Andrew Swan and Taichi Uemura.  On Church’s thesis in cubical assemblies.  CoRR, abs/1905.03014, 2019.
  * [33] A. S. Troelstra and D. van Dalen.  Constructivism in mathematics. Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics.  North-Holland Publishing Co., Amsterdam, 1988.  An introduction.
  * [34] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  Institute for Advanced Study, 2013.
  * [35] Vladimir Voevodsky.  An experimental library of formalized mathematics based on the univalent foundations.  Mathematical Structures in Computer Science, 25(5):1278–1294, 2015\.
  * [36] Matthew Z. Weaver and Daniel R. Licata.  A constructive model of directed univalence in bicubical sets.  In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 915–928. ACM, 2020.
  * [37] Felix Wellen.  Formalizing Cartan Geometry in Modal Homotopy Type Theory.  PhD thesis, Karlsruher Institut für Technologie, Germany, 2017.