draft

# Categorical structures for type theory in univalent foundations

Benedikt Ahrens
<EMAIL_ADDRESS>Peter LeFanu Lumsdaine
<EMAIL_ADDRESS>Vladimir Voevodsky
<EMAIL_ADDRESS>
###### Abstract

In this paper, we analyze and compare three of the many algebraic structures
that have been used for modeling dependent type theories: _categories with
families_ , _split type-categories_ , and _representable maps of presheaves_.
We study these in the setting of univalent foundations, where the
relationships between them can be stated more transparently. We also introduce
_relative universes_ , generalizing the preceding notions.

We then analyze how these structures transfer along (weak and strong)
equivalences of categories, and, in particular, show how they descend from a
category (not assumed univalent/saturated) to its Rezk completion.

We work throughout in (intensional) dependent type theory; some results, but
not all, assume the univalence axiom. All the material of this paper has been
formalized in Coq, over the UniMath library.

#### Keywords.

.

###### keywords:

Categorical Semantics, Type Theory, Univalence Axiom

draft

###### Contents

  1. 1 Introduction
  2. 2 Background
    1. 2.1 Categorical structures for type theory
    2. 2.2 The agnostic, univalent, and classical settings
    3. 2.3 Comparing structures in the univalent setting
    4. 2.4 Categories in the univalent setting
  3. 3 Equivalence between categories with families and split type-categories
    1. 3.1 CwF’s and type-categories
    2. 3.2 Equivalence between CwF’s and split type-categories
  4. 4 Relative universes and a transfer construction
    1. 4.1 Relative universes and weak universes
    2. 4.2 Transfer constructions
  5. 5 Cwf structures, representable maps of presheaves and the Rezk completion
    1. 5.1 Representable maps of presheaves
    2. 5.2 CwF structures as relative universes
  6. 6 Guide to the accompanying formalization
  7. 7 Summary and future work

##  1 Introduction

Various kinds of categorical structures have been introduced in which to
interpret type theories: for instance, categories with families, C-systems,
categories with attributes, and so on. The aim of these structures is to
encompass and abstract away the structural rules of type theories—weakening,
substitution, and so on—that are independent of the specific logical type and
term formers of the type theory under consideration.

For a given kind of categorical structures and a given type theory one expects
furthermore to be able to build, from the syntax, an initial object of a
category or 2-category whose objects are categorical structures of this kind
equipped with suitable extra operations ‘modelling’ the type and term formers
of the type theory under consideration. This universal property then provides
a means to construct interpretations of the syntax, by assembling the objects
of the desired interpretation into another instance of such a structure.

It is natural to ask if, and in what sense, these various categorical
structures are equivalent, or otherwise related. The equivalences,
differences, and comparisons between them are often said to be well-known, but
few precise statements exist in the literature.

The goals of the present work are twofold. Firstly, to give some such
comparisons precisely and carefully. And secondly, to illustrate how in
univalent foundations, such comparisons can be approached in a different and
arguably more straightforward fashion than in classical settings.

More specifically, the paper falls into two main parts:

  * •

comparison between categories with families (CwF’s) and split type-categories;

  * •

interaction between CwF structures and Rezk completion of categories, and
comparison between CwF structures and representable maps of presheaves, all
via comparison with _relative universes_ (introduced in the present work).

Our constructions and equivalences may be summed up in the following diagram:

$\textstyle{\mathsf{splty}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{cwf}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relu}(\mathsf{y}_{{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{relu}(\mathsf{y}_{\mathsf{RC}({{\mathcal{C}}})})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{cwf}(\mathsf{RC}({{\mathcal{C}}}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{rep}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relwku}(\mathsf{y}_{{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relwku}(\mathsf{y}_{\mathsf{RC}({{\mathcal{C}}})})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{rep}(\mathsf{RC}({{\mathcal{C}}}))}$

All proofs and constructions of the article have been formalized in Coq, over
the UniMath library. We take this as licence to err on the side of indulgence
in focusing on the key ideas of constructions and suppressing less-
enlightening technical details, for which we refer readers to the
formalization. An overview the formalization is given in Section 6.
Throughout, we annotate results with their corresponding identifier in the
formalization, in teletype_font.

##  2 Background

###  2.1 Categorical structures for type theory

In this short section we briefly review some of the various categorical
structures for dependent type theory introduced in the literature. We do not
aim to give a comprehensive survey of the field, but just to recall what
pertains to the present paper.

The first introduced were Cartmell’s _contextual categories_ [Car78, Car86],
since studied by Voevodsky under the name of _C-systems_ [Voe16, Voe15].

Pitts [Pit00, Def. 6.3.3] introduced _split type-categories_ , originally just
as _type-categories_ ; Van den Berg and Garner [vdBG12, Def. 2.2.1] (whom we
follow here) later reorganized Pitts’ definition to isolate the splitness
conditions, and hence allow what they call _(non-split) type-categories_.
These have also been studied as _categories with attributes_ by Hofmann
[Hof97] and others.111Cartmell originally used the name _categories with
attributes_ for a slightly different notion [Car78, §3.2].

_Categories with families_ were defined by Dybjer [Dyb95] to make explicit the
data of _terms_ , not taken as primary in the previous approaches. A
functional variant of Dybjer’s definition, which we follow in the present
paper, was suggested by Fiore [Fio12, Appendix], and studied under the name
_natural models_ by Awodey [Awo16] (see also footnote to Def. 32 below).

The notions of _universes_ and _universe categories_ , which we generalize in
the present work to _universes relative to a functor_ , were introduced by
Voevodsky in [Voe15, Def. 2.1].

###  2.2 The agnostic, univalent, and classical settings

The background setting of the present work is intensional type theory,
assuming throughout: $\Sigma$-types, with the strong $\eta$ rule; identity
types; $\Pi$-types, also with $\eta$, and functional extensionality;
$\mathsf{0}$, $\mathsf{1}$, $\mathsf{2}$, and $\mathsf{N}$; propositional
truncation; and two universes.

All the above is _agnostic_ about equality on types—it is not assumed either
to be univalent, or to be always a proposition—and hence is expected to be
compatible with the interpretation of types as classical sets. In particular,
our main definitions of categorical structures use only this background
theory, and under the classical interpretation they become the established
definitions from the literature. Similarly, most of the comparison maps we
construct rely only on this, so can be understood in the classical setting.

Other results, however—essentially, all non-trivial equivalences of
types—assume additionally the univalence axiom; these therefore only make
sense in the univalent setting, and are not compatible with the classical
interpretation.

We mostly follow the type-theoretic vocabulary standardized in [Uni13]. A
brief, but sufficient, overview is given in [AKS15], among other places. By
$\mathsf{Set}$ we denote the category of h-sets of a fixed, but unspecified
universe.

We depart from it (and other type-theoretic traditions) in using _existence_
for what is called _mere existence_ in [Uni13] and _weak existence_ by Howard
[How80], since this is what corresponds to the standard mathematical usage of
_existence_.

###  2.3 Comparing structures in the univalent setting

Suppose one wishes to show that two kinds of mathematical object are
equivalent—say, one-object groupoids and groups. What precise statement should
one aim for?

In the classical setting, the most obvious candidate—a bijection of the sets
(or classes) of these objects—is not at all satisfactory. On the one hand, the
natural back-and-forth constructions may well fail to form a bijection. On the
other hand, the axiom of choice may imply that bijections exist even when the
objects involved are quite unrelated.

To give a more meaningful statement, one may define suitable morphisms, corral
the objects into two categories, and construct an equivalence of categories
between these. Sometimes, one needs to go further, and construct an
equivalence of higher categories, or spaces.

In the univalent setting, however, life is simpler. The most straightforward
candidate, an equivalence of _types_ between the types of the two kinds of
objects, is already quite satisfactory and meaningful, corresponding roughly
to an equivalence between the _groupoids_ of such objects in the classical
setting (or higher groupoids, etc.).

This is not to dismiss the value given by constructing (say) an equivalence of
categories However, defining the morphisms and so on is no longer _required_
in order to give a meaningful equivalence between the two kinds of objects.

Another advantage of a comparison in terms of equivalence of types is its
_uniformity_. Indeed, the one notion of equivalence of types can serve to
compare objects that naturally form the elements of sets, or the objects of
categories, or bicategories, etc.

In the present paper, therefore, we take advantage of this: two of our main
results are such equivalences, between the types of categories with families
and of split type-categories, and between the types of representable maps of
presheaves on a category ${\mathcal{C}}$, and of CwF structures on its Rezk
completion.

(We have focused here on equivalences, but the principle applies equally for
other comparisons: for instance, an injection of types carries more
information than an injection of sets/classes, corresponding roughly to a full
and faithful map of (possibly higher) groupoids.)

###  2.4 Categories in the univalent setting

The fundamentals of category theory were transferred to the univalent setting
in [AKS15]. Two primary notions of category are defined, there called
_precategories_ and _categories_. We change terminology, calling their
precategories _categories_ (since it is this that becomes the traditional
definition under the set interpretation), and their categories _univalent
categories_.

Specifically, a _category_ ${\mathcal{C}}$ (in our terminology) consists of:

  * •

a type ${\mathcal{C}}_{0}$, its _objects_ ;

  * •

for each $a,b:{\mathcal{C}}_{0}$, a set ${\mathcal{C}}(a,b)$, the _morphisms_
or _maps_ from $a$ to $b$;

  * •

together with identity and composition operations satisfying the usual axioms.

We emphasize that the hom-sets ${\mathcal{C}}(a,b)$ are required to be sets,
but ${\mathcal{C}}_{0}$ is allowed to be an arbitrary type.

In any category ${\mathcal{C}}$, there is a canonical map from equalities of
objects to isomorphisms,
$\mathsf{idtoiso}_{a,b}:(a=_{{\mathcal{C}}_{0}}b)\to\mathsf{Iso}_{{\mathcal{C}}}(a,b)$.
We say that ${\mathcal{C}}$ is _univalent_ if for all $a,b:{\mathcal{C}}_{0}$,
this map $\mathsf{idtoiso}_{a,b}$ is an equivalence: informally, if ‘equality
of objects is isomorphism’.

A central example is the category $\mathsf{Set}$ of sets (in some universe).
Univalence of this category follows directly from the univalence axiom for the
corresponding universe. It follows in turn that
$\mathsf{PreShv}({{\mathcal{C}}})$, the category of presheaves on a category
${\mathcal{C}}$, is also always univalent. We write
$\mathsf{y}_{{\mathcal{C}}}:{\mathcal{C}}\to\mathsf{PreShv}({{\mathcal{C}}})$
for the Yoneda embedding.

In properties of functors, we distinguish carefully between existence
properties and chosen data. We say a functor $F:{\mathcal{C}}\to{\mathcal{D}}$
is _essentially surjective_ if for each $d:{\mathcal{D}}_{0}$, there exist
some $c:{\mathcal{C}}_{0}$ and isomorphism $i:Fc\cong d$, and is _split
essentially surjective_ if it is equipped with an operation giving, for each
$d:{\mathcal{D}}_{0}$, some such $c$ and $i$. A _weak equivalence_ is a
functor that is full, faithful, and essentially surjective.

An important construction from [AKS15] is the _Rezk completion_
$\mathsf{RC}({{\mathcal{C}}})$ of a category ${\mathcal{C}}$, the ‘free’
univalent category on ${\mathcal{C}}$. Precisely,
$\mathsf{RC}({{\mathcal{C}}})$ is univalent, and there is a weak equivalence
$\eta_{{\mathcal{C}}}:{\mathcal{C}}\to\mathsf{RC}({{\mathcal{C}}})$, enjoying
the expected universal property: any functor from ${\mathcal{C}}$ to a
univalent category factorizes uniquely through $\eta_{{\mathcal{C}}}$.

$\textstyle{{\mathcal{C}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta}$$\scriptstyle{F}$$\textstyle{\mathsf{RC}({{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists!}$$\textstyle{{\mathcal{D}}\text{
univalent}}$

Note that the main definitions make sense in the agnostic background setting,
and under the classical interpretation become the standard definitions; but
the Rezk completion construction and the univalence of $\mathsf{Set}$ and
$\mathsf{PreShv}({{\mathcal{C}}})$ rely additionally on the univalence axiom.

As usual, we will write $f:a\to b$ for $f:{\mathcal{C}}(a,b)$ in arbitrary
categories, and will write $c:{\mathcal{C}}$ rather than
$c:{\mathcal{C}}_{0}$. We write composition in the ‘diagrammatic’ order; that
is, the composite of $f:a\to b$ and $g:b\to c$ is denoted ${f}\cdot{g}:a\to
c$.

##  3 Equivalence between categories with families and split type-categories

###  3.1 CwF’s and type-categories

For the most part, we take care to follow established definitions closely. We
depart from most literature however in one way: we do not take CwF’s or type-
categories (or other similar structures) to include a terminal object. This
does not interact in any way with the rest of the structure, so does not
affect the equivalences we construct below. We do this since both versions
(with and without terminal object) seem useful for the development of the
theory; and it is easier to equip objects with extra structure later than to
remove it.

######  Definition 1 ([Fio12, Appendix]; cwf_structure, cwf).

A _category with families (à la Fiore)_ consists of:

  1. 0.

a category ${\mathcal{C}}$, together with

  2. 1.

presheaves
$\mathsf{Ty},\mathsf{Tm}:{\mathcal{C}}^{\mathrm{op}}\to\mathsf{Set}$;

  3. 2.

a natural transformation $\mathsf{p}:\mathsf{Tm}\to\mathsf{Ty}$; and

  4. 3.

for each object $\Gamma:{\mathcal{C}}$ and $A:\mathsf{Ty}({\Gamma})$, a
representation of the fiber of $\mathsf{p}$ over $A$, i.e.

    1. (a)

an object ${\Gamma}.{A}:{\mathcal{C}}$ and map
$\mathsf{\pi}_{A}:{\Gamma}.{A}\to\Gamma$,

    2. (b)

an element $\mathsf{te}_{A}:\mathsf{Tm}({{\Gamma}.{A}})$, such that
$\mathsf{p}_{{\Gamma}.{A}}(\mathsf{te}_{A})=\mathsf{\pi}_{A}^{*}{A}:\mathsf{Tm}({\Gamma}.{A}),$

    3. (c)

and such that the induced commutative square

$\textstyle{\mathsf{y}({\Gamma}.{A})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widehat{\mathsf{te}_{A}}}$$\scriptstyle{\mathsf{y}(\mathsf{\pi}_{A})}$A$\textstyle{\mathsf{Tm}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{p}}$$\textstyle{\mathsf{y}(\Gamma)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widehat{A}}$$\textstyle{\mathsf{Ty}}$

is a pullback. (Here e.g. $\widehat{A}$ denotes the Yoneda transpose of an
element of a presheaf.)

By a _CwF structure_ on a category ${\mathcal{C}}$, we mean the data of items
1–3 above.

######  Remark.

This is a reformulation, due to Fiore, of Dybjer’s original definition of
CwF’s [Dyb95, Def. 1], replacing the single functor
${\mathcal{C}}\to\mathsf{Fam}$ by the map of presheaves
$\mathsf{p}:\mathsf{Tm}\to\mathsf{Ty}$.

######  Definition 2.

Let ${\mathcal{C}}$ be a CwF, $\Gamma:{\mathcal{C}}$ an object, and $e:A=B$ an
equality of elements of $\mathsf{Ty}({\Gamma})$. We write
$\Delta_{e}:{\Gamma}.{A}\cong{\Gamma}.{B}$ for the induced isomorphism
$\mathsf{idtoiso}(\mathsf{ap}_{x\mapsto{\Gamma}.{x}}(e))$.

Since $\mathsf{Ty}({\Gamma})$ is a set, we will sometimes suppress $e$ and
write just $\Delta_{A,B}$. We will also use this notation in other situations
with a family $\mathsf{Ty}$ and operation $\Gamma,A\mapsto{\Gamma}.{A}$ as in
a CwF.

######  Definition 3 ([Pit00]; typecat_structure, is_split_typecat,
split_typecat_structure).

A _type-category_ consists of:

  1. 0.

a category ${\mathcal{C}}$, together with

  2. 1.

for each object $\Gamma:{\mathcal{C}}$, a type $\mathsf{Ty}({\Gamma})$,

  3. 2.

for each $\Gamma:{\mathcal{C}}$ and $A:\mathsf{Ty}({\Gamma})$, an object
${\Gamma}.{A}:{\mathcal{C}}$

  4. 3.

for each such $\Gamma$, $A$, a morphism
$\mathsf{\pi}_{A}:{\Gamma}.{A}\to\Gamma$,

  5. 4.

for each map $f:\Gamma^{\prime}\to\Gamma$, a ‘reindexing’ function
$\mathsf{Ty}({\Gamma})\to\mathsf{Ty}({\Gamma^{\prime}})$, denoted $A\mapsto
f^{*}{A}$,

  6. 5.

for each $\Gamma$, $A:\mathsf{Ty}({\Gamma})$, and
$f:\Gamma^{\prime}\to\Gamma$, a morphism
$\mathsf{q}({f},{A}):{\Gamma^{\prime}}.{f^{*}{A}}\to{\Gamma}.{A}$,

  7. 6.

such that for each such $\Gamma$, $A$, $\Gamma^{\prime}$, $f$, the following
square commutes and is a pullback:

$\textstyle{{\Gamma^{\prime}}.{f^{*}{A}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{q}({f},{A})}$$\scriptstyle{\mathsf{\pi}_{f^{*}{A}}}$A$\textstyle{{\Gamma}.{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{\pi}_{A}}$$\textstyle{\Gamma^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{\Gamma}$

A type-category is _split_ if:

  1. 7.

for each $\Gamma$, the type $\mathsf{Ty}({\Gamma})$ is a set;

  2. 8.

for each $\Gamma$ and $A:\mathsf{Ty}({\Gamma})$, we have equalities

    1. (a)

$e:1_{\Gamma}^{*}{A}=A$, and

    2. (b)

$\mathsf{q}({1_{\Gamma}},{A})=\Delta_{e}\ :\
{\Gamma}.{1_{\Gamma}^{*}{A}}\to{\Gamma}.{A}$; and

  3. 9.

for $f^{\prime}:\Gamma^{\prime\prime}\to\Gamma^{\prime})$,
$f:\Gamma^{\prime}\to\Gamma$, and $A:\mathsf{Ty}({\Gamma})$, we have
equalities

    1. (a)

$e^{\prime}:({f^{\prime}}\cdot{f})^{*}{A}=f^{\prime*}{f^{*}{A}}$, and

    2. (b)

$\mathsf{q}({{f^{\prime}}\cdot{f}},{A})={{\Delta_{e^{\prime}}}\cdot{\mathsf{q}({f^{\prime}},{f^{*}{A}})}}\cdot{\mathsf{q}({f},{A})}\
:\ {\Gamma^{\prime\prime}}.{({f^{\prime}}\cdot{f})^{*}{A}}\to{\Gamma}.{A}.$

In the present work, we will only consider split type-categories. Non-split
type-categories are however also of great importance, especially in the
agnostic/univalent settings, since classical methods for constructing split
ones may no longer work.

###  3.2 Equivalence between CwF’s and split type-categories

The main goal of this section is to construct an equivalence of types between
the type of CwF’s and the type of split type-categories. In outline, we
proceed as follows:

Firstly, we specialize to giving an equivalence between CwF structures and
split type-category structures over a fixed base category ${\mathcal{C}}$.

Secondly, we further abstract out the shared part of these, decomposing them
into

  * •

_object extension structures_ , the shared structure common to CwF’s and split
type-categories, and

  * •

structures comprising the remaining data of CwF structures and split type-
category structures, which we call _term-structures_ and _$\mathsf{q}$
-morphism structures_ respectively.

Finally, we give an equivalence between term-structures and
$\mathsf{q}$-morphism structures over a given category and object extension
structure. We do this by defining a _compatibility_ relation between them, and
showing that for each term-structure there exists a unique compatible
$\mathsf{q}$-morphism structure, and vice versa.

|  |  |
---|---|---|---
$\textstyle{\displaystyle\sum_{X,Y,Z}\mathsf{compat}_{X}(Y,Z)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{splty}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\displaystyle\sum_{X:\mathsf{objext}({\mathcal{C}})}\\!\\!\\!\\!\mathsf{qmor}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\displaystyle\sum_{X:\mathsf{objext}({\mathcal{C}})}\\!\\!\\!\\!\mathsf{tmstr}(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{cwf}({\mathcal{C}})}$$\textstyle{\mathsf{objext}({\mathcal{C}})}$

######  Definition 4 (obj_ext_structure).

A _(split) object extension structure_ on a category ${\mathcal{C}}$ consists
of:

  1. 1.

a functor $\mathsf{Ty}:{\mathcal{C}}^{\mathrm{op}}\to\mathsf{Set}$;

  2. 2.

for each $\Gamma:{\mathcal{C}}$ and $A:\mathsf{Ty}({\Gamma})$,

    1. (a)

an object ${\Gamma}.{A}$, and

    2. (b)

a _projection_ morphism $\mathsf{\pi}_{A}:{\mathcal{C}}({\Gamma}.{A},\Gamma)$.

In general, one might want to loosen the setness and functoriality conditions
on $\mathsf{Ty}$, and hence distinguish the present definition as the split
version of a more general notion. In this paper, however, we do not consider
the non-split case, so take _object extension structures_ to mean the split
ones throughout.

######  Definition 5 (term_fun_structure).

Let ${\mathcal{C}}$ be a category equipped with an object extension structure
$X$. A _(functional) term-structure_ over $X$ consists of:

  1. 1.

a presheaf $\mathsf{Tm}:{\mathcal{C}}^{\mathrm{op}}\to\mathsf{Set}$, and
natural transformation $\mathsf{p}:\mathsf{Tm}\to\mathsf{Ty}$;

  2. 2.

for each object $\Gamma:{\mathcal{C}}$ and $A:\mathsf{Ty}({\Gamma})$, an
element $\mathsf{te}_{A}:\mathsf{Tm}({{\Gamma}.{A}})$, such that
$({\Gamma}.{A},\mathsf{\pi}_{A},\mathsf{te}_{A})$ form a representation of the
fiber of $\mathsf{p}$ over $A$ as in item 3 of Def. 1.

One might say _functional_ to distinguish these from _familial_ term-
structures, which would correspond analogously to CwF’s in the sense of
Dybjer, with $\mathsf{Tm}({\Gamma})$ a family indexed by
$\mathsf{Ty}({\Gamma})$. For the present paper, however, we work only with the
functional ones, so call these simply _term-structures_.

######  Problem 6.

Given a category ${\mathcal{C}}$, to construct an equivalence between CwF
structures on ${\mathcal{C}}$ and pairs $(X,Y)$ of an object extension
structure $X$ on ${\mathcal{C}}$ and a term-structure $Y$ over $X$.

######  Construction 7 (for Problem 6; weq_cwf_cwf'_structure).

Mathematically, this is essentially trivial, as is visibly evident from the
definitions: just a matter of reordering and reassociating $\Sigma$-types, and
distributing $\Pi$-types over $\Sigma$-types. It is perhaps worth noting
however that this distributivity requires functional extensionality. ∎

######  Definition 8 (qq_morphism_structure).

Let ${\mathcal{C}}$ be a category equipped with an object extension structure
$X$. A _(split) $\mathsf{q}$-morphism structure_ over $X$ consists of:

  1. 1.

for each $f:\Gamma^{\prime}\to\Gamma$ and $A:\mathsf{Ty}({\Gamma})$, a map
$\mathsf{q}({f},{A}):{\Gamma}.{A}\to\Gamma$, such that following square
commutes and is a pullback

$\textstyle{{\Gamma^{\prime}}.{f^{*}{A}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{q}({f},{A})}$$\scriptstyle{\mathsf{\pi}_{f^{*}{A}}}$A$\textstyle{{\Gamma}.{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{\pi}_{A}}$$\textstyle{\Gamma^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{\Gamma}$

and such that

  2. 2.

for each $\Gamma$ and $A:\mathsf{Ty}({\Gamma})$,
$\mathsf{q}({1_{\Gamma}},{A})=\Delta_{1_{\Gamma}^{*}{A},A}\ :\
{\Gamma}.{1_{\Gamma}^{*}{A}}\to{\Gamma}.{A}$; and

  3. 3.

for each $f^{\prime}:\Gamma^{\prime\prime}\to\Gamma^{\prime}$,
$f:\Gamma^{\prime}\to\Gamma$, and $A:\mathsf{Ty}({\Gamma})$,

$\mathsf{q}({{f^{\prime}}\cdot{f}},{A})={{\Delta_{({f^{\prime}}\cdot{f})^{*}{A},f^{\prime*}{f^{*}{A}}}}\cdot{\mathsf{q}({f^{\prime}},{f^{*}{A}})}}\cdot{\mathsf{q}({f},{A})}\
:\ {\Gamma^{\prime\prime}}.{({f^{\prime}}\cdot{f})^{*}{A}}\to{\Gamma}.{A}.$

Here the suppressed equalities on the $\Delta$ terms come from the
functoriality axioms of $\mathsf{Ty}$.

######  Problem 9.

Given a category ${\mathcal{C}}$, to construct an equivalence between split
type-category structures on ${\mathcal{C}}$ and pairs $(X,Z)$ of an object
extension structure $X$ on ${\mathcal{C}}$ and a $\mathsf{q}$-morphism
structure $Z$ over $X$.

######  Construction 10 (for Problem 9; weq_standalone_to_regrouped).

Much like Construction 7, simply a matter of wrangling $\Pi$\- and
$\Sigma$-types. ∎

For most of the remainder of this section, we fix a category ${\mathcal{C}}$
and object extension structure $X$ on ${\mathcal{C}}$. We can now explicitly
define constructions going back and forth between term-structures and
$\mathsf{q}$-morphism structures over $X$, preparatory to showing that they
form an equivalence. Before we do so, we define the _compatibility_ relation
between them.

######  Definition 11.

Let $Y$ be a term-structure and $Z$ a $\mathsf{q}$-morphism structure over
$X$. Say that $Y$ and $Z$ are _compatible_ if for all
$f:\Gamma\to\Gamma^{\prime}$ and $A:\mathsf{Ty}({\Gamma})$,
$\mathsf{te}_{f^{*}{A}}=\mathsf{q}({f},{A})^{*}{\mathsf{te}_{A}}$.

######  Problem 12.

Given a term-structure $Y$ over $X$, to construct a $\mathsf{q}$-morphism
structure over $X$ compatible with $Y$.

######  Construction 13 (for Problem 12; compatible_qq_from_term).

Given $Y$ and $f:\Gamma\to\Gamma^{\prime}$ and $A:\mathsf{Ty}({\Gamma})$, the
term-structure axioms give a pullback square

$\textstyle{{\mathcal{C}}({\Gamma^{\prime}}.{f^{*}{A}},{\Gamma}.{A})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g\mapsto
g^{*}{\mathsf{te}_{A}}}$$\scriptstyle{{-}\cdot{\mathsf{\pi}_{A}}}$A$\textstyle{\mathsf{Tm}({{\Gamma^{\prime}}.{f^{*}{A}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{p}_{{\Gamma^{\prime}}.{f^{*}{A}}}}$$\textstyle{{\mathcal{C}}({\Gamma^{\prime}}.{f^{*}{A}},\Gamma)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g\mapsto
g^{*}{A}}$$\textstyle{\mathsf{Ty}({{\Gamma^{\prime}}.{f^{*}{A}}})}$

So we may take $\mathsf{q}({f},{A})$ to be the unique map
${\Gamma^{\prime}}.{f^{*}{A}}\to{\Gamma}.{A}$ such that
${\mathsf{q}({f},{A})}\cdot{\mathsf{\pi}_{A}}={\mathsf{\pi}_{f^{*}{A}}}\cdot{f}$
and $\mathsf{q}({f},{A})^{*}{\mathsf{te}_{A}}=\mathsf{te}_{f^{*}{A}}$.
Verification that this forms a compatible $\mathsf{q}$-morphism structure is
essentially routine calculation. ∎

######  Problem 14.

Given a $\mathsf{q}$-morphism structure $Y$ over $X$, to construct a term-
structure over $X$ compatible with $Y$.

######  Construction 15 (for Problem 14; compatible_term_from_qq).

This construction is rather more involved; we only sketch it here, and refer
to the formalization for full details.

Briefly, $\mathsf{Tm}({\Gamma})$ is the set of pairs $(A,s)$, where
$A:\mathsf{Ty}({\Gamma})$, and $s:\Gamma\to{\Gamma}.{A}$ is a section of
$\mathsf{\pi}_{A}$. Its functorial action $f^{*}{}$ involves pulling back
sections along the pullback squares given by the $\mathsf{q}$-morphism
structure. Finally, the universal element
$\mathsf{te}_{A}:\mathsf{Tm}({\Gamma})$ is the pair
$(\mathsf{\pi}_{A}^{*}{A},\delta_{\mathsf{\pi}_{A}})$, where
$\delta_{\mathsf{\pi}_{A}}:{\Gamma}.{A}\to{{\Gamma}.{A}}.{\mathsf{\pi}_{A}^{*}{A}}$
is the diagonal map of the pullback square for $A$ and $\mathsf{\pi}_{A}$
given by the $\mathsf{q}$-morphism structure. ∎

######  Problem 16.

(Assuming Univalence.) To give an equivalence between term-structures and
$\mathsf{q}$-morphism structures over $X$, whose underlying functions are as
given in the two preceding constructions.

From this equivalence, to derive an equivalence between the type of pairs
$(X,Y)$ of an object extension structure and a term-structure, and of pairs
$(X,Z)$ an object extension structure and a $\mathsf{q}$-morphism structure.

######  Construction 17 (for Problem 16; weq_cwf'_sty').

As intimated above, we proceed by showing that for each term-structure, the
compatible $\mathsf{q}$-morphism structure constructed above is in fact the
_unique_ compatible such structure, and vice versa.

This equivalence immediately induces an equivalence of pair types, which is
the identity on the first component carrying the object extension structure.

Note in particular that for this result—unlike in the constructions above—we
rely essentially on the univalence axiom. ∎

######  Problem 18.

To construct an equivalence between cwf structures and split type-category
structures on a category ${\mathcal{C}}$.

######  Construction 19 (for Problem 18; weq_sty_cwf).

By composing the equivalences of Constructions 7, 10, and 17. ∎

The back-and-forth constructions above (though not compatibility) are also
sketched in e.g. [Hof97, Sections 3.1, 3.2] (note that Hofmann’s _categories
with attributes_ are what we call _split type-categories_). Hofmann also
mentions that—in our terminology—going from $\mathsf{q}$-morphism structures
to term-structures and back yields the original $\mathsf{q}$-morphism
structure. However, working in set-theoretic foundations, the same is not true
for the other direction—the original term presheaf is not recovered up to
equality. This is exactly where the univalence axiom comes to our rescue: it
allows us to conclude that, by showing that the obtained term presheaf is
_isomorphic_ to the original one, the two are identical. Hence we obtain an
equivalence of types. Note however that our proof that the maps are indeed an
equivalence is slightly different, to avoid the difficult direct construction
of an identity between two term-structures.

In the absence of the univalence axiom, the constructed maps back and forth
can still be used to compare term-structures and $\mathsf{q}$-morphism
structures: by defining suitable notions of morphisms of those structures,
these maps underlie an equivalence of categories. We have also formalized this
equivalence of categories, and will report on it in a forthcoming article.

##  4 Relative universes and a transfer construction

In this section we introduce the notion of _universes relative to a functor
$J:{\mathcal{C}}\to{\mathcal{D}}$_. This notion generalizes the universes
studied in [Voe15], and is inspired by the generalization of monads to
relative monads [ACU15].

###  4.1 Relative universes and weak universes

######  Definition 20 (fpullback).

Let $J:{\mathcal{C}}\to{\mathcal{D}}$ be a functor, and
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ a morphism of ${\mathcal{D}}$.

Given an object $X$ of ${\mathcal{C}}$ and morphism $f:J(X)\to\mathsf{U}$ in
${\mathcal{D}}$, a _$J$ -pullback of $\mathsf{p}$ along $f$_ consists of an
object $X^{\prime}$ of ${\mathcal{C}}$ and morphisms $p^{\prime}:X^{\prime}\to
X$ and $Q:J(X^{\prime})\to\mathsf{\tilde{U}}$, such that the following square
commutes and is a pullback:

$\textstyle{J(X^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q}$$\scriptstyle{J(p^{\prime})}$A$\textstyle{\mathsf{\tilde{U}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{p}}$$\textstyle{J(X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{\mathsf{U}}$

######  Definition 21 (relative_universe, weak_relative_universe).

Let $J:{\mathcal{C}}\to{\mathcal{D}}$ be a functor, as above.

A _$J$ -universe structure_ on a map
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ of ${\mathcal{D}}$ is a function
giving, for each object $X$ in ${\mathcal{C}}$ and map $f:J(X)\to\mathsf{U}$,
a $J$-pullback $({X}.{f},\mathsf{p}_{f},\mathsf{Q}({X},{f}))$ of $\mathsf{p}$
along $f$. A _universe relative to $J$_, or briefly a _$J$ -relative
universe_, is a map $\mathsf{p}$ equipped with a $J$-universe structure.

A _weak universe relative to $J$_ is a map
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ such that for all suitable $X$,
$f$, there exists some $J$-pullback of $\mathsf{p}$ along $f$.

A _universe_ in ${\mathcal{C}}$, as defined in [Voe15], is exactly a universe
relative to the identity functor $\mathsf{Id}_{{\mathcal{C}}}$. We will see in
Section 5 that universes relative to the Yoneda embedding
$\mathsf{y}_{{\mathcal{C}}}:{\mathcal{C}}\to\mathsf{PreShv}({{\mathcal{C}}})$
correspond precisely to CwF structures on ${\mathcal{C}}$.

######  Lemma 22 (isaprop_rel_universe_structure).

Suppose $J:{\mathcal{C}}\to{\mathcal{D}}$ is full and faithful, and
${\mathcal{C}}$ is univalent. Then for any morphism
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ in ${\mathcal{D}}$, and object
$X:{\mathcal{C}}$ and $f:J(X)\to\mathsf{U}$, the type of $J$-pullbacks of
$\mathsf{p}$ along $f$ is a proposition. Similarly, for any such $\mathsf{p}$,
the type of $J$-universe structures on $\mathsf{p}$ is a proposition.

###### Proof.

The first statement is similar to the argument that pullbacks in univalent
categories are unique. The second follows directly from the first. ∎

######  Corollary 23 (weq_relative_universe_weak_relative_universe).

When $J:{\mathcal{C}}\to{\mathcal{D}}$ is fully faithful and ${\mathcal{C}}$
is univalent, the forgetful function from universes to weak universes relative
to $J$ is an equivalence.

###  4.2 Transfer constructions

We give three constructions for transferring (weak) relative universes from
one functor to another. The first, with all data assumed to be given
explicitly, is the most straightforward. However, it does not suffice for
transfers to the Rezk completion, since the embedding
$\eta_{{\mathcal{C}}}:{\mathcal{C}}\to\mathsf{RC}({{\mathcal{C}}})$ is only a
weak equivalence, not in general _split_ essentially surjective. The second
and third constructions are therefore adaptations of the first to require only
essential surjectivity.

######  Problem 24.

Given a square of functors commuting up to natural isomorphism, as in

$\textstyle{{\mathcal{C}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\alpha}$$\scriptstyle{J}$$\scriptstyle{R}$$\textstyle{{\mathcal{D}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S}$$\textstyle{{\mathcal{C}}^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{J^{\prime}}$$\textstyle{{\mathcal{D}}^{\prime},}$

such that

  * •

$S$ preserves pullbacks,

  * •

$S$ is split full, and

  * •

$R$ is split essentially surjective,

and given a $J$-relative universe structure on a map
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ in ${\mathcal{D}}$, to construct
a $J^{\prime}$-universe structure on $S(\mathsf{p})$ in
${\mathcal{D}}^{\prime}$.

######  Construction 25 (for Problem 24;
rel_universe_structure_induced_with_ess_split).

Given $X$ in ${\mathcal{C}}^{\prime}$ and $f:J^{\prime}(X)\to S\mathsf{U}$, we
need to construct a $J^{\prime}$-pullback of $S(\mathsf{p})$ along $f$.

Split essential surjectivity of $R$ gives some $\bar{X}:{\mathcal{C}}$ and
isomorphism $i:R(\bar{X})\cong X$. We therefore have
${\alpha_{\bar{X}}}\cdot{{J^{\prime}i}\cdot{f}}:SJ\bar{X}\to S\mathsf{U}$; so
split fullness of $S$ gives us some $\bar{f}:J\bar{X}\to\mathsf{U}$ with
$S\bar{f}={\alpha_{\bar{X}}}\cdot{{J^{\prime}i}\cdot{f}}$. Taking the given
$J$-pullback of $\mathsf{p}$ along $\bar{f}$ and mapping it forward under $S$,
we get a pullback square in ${\mathcal{D}}^{\prime}$:

$\textstyle{SJ({\bar{X}}.{\bar{f}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S(\mathsf{Q}({\bar{X}},{\bar{f}}))}$$\scriptstyle{SJ\mathsf{p}_{\bar{f}}}$A$\textstyle{S\mathsf{\tilde{U}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S\mathsf{p}}$$\textstyle{SJ\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{\bar{X}}}$$\textstyle{J^{\prime}R\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{J^{\prime}i}$$\textstyle{J^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{S\mathsf{U}}$

The maps ${R(\mathsf{p}_{\bar{f}})}\cdot{i}:R({\bar{X}}.{\bar{f}})\to X$ and
${\alpha_{{\bar{X}}.{\bar{f}}}^{-1}}\cdot{S(\mathsf{Q}({\bar{X}},{\bar{f}}))}:J^{\prime}R({\bar{X}}.{\bar{f}})\to
S\mathsf{\tilde{U}}$ now give the desired $J^{\prime}$-pullback of
$S\mathsf{p}$ along $f$, since the square they give—the right-hand square
below—is isomorphic to the pullback obtained above.

$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
23.13959pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{SJ({\bar{X}}.{\bar{f}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
28.71638pt\raise 5.6425pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-0.3714pt\hbox{$\scriptstyle{\alpha_{{\bar{X}}.{\bar{f}}}}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
32.8859pt\raise-6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 55.88544pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.25612pt\hbox{$\scriptstyle{SJ\mathsf{p}_{\bar{f}}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-29.80554pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
55.88544pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}R({\bar{X}}.{\bar{f}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
111.40814pt\raise 5.25555pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.25555pt\hbox{$\scriptstyle{1}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
110.53314pt\raise-6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 134.15814pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
77.02179pt\raise-19.81943pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.81168pt\hbox{$\scriptstyle{J^{\prime}R\mathsf{p}_{\bar{f}}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
77.02179pt\raise-28.24998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
134.15814pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}R({\bar{X}}.{\bar{f}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
182.66118pt\raise 6.97444pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.70334pt\hbox{$\scriptstyle{{\alpha_{{\bar{X}}.{\bar{f}}}^{-1}}\cdot{S(\mathsf{Q}({\bar{X}},{\bar{f}}))}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 255.40306pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
155.2945pt\raise-19.81943pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.81168pt\hbox{$\scriptstyle{J^{\prime}({R(\mathsf{p}_{\bar{f}})}\cdot{i})}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
155.2945pt\raise-28.24998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
160.8906pt\raise-7.15111pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{\text{\pigpenfont
A}}$}}}}}\ignorespaces{}{\hbox{\kern 212.43085pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 255.40306pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{S\mathsf{\tilde{U}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
264.535pt\raise-19.81943pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{S\mathsf{p}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
264.535pt\raise-29.80554pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{SJ\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
31.27194pt\raise-33.99635pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-0.3714pt\hbox{$\scriptstyle{\alpha_{\bar{X}}}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
32.8859pt\raise-45.78885pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
63.66324pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
63.66324pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}R\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
109.12492pt\raise-33.69164pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.94722pt\hbox{$\scriptstyle{J^{\prime}i}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
110.53314pt\raise-45.78885pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
143.73631pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
143.73631pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
204.82446pt\raise-33.52776pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
254.43085pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
212.43085pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern
254.43085pt\raise-39.63885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{S\mathsf{U}}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\\[0.0pt]
\end{gathered}\qed$

######  Problem 26.

Given a square of functors as in Problem 24, such that

  * •

$S$ preserves pullbacks,

  * •

$S$ is full,

  * •

$R$ is essentially surjective,

  * •

${\mathcal{C}}^{\prime}$ is univalent,

  * •

$J^{\prime}$ is fully faithful,

and given a $J$-relative universe structure on a map
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ in ${\mathcal{D}}$, to construct
a $J^{\prime}$-universe structure on $S(\mathsf{p})$ in
${\mathcal{D}}^{\prime}$.

######  Construction 27 (for Problem 26;
rel_universe_structure_induced_with_ess_surj).

Mostly the same as Construction 25. The only problematic steps are finding
$(\bar{X},i)$ and $\bar{f}$ as above, since the hypotheses which provided them
there have now been weakened to existence properties. However, our new
hypotheses that ${\mathcal{C}}^{\prime}$ is univalent and $J^{\prime}$ fully
faithful allow us to apply Lemma 22 to see that the goal of a
$J^{\prime}$-pullback is a proposition; so the existence properties do in fact
suffice. ∎

######  Lemma 28 (is_universe_transfer).

Suppose given a square of functors as in Problem 24, such that

  * •

$S$ preserves pullbacks,

  * •

$S$ is full,

  * •

$R$ is essentially surjective.

If $\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ in ${\mathcal{D}}$ is a weak
$J$-relative universe in ${\mathcal{C}}$, then $S(\mathsf{p})$ is a weak
$J^{\prime}$-relative universe in ${\mathcal{D}}^{\prime}$.

###### Proof.

Again, mostly the same as Construction 25. Now our goal is just to show, for
each suitable $X$, $f$, that there exists some $J^{\prime}$-pullback of
$S\mathsf{p}$ along $f$. This is by construction a proposition; so, again, we
can obtain objects from our existence hypotheses whenever required. ∎

######  Lemma 29 (isweq_is_universe_transfer).

Given functors satisfying the hypotheses of Lemma 28, if additionally $R$ is
full and $S$ is faithful, then a map
$\mathsf{p}:\mathsf{\tilde{U}}\to\mathsf{U}$ in ${\mathcal{D}}$ is a weak
$J$-relative universe if and only if $S(\mathsf{p})$ is a weak
$J^{\prime}$-relative universe.

###### Proof.

One implication is exactly Lemma 28. For the other, assume that
$S(\mathsf{p})$ is a weak $J^{\prime}$-relative universe; we must show that
$\mathsf{p}$ is a weak $J$-relative universe.

Given $X:{\mathcal{C}}$ and $f:J(X)\to\mathsf{U}$, we need to show there
exists a $J$-pullback for $\mathsf{p}$ along $f$. Since the goal is just
existence, we can take witnesses for existence hypotheses as needed. In
particular, we can take some $X^{\prime}:{\mathcal{C}}^{\prime}$,
$p^{\prime}:X^{\prime}\to RX$ and $Q:J^{\prime}X^{\prime}\to
S\mathsf{\tilde{U}}$ forming a $J$-pullback for $S\mathsf{p}$ along
${\alpha^{-1}_{X}}\cdot{Sf}:J^{\prime}RX\to S\mathsf{U}$.

By essential surjectivity of $R$, we can find some
$\bar{X}^{\prime}:{\mathcal{C}}$ and isomorphism $i:R\bar{X}^{\prime}\cong
X^{\prime}$; and similarly by its fullness, we can take some arrow
$\bar{p}^{\prime}:\bar{X}^{\prime}\to X$ such that
$R(\bar{p}^{\prime})={i}\cdot{p^{\prime}}$. Finally, fullness of $S$ gives a
map $\bar{Q}:J\bar{X}^{\prime}\to\mathsf{\tilde{U}}$ with
$S\bar{Q}={\alpha_{\bar{X}^{\prime}}}\cdot{{J^{\prime}i}\cdot{Q}}$.

But now $(\bar{X}^{\prime},\bar{p}^{\prime},\bar{Q})$ form a $J$-pullback for
$\mathsf{p}$ along $f$, since under $S$, the square they give becomes
isomorphic to the original $J^{\prime}$-pullback square of
$(X^{\prime},p^{\prime},Q)$, and $S$ reflects limits, as it is full and
faithful.

$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
21.35068pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{SJ\bar{X}^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
23.82413pt\raise 5.86472pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-0.14917pt\hbox{$\scriptstyle{\alpha_{\bar{X}^{\prime}}}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
25.87808pt\raise-6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 48.87762pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.39444pt\hbox{$\scriptstyle{SJ{\bar{p}^{\prime}}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-28.55554pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
48.87762pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}R\bar{X}^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
87.2013pt\raise 5.94722pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.94722pt\hbox{$\scriptstyle{J^{\prime}i}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
88.60951pt\raise-6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 113.1347pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
39.88222pt\raise-19.19443pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.39444pt\hbox{$\scriptstyle{J^{\prime}R\bar{p}^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
63.00616pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
113.1347pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
148.9121pt\raise 6.07222pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{Q}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 174.76326pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
125.46288pt\raise-19.19443pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.26668pt\hbox{$\scriptstyle{J^{\prime}p^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
125.46288pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
127.28436pt\raise-4.64767pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{\text{\pigpenfont
A}}$}}}}}\ignorespaces{}{\hbox{\kern 174.76326pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{S\mathsf{\tilde{U}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
183.8952pt\raise-19.19443pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.71112pt\hbox{$\scriptstyle{S\mathsf{p}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
183.8952pt\raise-28.55554pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{SJ\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
24.45024pt\raise-33.19858pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-0.82361pt\hbox{$\scriptstyle{\alpha_{X}}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
25.87808pt\raise-44.53885pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
49.64761pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
49.64761pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}R\bar{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
89.48451pt\raise-33.1333pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.25555pt\hbox{$\scriptstyle{1}$}}}\kern
3.0pt}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
88.60951pt\raise-44.53885pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\cong}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
113.9047pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
113.9047pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{J^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
142.363pt\raise-32.27496pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.74722pt\hbox{$\scriptstyle{{\alpha^{-1}_{X}}\cdot{Sf}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
173.79105pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
173.79105pt\raise-38.38885pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{S\mathsf{U}}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\\[0.0pt]
\end{gathered}\qed$

######  Problem 30.

Given a square of functors as in Problem 24, such that

  * •

${\mathcal{D}}$ and ${\mathcal{D}}^{\prime}$ are both univalent,

  * •

$S$ is an equivalence, and

  * •

$R$ is essentially surjective and full,

to construct an equivalance between weak $J$-relative universes and weak
$J^{\prime}$-relative universes.

######  Construction 31 (for Problem 30; weq_weak_relative_universe_transfer).

The equivalence $S$ of univalent categories induces an equivalence between
morphisms in ${\mathcal{D}}$ and in ${\mathcal{D}}^{\prime}$. Lemma 29 implies
that this restricts to an equivalence between weak relative universes as
desired. ∎

##  5 Cwf structures, representable maps of presheaves and the Rezk completion

In this section, we show that CwF structures can be seen as relative
universes, and hence apply the results of the previous section to transfer CwF
structures along weak equivalences of categories: in particular, from a
category to its Rezk completion.

We also consider _representable maps of presheaves_ , corresponding similarly
to relative _weak_ universes, and use the results on relative universes to
elucidate their relationship to CwF structures.

The resulting transfers and relationships are summed up in the following
diagram, whose vertical maps all simply forget chosen structure:

$\textstyle{\mathsf{cwf}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relu}(\mathsf{y}_{{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{relu}(\mathsf{y}_{\mathsf{RC}({{\mathcal{C}}})})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{cwf}(\mathsf{RC}({{\mathcal{C}}}))\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{rep}({\mathcal{C}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relwku}(\mathsf{y}_{{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{relwku}(\mathsf{y}_{\mathsf{RC}({{\mathcal{C}}})})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\textstyle{\mathsf{rep}(\mathsf{RC}({{\mathcal{C}}}))}$

###  5.1 Representable maps of presheaves

######  Definition 32 (rep_map).

A map $\mathsf{p}:\mathsf{Tm}\to\mathsf{Ty}$ of presheaves on a category
${\mathcal{C}}$ is _representable_ if for each for each $\Gamma:{\mathcal{C}}$
and $A:\mathsf{Ty}({\Gamma})$, there exists some representation of the fiber
of $\mathsf{p}$ over $A$, i.e. some $\mathsf{\pi}_{A}:{\Gamma}.{A}\to\Gamma$
and $\mathsf{te}_{A}\in\mathsf{Tm}({{\Gamma}.{A}})$ satisfying the conditions
of Definition 1, item 3.222Note that in [Awo16], Awodey takes _representable
map_ to mean what we call a CwF structure, i.e. to include choices of
representations of the fibers; cf. [Awo16, §1.1, Algebraic character].

In other words, a representable map of presheaves on ${\mathcal{C}}$ is just
like a CwF structure, except that the representations are merely assumed to
exist, not included as chosen data.

Evidently, the underlying map $\mathsf{p}:\mathsf{Ty}\to\mathsf{Tm}$ of any
CwF structure is representable, just by forgetting its chosen representations.
This can sometimes be reversed:

######  Lemma 33 (isweq_from_cwf_to_rep).

If ${\mathcal{C}}$ is a univalent category, then the forgetful map from CwF
structures to representable maps of presheaves on ${\mathcal{C}}$ is an
equivalence. That is, any representable map of presheaves on ${\mathcal{C}}$
carries a unique choice of representing data.

###### Proof.

If suffices to show that for a given map
$\mathsf{p}:\mathsf{Tm}\to\mathsf{Ty}$, and for any $\Gamma:{\mathcal{C}}$ and
$A:\mathsf{Ty}({\Gamma})$, representing data
$({\Gamma}.{A},\mathsf{\pi}_{A},\mathsf{te}_{A})$ for the fiber is unique if
it exists.

Such data is always unique up to isomorphism, for any category
${\mathcal{C}}$, since pullbacks are unique up to isomorphism and
$\mathsf{y}_{{\mathcal{C}}}$ is full and faithful. But when ${\mathcal{C}}$ is
univalent, this uniqueness up to isomorphism can be translated into literal
uniqueness, as required.

(Alternatively, following Constructions 35 and 37 below, we could see this
result as essentially a special case of Corollary 23 on universe structures.)
∎

###  5.2 CwF structures as relative universes

In order to apply the transfer results of the previous section, we first
establish the equivalences between CwF structures on a category
${\mathcal{C}}$ (resp. representable maps of presheaves) and relative (weak)
universes on $\mathsf{y}_{{\mathcal{C}}}$.

######  Problem 34.

Given a category ${\mathcal{C}}$, to construct an equivalence between
$\mathsf{cwf}({\mathcal{C}})$ and $\mathsf{relu}(\mathsf{y}_{{\mathcal{C}}})$.

######  Construction 35 (for Problem 34; weq_cwf_structure_RelUnivYo).

This is a matter of reassociating components, and replacing two
quantifications over elements of a presheaf—once over $\mathsf{Ty}({\Gamma})$,
once over $\mathsf{Tm}({{\Gamma}.{A}})$—by quantification over the respective
isomorphic sets of natural transformations into $\mathsf{Ty}$ and
$\mathsf{Tm}$. ∎

######  Problem 36.

Given a category ${\mathcal{C}}$, to construct an equivalence between
$\mathsf{rep}({\mathcal{C}})$ and
$\mathsf{relwku}(\mathsf{y}_{{\mathcal{C}}})$.

######  Construction 37 (for Problem 36; weq_rep_map_weakRelUnivYo).

Similar to Construction 35. ∎

Next, we make use of this to transfer CwF structures and representable maps
along weak equivalences, by viewing them as relative (weak) universes and
applying the transfer results for those.

######  Problem 38.

Given a weak equivalence $F:{\mathcal{C}}\to{\mathcal{D}}$, where
${\mathcal{D}}$ is univalent, to construct a map
$\mathsf{cwf}({\mathcal{C}})\to\mathsf{cwf}({\mathcal{D}})$.

######  Construction 39 (for Problem 38; transfer_cwf_weak_equivalence).

We construct a map
$\mathsf{relu}(\mathsf{y}_{{\mathcal{C}}})\to\mathsf{relu}(\mathsf{y}_{{\mathcal{D}}})$
and obtain the desired map by composition with the equivalence constructed in
Construction 35. Consider the diagram

$\textstyle{{\mathcal{C}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\alpha}$$\scriptstyle{\mathsf{y}_{{\mathcal{C}}}}$$\scriptstyle{F}$$\textstyle{\mathsf{PreShv}({{\mathcal{C}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathcal{S}}$$\textstyle{{\mathcal{D}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{y}_{{\mathcal{D}}}}$$\textstyle{\mathsf{PreShv}({{\mathcal{D}}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\scriptstyle{F^{\circ}}$

Here, the functor $F^{\circ}$ given by precomposition with $F^{\mathrm{op}}$
is a weak equivalence between univalent categories, and hence a strong
equivalence with inverse $\mathcal{S}$. The isomorphism $\alpha$ is
constructed as follows: Note that fully faithful functors reflect
isomorphisms; we apply this for the functor $F^{\circ}$ of precomposition with
$F^{\mathrm{op}}$. It hence suffices to construct a natural isomorphism from
${\mathsf{y}_{{\mathcal{C}}}}\cdot{{\mathcal{S}}\cdot{F^{\circ}}}\simeq\mathsf{y}_{{\mathcal{C}}}$
to ${F}\cdot{{\mathsf{y}_{{\mathcal{D}}}}\cdot{F^{\circ}}}$. But this is an
instance of a general isomorphism: indeed, for any functor
$G:{\mathcal{A}}\to{\mathcal{X}}$, we have natural transformation from
$\mathsf{y}_{{\mathcal{A}}}$ to
${G};{{\mathsf{y}_{{\mathcal{X}}}};{G^{\circ}}}$, and this natural
transformation is an isomorphism when $G$ is fully faithful. This ends the
construction of the natural isomorphism $\alpha$. The functor $\mathcal{S}$
preserves pullbacks since it is fully faithful and essentially surjective. The
hypotheses of Problem 26 are easily checked, hence Construction 27 applies. ∎

######  Problem 40.

Given a weak equivalence $F:{\mathcal{C}}\to{\mathcal{D}}$, to construct an
equivalence $\mathsf{rep}({\mathcal{C}})\simeq\mathsf{rep}({\mathcal{D}})$.

######  Construction 41 (for Problem 40; transfer_rep_map_weak_equivalence).

A direct instance of Construction 31. ∎

Putting everything together, we obtain:

######  Problem 42.

For any category ${\mathcal{C}}$, to construct an equivalence between
representable maps on ${\mathcal{C}}$ and CwF structures on
$\mathsf{RC}({{\mathcal{C}}})$.

######  Construction 43 (for Problem 42; weq_rep_map_cwf_Rezk).

Construction 41, applied to $\eta_{{\mathcal{C}}}$, gives us an equivalence
$\mathsf{rep}({\mathcal{C}})\simeq\mathsf{rep}(\mathsf{RC}({{\mathcal{C}}}))$.
On the other hand, Lemma 33 tells us that
$\mathsf{cwf}(\mathsf{RC}({{\mathcal{C}}}))\simeq\mathsf{rep}(\mathsf{RC}({{\mathcal{C}}}))$.
Composing the first of these with the inverse of the second yields the desired
equivalence. ∎

##  6 Guide to the accompanying formalization

All constructions and theorems of this work have been formalized in the proof
assistant Coq, over the UniMath library of univalent mathematics [VAG+]. We
rely particularly heavily on UniMath’s category theory library.

Our formalization can be found at https://github.com/UniMath/TypeTheory. The
version current at time of writing will remain permanently available under the
tag 2017-ALV1-arxiv.

The main library will continue development, so naming, organisation, etc. may
change from what is presented here. However, the file Articles/ALV_2017.v will
be maintained to keep the main results of this paper available and locatable
over future versions of the library.

For the reader interested in exploring the formalization, we recommend
starting with that file, and following backwards to find the details of
definitions and constructions. A browsable version is available at
https://unimath.github.io/TypeTheory/coqdoc/master/TypeTheory.Articles.ALV_2017.html.

The specific material of the present article amounts to about 3700 lines of
code in the formalization. Additionally, this development required formalizing
a further c. 1500 lines of general background material (mostly on category
theory) that had not previously been given.

##  7 Summary and future work

The above sections complete the construction of the maps and equivalences of
types promised in the introduction: in particular,

  * •

equivalence between split type-category structures and CwF structures;

  * •

equivalence between CwF structures and universes relative to the Yoneda
embedding, and similarly between representable maps and weak such relative
universes;

  * •

transfer of CwF structures and representable maps to the Rezk completion;

  * •

equivalence between CwF structures on a category ${\mathcal{C}}$ and
representable maps of presheaves on its Rezk completion.

There are several natural interesting directions for further work:

  * •

Define _categories_ of all the various structures considered here; show that
the comparison constructions given here are all moreover functorial, and that
our equivalences of types underlie equivalences of categories. Besides its
intrinsic interest, this would make more of our constructions meaningful and
useful in the classical setting.

  * •

Extend these constructions to give comparisons with other categorical
structures considered for similar purposes in the literature: Dybjer’s
original CwF’s; Cartmell’s contextual categories/C-systems; comprehension
categories; categories with display maps…

  * •

Understand further the transfer of CwF structures along the Rezk completion
construction: does the result enjoy an analogous universal property, making it
the ‘free univalent category with families’ on a category ${\mathcal{C}}$?

Progress in some of these directions may be already found in our
formalization, though not included in the present article.

#### Acknowledgements.

This material is based upon work supported by the National Science Foundation
under agreement Nos. DMS-1128155 and CMU 1150129-338510. Any opinions,
findings and conclusions or recommendations expressed in this material are
those of the author(s) and do not necessarily reflect the views of the
National Science Foundation. This material is based on research sponsored by
The United States Air Force Research Laboratory under agreement number
FA9550-15-1-0053. The US Government is authorized to reproduce and distribute
reprints for Governmental purposes notwithstanding any copyright notation
thereon. The views and conclusions contained herein are those of the author
and should not be interpreted as necessarily representing the official
policies or endorsements, either expressed or implied, of the United States
Air Force Research Laboratory, the U.S. Government or Carnegie Mellon
University. This work has partly been funded by the CoqHoTT ERC Grant 637339,
and by the Swedish Research Council (VR) Grant 2015-03835 _Constructive and
category-theoretic foundations of mathematics_.

## References

  * [ACU15] Thorsten Altenkirch, James Chapman, and Tarmo Uustalu, _Monads need not be endofunctors_ , Logical Methods in Computer Science 11 (2015), no. 1, doi:10.2168/LMCS-11(1:3)2015.
  * [AKS15] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman, _Univalent categories and the Rezk completion_ , Mathematical Structures in Computer Science 25 (2015), 1010–1039, arXiv:1303.0584, doi:10.1017/S0960129514000486.
  * [Awo16] Steve Awodey, _Natural models of homotopy type theory_ , Mathematical Structures in Computer Science (2016), 1–46, arXiv:1406.3219, doi:10.1017/S0960129516000268.
  * [Car78] John Cartmell, _Generalised algebraic theories and contextual categories_ , Ph.D. Thesis, Oxford University (1978), http://www.cs.ru.nl/~spitters/Cartmell.pdf.
  * [Car86] John Cartmell, _Generalised algebraic theories and contextual categories_ , Ann. Pure Appl. Logic 32 (1986), 209–243, doi:10.1016/0168-0072(86)90053-9.
  * [Dyb95] Peter Dybjer, _Internal type theory_ , Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers (Stefano Berardi and Mario Coppo, eds.), Lecture Notes in Computer Science, vol. 1158, Springer, 1995, pp. 120–134, doi:10.1007/3-540-61780-9_66.
  * [Fio12] Marcelo Fiore, _Discrete generalised polynomial functors_ , 2012, Slides from talk given at ICALP 2012, http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf.
  * [Hof97] Martin Hofmann, _Syntax and semantics of dependent types_ , Semantics and Logics of Computation, Cambridge University Press, 1997, pp. 79–130.
  * [How80] William A. Howard, _The formulae-as-types notion of construction_ , To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism (J. P. Seldin and J. R. Hindley, eds.), Academic Press, 1980, Reprint of 1969 article, pp. 479–490.
  * [Pit00] Andrew M. Pitts, _Categorical logic_ , Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures (S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, eds.), Oxford University Press, 2000, pp. 39–128, http://www.oup.co.uk/isbn/0-19-853781-6.
  * [Uni13] The Univalent Foundations Program, _Homotopy type theory: Univalent foundations of mathematics_ , http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [VAG+] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al., _UniMath : Univalent Mathematics_, Available at https://github.com/UniMath.
  * [vdBG12] Benno van den Berg and Richard Garner, _Topological and simplicial models of identity types_ , ACM Trans. Comput. Logic 13 (2012), no. 1, 3:1–3:44, doi:10.1145/2071368.2071371, http://doi.acm.org/10.1145/2071368.2071371.
  * [Voe15] Vladimir Voevodsky, _A C-system defined by a universe category_ , Theory Appl. Categ. 30 (2015), no. 37, 1181–1215, http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf.
  * [Voe16] , _Subsystems and regular quotients of C-systems_ , Conference on Mathematics and its Applications, (Kuwait City, 2014), Contemporary Mathematics, no. 658, 2016, pp. 127–137, http://arxiv.org/abs/1406.7413.