Theory and Applications of Categories, Vol. 32, No. 3, 2017, pp. 53–112.

C-SYSTEMS DEFINED BY UNIVERSE CATEGORIES: PRESHEAVES

VLADIMIR VOEVODSKY

Abstract. The main result of this paper may be stated as a construction of “almost representations” μ_{n} and μ̃_{n} for the presheaves Ob_{n} and Õb_{n} on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these “almost representations” with respect to the universe category functors.

In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.

Contents

1 Introduction  54
2 Presheaves Ob_{n} and Õb_{n}  58
2.1 Functor Sig and functor isomorphisms SOb_{n} and SÕb_{n} . . . . . . . . . . . 58
2.2 Functor D_{p}, sets D_{p}^{n}(X, Y) and the ∘-notation . . . . . . . . . . . . . . . . 64
2.3 Isomorphisms of presheaves u_{1} and ũ_{1} . . . . . . . . . . . . . . . . . . . . . 69
2.4 Functor isomorphisms SD_{p} . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
2.5 Isomorphisms of presheaves u_{n} and ũ_{n} for n ≥ 2 . . . . . . . . . . . . . . . 76
2.6 The case of a locally cartesian closed C - isomorphisms η_{n} and μ_{n} . . . . . 78
3 Functoriality  85
3.1 Universe category functors and the D_{p} construction . . . . . . . . . . . . . 85
3.2 Universe category functors and isomorphisms u_{n} and ũ_{n} . . . . . . . . . . . 94
3.3 Universe category functors and the I_{p} construction . . . . . . . . . . . . . 98
3.4 Universe category functors and the isomorphisms μ_{n} and μ̃_{n} . . . . . . . . 100
4 Appendices  101
4.1 Categories with binary products and binary cartesian closed categories . . 102
4.2 Slice categories, pullbacks and locally cartesian closed categories . . . . . . 106
5 Acknowledgements  110

Received by the editors 2017-01-01 and, in final form, 2017-01-11.

Transmitted by Martin Hyland. Published on 2017-01-20.

2010 Mathematics Subject Classification: 03F50, 18C50 18D15, .

Key words and phrases: Type theory, Contextual category, Universe category.

\begin{matrix}c \\ ◯ \end{matrix} Vladimir Voevodsky, 2017. Permission to copy for private use granted.

1. Introduction

The concept of a C-system in its present form was introduced in [9]. The type of the C-systems is constructively equivalent to the type of contextual categories defined by Cartmell in [1] and [2] but the definition of a C-system is slightly different from Cartmell’s foundational definition.

In [8, Sec.3] we constructed, on any C-system and for any n ≥ 0, presheaves Ob_{n} and Õb_{n}. These presheaves play a major role in our approach to the C-system formulation of systems of operations that correspond to systems of inference rules. For example, by providing a construction for [8, Prob. 4.5] we construct a representation in terms of these presheaves of the most important structure on the C-systems, the structure corresponding to the (Π, λ, app, β, η)-system of inference rules. Another formulation of this structure is the Cartmell-Streicher structure of products of families of types [1, pp. 3.37 and 3.41], [5, p. 71].

This paper appeared as an outcome of the work on systematization and generalization of the ideas that has been used in the second part of the preprint [7]. In the process of this work new structures became apparent both on the C-systems and on the universe categories whose general properties could be combined to obtained clear and systematic proofs of the main theorems of the second part of that preprint.

As a result the paper is about certain constructions on presheaves on C-systems and universe categories, about their interaction in the case of the C-systems of the form CC(C, p), and about their behavior with respect to the universe category functors.

The paper is subdivided into two parts. In the first part there are collected constructions and theorems (most often called ‘lemmas’) about structures on one C-system or universe category or one pair of a C-system and a universe category. In the second part we study the behavior of these constructions with respect to the universe category functors.

Throughout the paper we use the diagrammatic order in writing the composition, that is, for f : X → Y and g : Y → Z we write f ∘ g for their composition. This convention applies to functions between sets, morphisms in categories, functors etc.

We denote by Φ^{∘} the functor P reShv(C′) → P reShv(C) given by the pre-composition with a functor Φ^{op} : C^{op} → (C′)^{op}, that is,

Φ^{∘}(F)(X) = F (Φ(X))

In the literature this functor is denoted both by Φ^{∗} and Φ_{∗} and we decided to use a new unambiguous notation instead.

In the first Section 2.1 we study a functor Sig : P reShv(CC) → P reShv(CC) defined from any C-system CC. This functor comes together with functor isomorphisms

SOb_{n} : Sig(Ob_{n}) → Ob_{n+1}

that makes it important for the study of the ‘structure sheaves’ Ob_{n} and Õb_{n}.

In Section 2.2 we study a functor D_{p} : P reShv(C) → P reShv(C) that is defined for any category C with a choice of a universe p (see [6, Def. 2.1]) in it. We define the sets D_{p}^{n}(X, Y), which play a major role in all that follows, by the formula

D_{p}^{n}(X, Y) = D_{p}^{n}(Y o(Y))(X)

where Y o(Y) is the contravariant functor represented by Y and D_{p}^{n} refers to the n-th iteration of D_{p}. These sets are functorial both in X and Y and we use the notation ∘ for this functoriality, that is, for d ∈ D_{p}^{n}(X, Y), f : X′ → X and g : Y → Y′ we set

f ∘ d = D_{p}^{n}(f, Y)(d)
d ∘ g = D_{p}^{n}(X, g)(g)

This ∘-notation is justified by the identity and associativity equalities collected in Lemma 2.2.3 and makes many computations in the following sections more convenient.

In Section 2.3 we construct the first of the main isomorphisms that we work with in this paper, namely, the isomorphisms u_{1} and ũ_{1} of the form

u_{1} : Ob_{1} → int^{∘}(Y o(U))
ũ_{1} : Õb_{1} → int^{∘}(Y o(Ũ))

Here we start with a universe category, a category with a universe and a final object, that we denote (C, p) where p : Ũ → U is the universe. Associated to it in [6, Constr. 2.12] is a C-system CC(C, p) that comes together with a fully-faithful functor int : CC(C, p) → C. For a functor Φ we let Φ^{∘} denote the functor of pre-composition with Φ on presheaves. In particular, for a presheaf F on C, int^{∘}(F) is a presheaf on CC(C, p). The isomorphisms u_{1} and ũ_{1} provide what we referred to as ‘almost representations’ for Ob_{1} and Õb_{1}.

In Section 2.4 we connect, by a functor isomorphism SD_{p}, the functors D_{p} and Sig in the case of a pair of a universe category and the associated C-system. The isomorphism SD_{p} has the form

SD_{p} : int^{∘} ∘ Sig → D_{p} ∘ int^{∘}

In Section 2.5 we combine SOb_{n}, Sig and SD_{p} to provide the inductive step for a definition of isomorphisms

u_{n} : Ob_{n} → int^{∘}(D_{p}^{n−1}(Y o(U)))
ũ_{n} : Õb_{n} → int^{∘}(D_{p}^{n−1}(Y o(Ũ)))

starting with u_{1} and ũ_{1}. This construction combines all constructions introduced in Sections 2.1-2.4.

Section 2.6 is different from the preceding sections in that, that we assume an additional structure on C namely the combination of the locally cartesian closed and binary product structures. Under the assumption of these structures we construct a functor I_{p} : C → C and a family of representations for presheaves of the form D_{p}(Y o(V)) that we denote by η_{V}:

η_{V} : D_{p}(Y o(V)) → Y o(I_{p}(V))

This family is natural in V forming a functor isomorphism

η : Y o ∘ D_{p} → I_{p} ∘ Y o

where both functors are from C to P reShv(C). By a simple iterative construction we obtain from η functor isomorphisms

η_{n} : Y o ∘ D_{p}^{n} → I_{p}^{n} ∘ Y o

and with them representations of presheaves of the form D_{p}^{n}(Y o(V)). The naturality properties of our construction admit convenient presentation in the ∘-notation:

η_{n}(f ∘ d) = f ∘ η_{n}(d)
η_{n}(d ∘ g) = η_{n}(d) ∘ I_{p}^{n}(g)

Combining isomorphisms η with isomorphisms u and ũ we obtain the second main family of isomorphisms constructed in this paper

μ_{n} : Ob_{n} → int^{∘}(Y o(I_{p}^{n−1}(U)))
μ̃_{n} : Õb_{n} → int^{∘}(Y o(I_{p}^{n−1}(Ũ)))

To be able to rigorously construct I_{p} as a functor and later to study its properties with respect to universe category functors we need notations related to the locally cartesian closed structures that we could not find in the literature. Therefore, we added the two appendices where these notations are introduced. The appendices contain known facts about categories, but it seems that these facts have never been represented at the level of detail that we need in this paper.

We may add that using a locally cartesian closed and a binary product structure to construct I_{p}(V) and the representations of the functors D_{p}(Y o(V)) by means of these objects is to require a lot where much less would suffice. It would be sufficient to simply require a family of objects I_{p}(V) parametrized by V ∈ C and representations η_{V} of D_{p}(Y o(V)) by means of I_{p}(V). The functoriality for this family in V may then be derived from the representations and the functoriality of Y o ∘ D_{p} and this functoriality will automatically make the representations natural in V. This is a much less grand requirement that a full locally cartesian closed plus a binary products structure. However, we will continue to consider the construction based on these two structures because they are more familiar.

Section 2.6 completes the first part of the paper. In the second part we consider how the constructions introduced in the first part interact with the universe category functors.

In Section 3.1 we study the interaction of the functor D_{p} and the construction D_{p}^{n}(X, Y) with the universe category functors. We start with a universe category functor Φ = (Φ, ϕ, ϕ̃) : (C, p) → (C′, p′) and construct a functor isomorphism

ΦD : Φ^{∘} ∘ D_{p} → D_{p′} ∘ Φ^{∘}

Then we use this isomorphism along with a number of other constructions to define, for all X, Y ∈ C and n ≥ 0, functions

Φ_{X,Y}^{n} : D_{p}^{n}(X, Y) → D_{p′}^{n}(Φ(X), Φ(Y))

These functions are natural in X and Y, which, in the ∘-notation, can be written as

Φ^{n}(f ∘ d) = Φ(f) ∘ Φ^{n}(d)
Φ^{n}(d ∘ g) = Φ^{n}(d) ∘ Φ(g)

In Section 3.2 we study the interaction of the isomorphisms u_{n} and ũ_{n} with the universe category functors. First, we recall the construction, given in [6, Constr. 4.7], of the homomorphism of C-systems H : CC(C, p) → CC(C′, p′) defined by Φ. We also show that the family of isomorphisms ψ(Γ) constructed in the same paper forms a functor isomorphism

ψ : H ∘ int → int ∘ Φ

The main result of this section is Lemma 3.2.4 that establishes the rule under which isomorphisms u_{n} and ũ_{n} are transformed by universe category functors.

In Section 3.3 we study the interaction of universe category functors between locally cartesian closed universe categories with binary product structures and the constructions I_{p} and η_{n}. No assumption about the compatibility of the functor with the locally cartesian closed or binary product structures used to define I_{p} and I_{p′} and the corresponding η_{n} functions is made. In a somewhat surprising result no such assumption turns out to be necessary to construct a natural family of morphisms

χ_{Φ,n} : Φ(I_{p}^{n}(Y)) → I_{p′}^{n}(Φ(Y))

that satisfy, for d ∈ Φ^{n}(X, Y), the equalities

η_{n}(Φ^{n}(d)) = Φ(η_{n}(d)) ∘ χ_{n}(Y)

In Section 3.4 we apply the results of the previous section and Section 3.2 to describe the interaction of isomorphisms μ_{n} and μ̃_{n} with universe category functors. This is the last result of the present paper.

In [10] the result of Section 3.4 it is used to prove the functoriality theorem for the construction of a (Π, λ)-structure on CC(C, p) from a P -structure on p.

Throughout the paper we work in the Zermelo-Fraenkel foundations. The methods of this paper are constructive in the following sense. Neither the axiom of the excluded middle nor the axiom of choice are used. Unbounded universal quantification is used since we make statements about “any C-system” etc. and operate with concepts such as a presheaf or a family without specifying the target universe. I seems that this use of unbounded quantification can be easily eliminated at the price of extending the foundational system to include one or two universes. We have not fully analyzed the requirements that these universes would have to satisfy. At the moment it appears that it would be sufficient to use “small” universes whose existence can be proved in ZF.

At the same time as complying with the requirements imposed by ZF we made an effort to ensure that the paper can be translated into the UniMath language.

The paper is written in the formalization-ready style, that is, in such a way that no long arguments are hidden even when they are required only to substantiate an assertion that may feel obvious to readers who are closely associated with a particular tradition of mathematical thought.

As a result, a number of lemmas, especially in the appendices, may be well know to many readers. Their proofs are nevertheless included to comply with the requirements of the formalization ready style.

On the other hand, not all preliminary lemmas are included or a reference to a complete proof is given. There are some, but very much fewer than is usual in today’s papers, exceptions.

The concept of “a family” can be formalized as suggested in [8, Remark 3.9].

The main results of this paper are not theorems but constructions and so are many of the intermediate results. Because of the importance of constructions for this paper we use a special pair of names Problem-Construction for the specification of the goal of a construction and the description of the particular solution.

In the case of a Theorem-Proof pair one usually refers (by name or number) to the theorem when using the proof of this theorem. This is acceptable in the case of theorems because the future use of their proofs is such that only the fact that there is a proof but not the particulars of the proof matter.

In the case of a Problem-Construction pair the content of the construction often matters in the future use. Because of this we have to refer to the construction and not to the problem and we assign in this paper numbers both to Problems and to Constructions.

Acknowledgements are at the end of the paper.

2. Presheaves Ob_{n} and Õb_{n}

2.1. Functor Sig and functor isomorphisms SOb_{n} and SÕb_{n}. Let CC be a Csystem. Presheaves Ob_{n} and Õb_{n} on CC where defined in [8, Section 3]. On objects they are given by

Ob_{n}(Γ) = {T ∈ Ob(CC) | l(T) = l(Γ) + n, ft^{n}(T) = Γ}  (2.1)
Õb_{n}(Γ) = {o ∈ Mor(CC) | codom(o) ∈ Ob_{n}(Γ), o ∈ sec(p_{codom(o)}), codom(o) > Γ} (2.2)

where for a morphism p : Y → X we set

sec(p) = {s ∈ Mor(X, Y) | s ∘ p = Id_{X}}

Elements of sec(p) are called sections of p.

On morphisms these presheaves are defined by

Ob_{n}(f)(T) = f^{∗}(T)
Õb_{n}(o) = f^{∗}(o)

where f^{∗}(T) is defined in [8, above Lemma 2.4] and f^{∗}(o) is defined in [8, Lemma 2.13].

For o ∈ Õb_{n}(Γ) we write ∂_{n,Γ}(o) for codom(o). We will often omit the indexes n and Γ at ∂. The family of functions ∂_{n,Γ} forms a morphism of presheaves ∂_{n} : Õb_{n} → Ob_{n}.

In this section we consider three constructions that apply to any C-system CC – a functor Sig : P reShv(CC) → P reShv(CC) and two families of isomorphisms paramerized by n ∈ N:

SOb_{n} : Sig(Ob_{n}) → Ob_{n+1}

and

SÕb_{n} : Sig(Õb_{n}) → Õb_{n+1}

such that SÕb_{n} ∘ ∂_{n+1} = Sig(∂_{n}) ∘ SOb_{n}.

Let G be a presheaf on CC. For Γ ∈ CC we set

Sig(G)(Γ) = ⨿_{T ∈Ob_{1}(Γ)}G(T)  (2.3)

and for f : Γ′ → Γ

Sig(G)(f)(T, g) = (f^{∗}(T), G(q(f, T))(T))  (2.4)

2.1.1. Lemma. The presheaf data Sig is a presheaf, that is, one has:

1. for Γ ∈ CC,

Sig(G)(Id_{Γ}) = Id_{Sig(G)(Γ)}

2. for f′ : Γ′′ → Γ′, f : Γ′ → Γ,

Sig(G)(f′ ∘ f) = Sig(G)(f) ∘ Sig(G)(f′)

Proof. For the identity we have

Sig(G)(Id_{Γ})(T, g) = (Id_{Γ}^{∗}(T), G(q(Id_{Γ}, T))(g)) = (T, g)

where the second equality is by axioms of the C-system structure. For the composition we have

Sig(G)(f′)(Sig(G(f)(T, g))) = Sig(G)(f′)(f^{∗}(T), G(q(f, T))(g)) =

((f′)^{∗}(f^{∗}(T)), G(q(f′, f^{∗}(T)))(G(q(f, T))(g))) = ((f′)^{∗}(f^{∗}(T)), G(q(f′, f^{∗}(T))∘q(f, T))(g))

= (f′ ∘ f)^{∗}(T), G(q(f′ ∘ f, T))(g)) = Sig(G)(f′ ∘ f)(T, g)

where the first two equalities are by definition of Sig(G), the third by the composition property of G, the fourth by the axioms of the C-system structure and the fifth again by the definition of Sig(G). This completes the proof of Lemma 2.1.1.

One defines Sig on morphisms of presheaves r : G → G′ by the family of morphisms

Sig(r)_{Γ}(T, g) = (T, r_{T} (g))  (2.5)

For r : G → G′ and f : Γ′ → Γ, we have

Sig(G)(f) ∘ Sig(r)_{Γ′} = Sig(r)_{Γ} ∘ Sig(G′)(f)

that is, the family of functions Sig(r)_{Γ} parametrized by Γ ∈ CC is a morphism of presheaves.

For G ∈ P reShv(CC) we have

Sig(Id_{G})_{Γ}(T, g) = (T, (Id_{G})_{T} (g)) = (T, g)  (2.6)

and for r : G → G′, r′ : G′ → G′′ we have

Sig(r ∘ r′)_{Γ}(T, g) = (T, (r ∘ r′)_{T} (g)) = (T, r′_{T} (r_{T} (g))) = Sig(r′)(Sig(r)(T, g)) (2.7)

These two equalities show that the functor data given by Sig on presheaves and Sig on morphisms of presheaves is a functor that we also denote by

Sig : P reShv(CC) → P reShv(CC)

2.1.2. Remark. The construction of Sig works in more general setting than presheaves.

Indeed, for any family of sets G(Γ) parametrized by Γ ∈ CC the formula (2.3) defines a new family of sets Sig(G)(Γ) also parametrized by Γ ∈ CC. For any two families G, G′ and a family of functions r_{Γ} : G(Γ) → G′(Γ) the formula (2.5) defines a family of functions Sig(r)_{Γ} : Sig(G)(X) → Sig(G′)(X). The properties (2.6) and (2.7) hold in this more general setting.

We can also define Sig(G) for any presheaf data, that is, for any pair consisting of a family G(Γ) of sets parametrized by Γ ∈ CC and a family of functions G(f) : G(Γ) → G(Γ′) parametrized by f : Γ′ → Γ in Mor(CC). For this we can again use formulas (2.3) and (2.4).

If r_{Γ} : G(Γ) → G′(Γ) is a morphism of functor data, that is functions r_{∗} commute with functions G(∗), then Sig(r) is a morphism of functor data as well.

2.1.3. Problem. For n ≥ 0 to construct an isomorphism of presheaves

SOb_{n} : Sig(Ob_{n}) → Ob_{n+1}

In constructing a solution of this problem and other problems where one needs to build an of isomorphism of presheaves we will use the following lemma that is often applied without an explicit reference.

2.1.4. Lemma. Let Φ, Φ′ : C → D be functors and ϕ : Φ → Φ′ a natural transformation. Then ϕ is an isomorphism of functors if and only if for all objects X of C the morphism ϕ_{X} : Φ(X) → Φ′(X) is an isomorphism in D.

When this condition is satisfied, the inverse isomorphism is formed by the family of morphisms ϕ_{X}^{−1} = (ϕ_{X})^{−1}.

Proof. One should first verify that identity isomorphism of functors is formed by the family Id_{Φ(X)}. This is immediate from the definitions.

If ϕ is an isomorphism as above and ϕ^{−1} is its inverse, then the composition of these two morphisms is Id_{Φ(X)} and since it consists of the identity morphisms of the objects Φ(X) we conclude that the morphisms ϕ_{X}^{−1} form inverses to the morphisms ϕ_{X}. This proves the “only if part”.

If all morphisms ϕ_{X} are isomorphisms then the family (ϕ_{X})^{−1} forms a morphism of presheaves ϕ^{−1} : Φ′ → Φ. Indeed, for f : X → Y one has

ϕ_{X}^{−1} ∘ Φ(f) = Φ′(f) ∘ ϕ_{Y}^{−1}

This equality follows by taking its composition with ϕ_{X} on the left and ϕ_{Y} on the right. That ϕ^{−1} is both the left and the right inverse to ϕ is immediate from its definition. This proves the “if” part.

We will also need the following lemma.

2.1.5. Lemma. Let Γ ∈ CC. Then one has:

1. if T ∈ Ob_{1}(Γ) and X ∈ Ob_{n}(T) then X ∈ Ob_{n+1}(Γ),

2. if X ∈ Ob_{n+1}(Γ) then ft^{n}(X) ∈ Ob_{1}(Γ) and X ∈ Ob_{n}(ft^{n}(X)).

Proof. The first assertion follows from the equalities l(X) = l(T) + n = l(Γ) + 1 + n and ft^{n+1}(X) = ft(ft^{n}(X)) = ft(T) = Γ.

To prove the second assertion let X ∈ Ob_{n+1}(Γ). Since l(X) ≥ n we have l(ft^{n}(X)) = l(X) − n = l(Γ) + (n + 1) − n = l(Γ) + 1. The equality ft^{1}(ft^{n}(X)) = ft^{n+1}(X) = Γ is obvious and we conclude that ft^{n}(X) ∈ Ob_{1}(Γ). Next, again because l(X) ≥ n, we have l(X) = l(ft^{n}(X)) + n and since ft^{n}(X) = ft^{n}(X) we have that X ∈ Ob_{n}(ft^{n}(X)).

2.1.6. Construction. Let Γ ∈ CC. Then Sig(Ob_{n})(Γ) is the set of pairs (T, X) where T ∈ Ob_{1}(Γ) and X ∈ Ob_{n}(T). By Lemma 2.1.5(1), the formula

SOb_{n,Γ}(T, X) = X  (2.8)

defines a function Sig(Ob_{n})(Γ) → Ob_{n+1}(Γ). Conversely, by Lemma 2.1.5(2), the formula

SOb_{n,Γ}^{−1}(X) = (ft^{n}(X), X)  (2.9)

defines a function Ob_{n+1}(Γ) → Sig(Ob_{n})(Γ). If Φ = SOb_{n,Γ} and Ψ = SOb_{n,Γ}^{−1} then

Φ(Ψ(X)) = Φ((ft^{n}(X), X)) = X

and

Ψ(Φ(T, X)) = Ψ(X) = (ft^{n}(X), X) = (T, X)

where the last equality follows from the equality T = ft^{n}(X). We conclude that SOb_{n,Γ} and SOb_{n,Γ}^{−1} are mutually inverse bijections.

In view of Lemma 2.1.4, it remains to verify that the family of bijections SOb_{n,Γ} parametrized by Γ ∈ CC is a morphism of presheaves, that is, that for any f : Γ′ → Γ and (T, X) ∈ Sig(Ob_{n})(Γ) we have

Ob_{n+1}(f)(SOb_{n,Γ}((T, X))) = SOb_{n,Γ′}(Sig(Ob_{n})(f)((T, X)))  (2.10)

Computing we get

Ob_{n+1}(f)(SOb_{n,Γ}((T, X))) = f^{∗}(X)
SOb_{n,Γ′}(Sig(Ob_{n})(f)((T, X))) = SOb_{n,Γ′}(f^{∗}(T), q(f, T)^{∗}(X)) = q(f, T)^{∗}(X)

and (2.10) follows from [8, Lemma 2.7]. This completes Construction 2.1.6.

As a corollary of Construction 2.1.6 and Lemma 2.1.4 we obtain the fact that the family of functions (2.9) parametrized by Γ ∈ CC is an isomorphism of presheaves that is inverse to SOb_{n}.

We proceed now to the construction of isomorphisms SÕb_{n}.

Recall from [9, Sec. 3], that Õb(CC) is the set of elements o ∈ Mor(CC) such that o ∈ sec(p_{codom(o)}) and l(codom(o)) > 0. For such elements we also denote codom(o) by ∂(o).

It follows easily from (2.2) that for Γ ∈ Ob(CC) and n > 0 one has o ∈ Õb_{n}(Γ) if and only if o ∈ Õb(CC) and ∂(o) ∈ Ob_{n}(Γ). It also follows from (2.2) that Ob_{0}(Γ) = ∅.

2.1.7. Problem. For n ≥ 1 to construct an isomorphism of presheaves 2.1.8. Lemma. Let Γ ∈ CC. Then one has:

1. if T ∈ Ob_{1}(Γ) and o ∈ Õb_{n}(T) then o ∈ Õb_{n+1}(Γ),

2. if o ∈ Õb_{n+1}(Γ) then ft^{n}(∂(o)) ∈ Ob_{1}(Γ) and o ∈ Õb_{n}(ft^{n}(∂(o))).

Proof. If o ∈ Õb_{n}(T) we have n > 0 an therefore o ∈ Õb(CC) and ∂(o) ∈ Ob_{n}(T). By Lemma 2.1.5(1) we have ∂(o) ∈ Ob_{n+1}(Γ). Therefore o ∈ Õb_{n+1}(T). This proves the first assertion.

If o ∈ Õb_{n+1}(Γ) then o ∈ Õb(CC) and ∂(o) ∈ Ob_{n+1}(Γ). By Lemma 2.1.5(2) we have ft^{n}(∂(o)) ∈ Ob_{1}(Γ) and ∂(o) ∈ Ob_{n}(ft^{n}(∂(o))). Therefore o ∈ Õb_{n}(ft^{n}(∂(o))).

We can now provide a construction for Problem 2.1.7.

2.1.9. Construction. For Γ ∈ CC we have

Sig(Õb_{n})(Γ) = {(T, o) | T ∈ Ob_{1}(Γ), o ∈ Õb_{n}(T)}

For (T, o) ∈ Sig(Õb_{n})(Γ) we have o ∈ Õb_{n+1}(Γ) by Lemma 2.1.8(1) and therefore the formula

SÕb_{n,Γ}(T, o) = o  (2.11)

defines a function Sig(Õb_{n})(Γ) → Õb_{n+1}(Γ).

If o ∈ Õb_{n+1}(Γ) then by Lemma 2.1.8(2), ft^{n}(∂(o)) ∈ Õb_{1}(Γ) and o ∈ Õb_{n}(ft^{n}(∂(o))). Therefore the formula

SÕb_{n,Γ}^{−1}(o) = (ft^{n}(∂(o)), o)  (2.12)

defines a function Õb_{n+1}(Γ) → Sig(Õb_{n})(Γ).

One verifies in the same way as in Construction 2.1.6 that SÕb_{n,Γ} and SÕb_{n,Γ}^{−1} are mutually inverse bijections.

In view of Lemma 2.1.4 it remains to verify that the family of functions SÕb_{n,Γ} parametrized by Γ ∈ CC is a morphism of functors, that is, that for f : Γ′ → Γ and (T, o) ∈ SOb_{n,Γ} one has

Õb_{n+1}(f)(SÕb_{n,Γ}(T, o)) = SÕb_{n,Γ′}(Sig(Õb_{n})(f)(T, o))  (2.13)

Computing we get

Õb_{n+1}(f)(SÕb_{n,Γ}(T, o)) = Õb_{n+1}(f)(o) = f^{∗}(o)
SÕb_{n,Γ′}(Sig(Õb_{n})(f)(T, o)) = SÕb_{n,Γ′}(f^{∗}(T), q(f, T)^{∗}(o)) = q(f, T)^{∗}(o)

and we conclude that (2.13) holds by [8, Lemma 2.15].

This completes Construction 2.1.9.

As a corollary of Construction 2.1.9 and Lemma 2.1.4 we obtain the fact that the family of functions (2.12) parametrized by Γ ∈ CC is an isomorphism of presheaves that is inverse to SÕb_{n}.

2.1.10. Lemma. For any n ≥ 1 the square of morphisms of presheaves

\begin{matrix}Sig(Õb_{n}) & ⟶^{SÕb_{n}} & Õb_{n+1} \\ ^{Sig(∂)}↓ & & ↓^{∂} \\ Sig(Ob_{n}) & ⟶^{SOb_{n}} & Ob_{n+1} \end{matrix}  (2.14)

commutes.

Proof. Let Γ ∈ CC. By definition we have

Sig(Õb_{n})(Γ) = {(T, o) | T ∈ Ob_{1}(Γ), o ∈ Õb_{n}(T)}

Let (T, o) ∈ Sig(Õb_{n})(Γ). Then, again by definitions,

∂_{Γ}(SÕb_{n,Γ}(T, o)) = ∂_{Γ}(o)

and

SOb_{n,Γ}(Sig(∂)_{Γ}(T, o)) = SOb_{n,Γ}(T, ∂_{Γ}(o)) = ∂_{Γ}(o)

The lemma is proved.

2.1.11. Remark. Define Sig^{n} by induction on n, setting Sig^{0} = Id_{P reShv(CC)} and Sig^{n+1} = Sig^{n} ∘ Sig. Then, also by induction on n, we can construct isomorphisms

SOb_{m}^{n} : Sig^{n}(Ob_{m}) → Ob_{n+m}

where SOb_{m}^{0} = Id_{Ob_{m}} and SOb_{m}^{n+1} is the composition

Sig^{n+1}(Ob_{m}) = Sig(Sig^{n}(Ob_{m})) ⟶^{Sig(SOb_{m}^{n})} Sig(Ob_{n+m}) ⟶^{SOb_{n+m}} Ob_{n+m+1}

In exactly the same way we construct isomorphisms

SÕb_{m}^{n} : Sig^{n}(Õb_{m}) → Õb_{n+m}

2.2. Functor D_{p}, sets D_{p}^{n}(X, Y) and the ∘-notation. In this section we work in the context of a category C with a universe p. The goal of the section is to construct, for any such pair, a functor

D_{p} : P reShv(C) → P reShv(C)

The definition of a universe in a category was given in [6, Definition 2.1]. We repeat it here for the convenience of the reader.

2.2.1. Definition. Let C be a category. A universe structure on a morphism p : Ũ → U in C is a mapping that assigns to any morphism f : X → U in C a pullback of the form

\begin{matrix}(X, f) & ⟶^{Q(F)} & Ũ \\ ^{p_{X,F}} ↓ & & ↓^{p} \\ X & ⟶^{F} & U \end{matrix}  (2.15)

A universe in C is a morphism together with a universe structure on it.

We usually refer to a universe by the name of the corresponding morphism without mentioning the choices of pullbacks explicitly. To shorten the notation we will write p_{F} instead of p_{X,F}.

For f : W → X and g : W → Ũ such that f ∘ F = g ∘ p we will denote by f ∗_{F} g the unique morphism W → (X; F) such that

(f ∗_{F} g) ∘ p_{F} = f  (2.16)

(f ∗_{F} g) ∘ Q(F) = g  (2.17)

For X′ →^{f} X →^{F} U we let Q(f, F) denote the morphism

Q(f, F) = (p_{f∘F} ∘ f) ∗_{F} Q(f ∘ F) : (X′; f ∘ F) → (X; F)  (2.18)

Observe that one has

Q(f ∘ F) = Q(f, F) ∘ Q(F)  (2.19)
Q(Id_{X}, F) = Id_{(X;F)}  (2.20)
Q(f′ ∘ f, F) = Q(f′, f ∘ F) ∘ Q(f, F)  (2.21)

where the first equality follows directly from the definition, the second from the definition and the uniqueness of the morphisms f ∗_{F} g satisfying (2.16) and (2.17) and the third is proved in [6, Lemma 2.5].

Let us fix a category C and a universe p in it.

For any G ∈ P reShv(C) we define functor data D_{p}(G) given on objects by

D_{p}(G)(X) := ⨿_{F:X→U}G((X; F))  (2.22)

and on morphisms by

D_{p}(G)(f) : (F, γ) ↦ (f ∘ F, G(Q(f, F))(γ))  (2.23)

2.2.2. Lemma. The functor data D_{p}(G) specified above is a presheaf, i.e., one has

1. for any X ∈ C, D_{p}(G)(Id_{X}) = Id_{D_{p}(G)(X)},

2. for any f : X → Y, g : Y → Z in C,

D_{p}(G)(f ∘ g) = D_{p}(G)(g) ∘ D_{p}(G)(f)

Proof. For the first property we have

D_{p}(G)(Id_{X})((F, γ)) = (Id_{X} ∘ F, G(Q(Id_{X}, F))(γ)) = (F, γ)

where the second equality is by (2.20) and the identity morphism axiom for the presheaf G.

For the second one we have

D_{p}(G)(f ∘ g)(F, γ) = (f ∘ g ∘ F, G(Q(f ∘ g, F))(γ))) =

(f ∘ g ∘ F, G(Q(f, g ∘ F) ∘ Q(g, F))(γ)) = (f ∘ (g ∘ F), G(Q(f, g ∘ F))(G(Q(g, F))(γ))) =

D_{p}(G)(f)(D_{p}(G)(g)(F, γ)) = (D_{p}(G)(g) ∘ D_{p}(G)(f))(F, γ)

where the second equality is by (2.21) and the third one by the composition axiom of the presheaf G.

One defines D_{p} on morphisms of presheaves r : G → G′ by the family of morphisms

D_{p}(r)_{X}(F, γ) = (F, r_{(X;F)}(γ))  (2.24)

For f : X → X′ and r : G → G′ we have

D_{p}(G)(f) ∘ D_{p}(r)_{X} = D_{p}(r)_{X′} ∘ D_{p}(G′)(f)  (2.25)

that is, the family of functions D_{p}(r)_{X} parametrized by X ∈ C is a morphism of presheaves.

For G ∈ P reShv(C) we have

D_{p}(Id_{G})_{X} = Id_{D_{p}(G)(X)}

and for r : G → G′ and r′ : G′ → G′′ we have

D_{p}(r ∘ r′)_{X} = D_{p}(r)_{X} ∘ D_{p}(r′)_{X}  (2.26)

These two equalities show that the functor data given by D_{p} on presheaves and D_{p} on morphisms of presheaves is a functor that we also denote by

D_{p} : P reShv(C) → P reShv(C)

Note that for the presheaves of the form Y o(A), where Y o is the Yoneda embedding, we have

D_{p}(Y o(A))(X) = ⨿_{F:X→U}Mor_{C}((X; F), A)  (2.27)

and for a morphism f : X → X′,

D_{p}(Y o(A))(f)(F_{1}, F_{2}) = (f ∘ F_{1}, Q(f, F_{1}) ∘ F_{2})  (2.28)

For a morphism a : A′ → A we have

D_{p}(Y o(a))_{X}(F_{1}, F_{2}) = (F_{1}, F_{2} ∘ a)  (2.29)

Define

D_{p}^{n}(X, Y) = D_{p}^{n}(Y o(Y))(X)  (2.30)

such that in particular one has

D_{p}^{0}(X, Y) = Mor_{C}(X, Y)

Since D_{p}^{n}(Y o(Y)) is a presheaf we have, for any f : X′ → X, the function

D_{p}^{n}(Y o(Y))(f) : D_{p}^{n}(Y o(Y))(X) → D_{p}^{n}(Y o(Y))(X′)

that we denote by

D_{p}^{n}(f, Y) : D_{p}^{n}(X, Y) → D_{p}^{n}(X′, Y)  (2.31)

Since D_{p}^{n} and Y o are functors we have, for any g : Y → Y′, a function

D_{p}^{n}(Y o(g))_{X} : D_{p}^{n}(Y o(Y))(X) → D_{p}^{n}(Y o(Y′))(X)

that we denote by

D_{p}^{n}(X, g) : D_{p}^{n}(X, Y) → D_{p}^{n}(X, Y′)  (2.32)

Let d ∈ D_{p}^{n}(X, Y). For f : X′ → X we let f ∘^{n} d denote D_{p}^{n}(f, Y)(d). For g : Y → Y′ we let d^{n}∘ g denote D_{p}^{n}(X, g)(d). When no confusion is possible we will abbreviate both ∘^{n} and ^{n}∘ to ∘.

Let us summarize, using this “∘-notation” some of the results proved above in the following lemma.

2.2.3. Lemma. For d ∈ D_{p}^{n}(X, Y) we have the following formulas:

1. Id_{X} ∘ d = d,

2. (f′ ∘ f) ∘ d = f′ ∘ (f ∘ d),

3. d ∘ Id_{Y} = d,

4. d ∘ (g ∘ g′) = (d ∘ g) ∘ g′,

5. f ∘ (d ∘ g) = (f ∘ d) ∘ g.

Proof. The first two equalities follow from the axioms of presheaf for D_{p}^{n}(Y o(Y)), the second two from the fact that Y o ∘ D_{p}^{n} is a functor and the last one from the fact that the family of functions D_{p}(Y o(g))_{−} is a morphism of presheaves.

2.2.4. Lemma. Let (C, p) be a universe category, n ≥ 1, X, Y ∈ C, and

(F, a) ∈ ⨿_{F:X→U}D_{p}^{n−1}((X; F), Y) = D_{p}(D_{p}^{n−1}(Y o(Y)))(X) = D_{p}^{n}(X, Y)

Then one has

1. for f : X′ → X

f ∘ (F, a) = (f ∘ F, Q(f, F) ∘ a)

2. for g : Y → Y′

(F, a) ∘ g = (F, a ∘ g)

Proof. In the first case we have

f ∘ (F, a) =
D_{p}^{n}(Y o(Y))(f)((F, a)) = (f ∘ F, D_{p}^{n−1}(Y o(Y))(Q(f, F))(a)) =
(f ∘ F, Q(f, F) ∘ a)

where the first equality is by the definition of D_{p}^{n}(f, Y), the second by (2.23) and the third by the definition of D_{p}^{n−1}(Q(f, F), Y).

In the second case we have

(F, a) ∘ g =
D_{p}^{n}(Y o(g))_{X}((F, a)) = (F, D_{p}^{n−1}(Y o(g))_{(X;F)}(a)) =
(F, a ∘ g)

where the first equality is by the definition of D_{p}^{n}(X, g), the second by (2.23) and the third by the definition of D_{p}^{n−1}((X; F), g). The lemma is proved.

2.2.5. Remark. It is likely that the functions (2.31) and (2.32) generalize to composition functions

D_{p}^{n}(X, Y) × D_{p}^{m}(Y, Z) → D_{p}^{n+m}(X, Z)  (2.33)

The formulas 1.-5. suggest that these composition functions satisfy the unity and associativity axioms and therefore one obtains, from any universe category (C, p), a new category (C, p)_{∗} with the same collection of objects and morphisms between two objects given by

Mor_{(C,p)_{∗}}(X, Y) = ⨿_{n≥0}D_{p}^{n}(X, Y)

The study of the composition functions (2.33) and categories (C, p)_{∗} is deferred to a later paper.

2.2.6. Remark. The observations of Remark 2.1.2 apply, with obvious modifications, to the construction D_{p} as well.

2.3. Isomorphisms of presheaves u_{1} and ũ_{1}. We now consider a universe category, that is, a category C with a universe p and a choice of a final object pt. We usually denote a universe category as (C, p) without mentioning the final object. For any universe category we have constructed in [6, Section 2] a C-system CC(C, p).

The main goal of this section is to provide constructions for Problems 2.3.2 and 2.3.5. Let us first recall the construction of CC(C, p). One defines first, by induction on n,

pairs (Ob_{n}, int_{n} : Ob_{n} → C) where Ob_{n} = Ob_{n}(C, p) is a set and int_{n} is a function from Ob_{n} to objects of C. The definition is as follows:

1. Ob_{0} is the standard one point set unit whose element we denote by tt. The function int_{0} maps tt to the final object pt of the universe category structure on C,

2. Ob_{n+1} = ⨿_{A∈Ob_{n}}Mor(int(A), U) and int_{n+1}(A, F) = (int(A); F).

We then define Ob(CC(C, p)) as ⨿_{n≥0}Ob_{n} such that elements of Ob(CC(C, p)) are pairs Γ = (n, A) where A ∈ Ob_{n}(C, p). We define the function int : Ob(CC(C, p)) → C as the sum of functions int_{n}. Where no confusion between int and int_{n} is likely we will omit the index n at int_{n}.

The morphisms in CC(C, p) are defined by

Mor_{CC(C,p)} = ⨿_{Γ,Γ′∈Ob(CC)}Mor_{C}(int(Γ), int(Γ′))

and the function int on morphisms maps a triple ((Γ, Γ′), a) to a. Note that the subset in Mor that consists of f such that dom(f) = Γ and codom(f) = Γ′ is not equal to the set Mor_{C}(int(Γ), int(Γ′)) but instead to the set of triples of the form f = ((Γ, Γ′), a) where a ∈ Mor_{C}(int(Γ), int(Γ′)). The functor int maps ((Γ, Γ′), a) to a. This map is bijective and therefore the functor is fully faithful but its morphism component is not the identity function.

The length function is defined by l((n, A)) = n.

One defines pt as pt = (0, tt). It is the only object of length 0.

If Γ = (n, B) where n > 0 then, by construction, B = (A, F) where F : int(A) → U. The ft function is defined on such Γ by ft(Γ) = (n − 1, A) and on pt by ft(pt) = pt.

2.3.1. Lemma. For Γ = (n, A) and T = (n′, B) ∈ Ob(CC(C, p)) one has T ∈ Ob_{1}(Γ) if and only if n′ = n + 1 and there exists F : int(A) → U such that B = (A, F).

Proof. By definition of the length function l, we have l(Γ) = n and l(T) = n′. By definition of Ob_{1}, T ∈ Ob_{1}(Γ) if and only if n′ = n + 1 and ft(T) = Γ.

If T = (n + 1, (A, F)) then n′ = n + 1. In particular, l(T) > 0 and therefore ft(T) = (n, A) = Γ. This proves the ”if” part.

Assume that T = (n′, B) ∈ Ob_{1}(Γ). Then n′ = n + 1. Since n′ > 0, B is a pair of the form (A′, F). Since ft(T) = (n, A′) = (n, A) we have A′ = A. This proves the “only if” part.

The p-morphism for Γ = (n, A) where n > 0 and A = (B, F) is given by ((Γ, ft(Γ)), p_{F}) where p_{F} are the p-morphisms of the universe structure.

For f : (n, A′) → (n, A) and T such that l(T) = l(Γ) + 1 and ft(T) = Γ one has, by Lemma 2.3.1, T = (n + 1, (A, F)) and one defines

f^{∗}(T) = (n + 1, (A′, int(f) ∘ F))  (2.34)

and

q(f, T) = ((f^{∗}(T), T), Q(int(f), F))  (2.35)

The C-system axioms are verified in [6].

Let us denote by

int^{∘} : P reShv(C) → P reShv(CC)

the functor of pre-composition with int^{op} and by

Y o : C → P reShv(C)

the Yoneda embedding of C.

2.3.2. Problem. To construct an isomorphism of presheaves

u_{1} : Ob_{1} → int^{∘}(Y o(U))  (2.36)

such that for Γ = (n, A) and T = (n + 1, (A, F)) one has

u_{1,Γ}(T) = F  (2.37)

2.3.3. Construction. By definition of int^{∘} and Y o and Lemma 2.1.4, an isomorphism of presheaves of the form (2.36) is a family of functions of the form

u_{1,Γ} : Ob_{1}(Γ) → Mor_{C}(int(Γ), U)

parametrized by Γ ∈ Ob(CC(C, p)) such that for any f : Γ′ → Γ and any T ∈ Ob_{1}(Γ) one has

u_{1,Γ′}(f^{∗}(T)) = int(f) ∘ u_{1,Γ}(T)  (2.38)

and for any Γ the function u_{1,Γ} is a bijection.

By Lemma 2.3.1, the conditions (2.37) define our family completely and it remains to verify (2.38) and the bijectivity condition.

For Γ = (n, A), T = (n + 1, (A, F)), Γ′ = (n′, A′) and f : Γ′ → Γ we have, by (2.34),

f^{∗}(T) = (n′ + 1, (A′, int(f) ∘ F))

Therefore,

u_{1,Γ′}(f^{∗}(T)) = u_{1,Γ′}((n′ + 1, (A′, int(f) ∘ F))) = int(f) ∘ F = int(f) ∘ u_{1,Γ}(T)

which proves (2.38).

By Lemma 2.3.1, for Γ = (n, A), the formula F ↦ (n + 1, (A, F)) defines a function

Mor_{C}(int(A), U) → Ob_{1}(Γ)

By the same lemma and (2.37) this function is inverse to u_{1,Γ}. This proves the bijectivity condition and completes Construction 2.3.3.

Using again Lemma 2.3.1 and (2.37) we see that for any Γ ∈ Ob(CC(C, p)) and T ∈ Ob_{1}(Γ),

int(T) = (int(Γ); u_{1,Γ}(T))  (2.39)

and

int(p_{T}) = p_{u_{1,Γ}(T)}  (2.40)

For f : Γ′ → Γ and T as above we have

int(q(f, T)) = Q(int(f), u_{1,Γ}(T))  (2.41)

2.3.4. Lemma. For Γ = (n, A) and o ∈ Õb_{1}(Γ) one has

codom(int(o)) = (int(Γ); u_{1,Γ}(∂(o)))  (2.42)

Proof. We have codom(o) = ∂(o) ∈ Ob_{1}(Γ). Therefore (2.42) follows from the equality codom(int(f)) = int(codom(f)) and (2.39).

The second problem whose solution is constructed in this section is as follows.

2.3.5. Problem. To construct an isomorphism of presheaves

ũ_{1} : Õb_{1} → int^{∘}(Y o(Ũ))  (2.43)

such that for o ∈ Õb_{1}(Γ) one has

ũ_{1,Γ}(o) = int(o) ∘ Q(u_{1,Γ}(∂(o)))  (2.44)

where the right hand side is defined by (2.42) and the equality dom(Q(F)) = (dom(F); F).

To construct a solution for this problem we will need the following two lemmas.

2.3.6. Lemma. For a universe p in C and X ∈ C, the function

⨿_{F ∈Mor(X,U)}sec(p_{F}) → Mor(X, Ũ)

given by the formula (F, s) ↦ s∘Q(F) is a bijection. The inverse bijection is given by the formula F̃ ↦ (F̃ ∘ p, Id_{X} ∗_{F̃∘p} F̃) where Id_{X} ∗_{F̃∘p} F̃ is defined because Id_{X} ∘ F̃ ∘ p = F̃ ∘ p.

Proof. Let us denote the first function by Φ and second one by Ψ. We have

Φ(Ψ(F̃)) = Φ(F̃ ∘ p, Id_{X} ∗_{F̃∘p} F̃) = (Id_{X} ∗_{F̃∘p} F̃) ∘ Q(F̃ ∘ p) = F̃

where the last equality is by the definition of ∗_{F̃∘p}, and

Ψ(Φ(F, s)) = Ψ(s ∘ Q(F)) = ((s ∘ Q(F)) ∘ p, Id_{X} ∗_{(s∘Q(F))∘p} (s ∘ Q(F)))

Next we have

s ∘ Q(F) ∘ p = s ∘ p_{F} ∘ F = F  (2.45)

It remains to compare Id_{X} ∗_{s∘Q(F)∘p} (s ∘ Q(F)) with s. To do it we need to compare its post-compositions with p_{F} and Q(F) with the same post-compositions for s.

By (2.45) we may replace s ∘ Q(F) ∘ p with F. We have

Id_{X} ∗_{F} (s ∘ Q(F)) ∘ p_{F} = Id_{X} = s ∘ p_{F}
Id_{X} ∗_{F} (s ∘ Q(F)) ∘ Q(F) = s ∘ Q(F) = s ∘ Q(F)

Therefore, Id_{X} ∗_{F} (s ∘ Q(F)) = s and

Ψ(Φ(F, s)) = (F, s)

The lemma is proved.

2.3.7. Lemma. Let p : Y → X be a morphism in C and Φ : C → C′ a functor. Then for s ∈ sec(p) one has Φ(s) ∈ sec(Φ(p)).

If Φ is fully faithful then the resulting function

Φ_{sec,p} : sec(p) → sec(Φ(p))

is a bijection.

Proof. The first assertion follows immediately from the definition of sec and the axioms of a functor.

Assume that Φ is fully faithful. To prove that Φ_{sec,p} is a bijection let

Φ_{A,B}^{−1} : Mor_{C′}(Φ(A), Φ(B)) → Mor_{C}(A, B)

be the inverse to the function Φ_{A,B} : Mor_{C}(A, B) → Mor_{C′}(Φ(B), Φ(B)) that we denoted simply by Φ. One verifies easily that for any A, B, C ∈ C the functions Φ_{A,B}^{−1}, Φ_{B,C}^{−1} and Φ_{A,C}^{−1} commute with the compositions and for any A ∈ C one has Φ_{A,A}^{−1}(Id_{Φ(A)}) = Id_{A}.

Therefore, for s′ ∈ sec(Φ_{Y,X}(p)) we have Φ_{X,Y}^{−1} (s′) ∈ sec(p). Indeed,

Φ_{X,X}(Φ_{X,Y}^{−1} (s′) ∘ p) = Φ_{X,Y} (Φ_{X,Y}^{−1} (s′)) ∘ Φ_{Y,X}(p) = s′ ∘ Φ_{Y,X}(p) = Id_{Φ(X)}

and since Φ_{X,X}^{−1}(Id_{Φ(X)}) = Id_{X} we obtain that Φ_{X,Y}^{−1} (s′) ∘ p = Id_{X}. This implies that Φ_{sec,p} and the restriction of Φ_{X,Y}^{−1} to sec(Φ(p)) form a pair of functions between sec(p) and sec(Φ(p)) and one sees immediately that they are mutually inverse.

2.3.8. Construction. By definition of int^{∘} and Y o and Lemma 2.1.4, an isomorphism of presheaves of the form (2.43) is a family of functions of the form

ũ_{1,Γ} : Õb_{1}(Γ) → Mor_{C}(int(Γ), Ũ)

parametrized by Γ ∈ Ob(CC(C, p)) such that for any f : Γ′ → Γ and any o ∈ Õb_{1}(Γ) one has

ũ_{1,Γ′}(f^{∗}(o)) = int(f) ∘ ũ_{1,Γ}(o)  (2.46)

and for any Γ the function ũ_{1,Γ} is a bijection.

The equalities (2.44) define our family completely and it remains to prove (2.46) and the bijectivity condition.

For the proof of (2.46) we have the following, where we write u instead of u_{1,Γ} and u_{1,Γ′} and ũ instead of ũ_{1,Γ} and ũ_{1,Γ′},

ũ(f^{∗}(o)) = int(f^{∗}(o)) ∘ Q(u(∂(f^{∗}(o)))) = int(f^{∗}(o)) ∘ Q(u(f^{∗}(∂(o)))) =
int(f^{∗}(o)) ∘ Q(int(f) ∘ u(∂(o))) = int(f^{∗}(o)) ∘ Q(int(f), u(∂(o))) ∘ Q(u(∂(o))) =
int(f^{∗}(o)) ∘ int(q(f, ∂(o))) ∘ Q(u(∂(o))) = int(f^{∗}(o) ∘ q(f, ∂(o))) ∘ Q(u(∂(o))) =
int(q(f, Γ) ∘ o) ∘ Q(u(∂(o))) = int(f ∘ o) ∘ Q(u(∂(o))) =
int(f) ∘ int(o) ∘ Q(u(∂(o))) = int(f) ∘ ũ(o)

where the first equality is by (2.44), second is by definition of f^{∗}(o), the third is by (2.38), the fourth is by (2.19), the fifth is by (2.41), the sixth is because int is a functor, the seventh is by [8, (2.19)], the eighth is by definition of q(f, −), the ninth is because int is a functor and the tenth is again by (2.44). This completes the proof of (2.46).

To prove that the function ũ_{1,Γ} is a bijection we will represent it as the composition of functions that we can show to be bijections. The functions are of the form

Õb_{1}(Γ) → ⨿_{T ∈Ob_{1}(Γ)}∂^{−1}(T) → ⨿_{F:int(Γ)→U}sec(p_{F}) → Mor(int(Γ), Ũ)

and are given by the formulas

o ↦ (∂(o), o)  (T, o) ↦ (u(T), int(o))  (F, s) ↦ s ∘ Q(F)

The first function is the function X → ⨿_{y∈Y} f^{−1}(y), which is defined and is a bijection for any function of sets f : X → Y. The second one is the total function of the function u and the family of functions int_{sec,p_{T}} of Lemma 2.3.7. Since u and the functions int_{sec,p_{T}} are bijections the total function is a bijection. The third function is the bijection of Lemma 2.3.6.

Let us show that the composition of these bijections equals ũ. Indeed, for o ∈ Õb_{1}(Γ) we have

o ↦ (∂(o), o) ↦ (u(∂(o)), int(o)) ↦ int(o) ∘ Q(u(∂(o))) = ũ(o)

This completes Construction 2.3.8.

2.3.9. Remark. The inverse to ũ_{1,Γ} can be expressed by the formula

ũ_{1,Γ}^{−1}(H) = int_{Γ,u_{1,Γ}^{−1}(H∘p)}^{−1}(Id_{int(Γ)} ∗_{H∘p} H)

Note that while we can omit explicitly mentioning dom(f) and codom(f) when we write int(f) we must specify them when we write int^{−1}(f) because int is bijective only on the subsets of morphisms with fixed domain and codomain. This makes the expression for ũ_{1,Γ}^{−1} longer than one would prefer.

The family of functions ∂_{Γ} forms a morphism of presheaves Õb_{n} → Ob_{n} that we usually denote simply by ∂.

2.3.10. Lemma. The square of morphisms of presheaves

\begin{matrix}Õb_{1} & \underrightarrow{ũ_{1}} & int^{∘}(Y o(Ũ)) \\ ^{∂}↓ & & ↓^{int^{∘}(Y o(p))} \\ Ob_{1} & ⟶^{u_{1}} & int^{∘}(Y o(U)) \end{matrix}  (2.47)

commutes.

Proof. For Γ and o ∈ Õb_{1}(Γ) we have

int^{∘}(Y o(p))_{Γ}(ũ_{1,Γ}(o)) = (ũ_{1,Γ}(o)) ∘ p = int(o) ∘ Q(u_{1,Γ}(∂(o))) ∘ p =
int(o) ∘ p_{u_{1,Γ}(∂(o))} ∘ u_{1,Γ}(∂(o)) = int(o ∘ p_{∂(o)}) ∘ u_{1,Γ}(∂(o)) = u_{1,Γ}(∂(o))

where the first equality is by definition of int^{∘} and Y o, the second by (2.44), the third by commutativity of (2.15), the fourth by (2.40) and the fifth by the definition Õb_{1}(Γ) in (2.2) and the fact that ∂(o) = codom(o). The lemma is proved.

2.4. Functor isomorphisms SD_{p}. In this section we continue to consider a universe category (C, p). For any (C, p) we will relate the functor D_{p} on P reShv(C) and the functor Sig on P reShv(CC(C, p)).

2.4.1. Problem. For a universe category (C, p) to construct an isomorphism of functors from P reShv(C) to P reShv(CC) of the form

SD_{p} : int^{∘} ∘ Sig → D_{p} ∘ int^{∘}

2.4.2. Construction. In view of Lemma 2.1.4, we have to construct, for any G ∈ P reShv(C), an isomorphism of presheaves on CC(C, p) of the form

SD_{p,G} : Sig(int^{op} ∘ G) → int^{op} ∘ D_{p}(G)

and to show that these isomorphisms are natural in G, that is, that for a morphism of presheaves r : G → G′ one has

SD_{p,G} ∘ int^{∘}(D_{p}(r)) = Sig(int^{∘}(r)) ∘ SD_{p,G′}

Applying Lemma 2.1.4 again, we see that we need to construct, for each G and Γ ∈ CC(C, p), a bijection SD_{p,G,Γ}, which we will denote ϕ_{G,Γ} for the duration of the proof, of the form

ϕ_{G,Γ} : Sig(int^{op} ∘ G)(Γ) → (int^{op} ∘ D_{p}(G))(Γ) = D_{p}(G)(int(Γ))

and to show that two conditions hold:

1. for any f : Γ′ → Γ we have

ϕ_{G,Γ} ∘ D_{p}(G)(int(f)) = Sig(int^{op} ∘ G)(f) ∘ ϕ_{G,Γ′}  (2.48)

that is, the square

\begin{matrix}Sig(int^{op} ∘ G)(Γ) & ⟶^{ϕ_{G,Γ}} & D_{p}(G)(int(Γ)) \\ ^{Sig(int^{op}∘G)(f)}↓ & & ↓^{D_{p}(G)(int(f))} \\ Sig(int^{op} ∘ G)(Γ′) & ⟶^{ϕ_{G,Γ′}} & D_{p}(G)(int(Γ′)) \end{matrix}  (2.49)

commutes.

2. for any r : G → G′ and Γ ∈ CC(C, p) we have

ϕ_{G,Γ} ∘ D_{p}(r)_{int(Γ)} = Sig(int^{∘}(r))_{Γ} ∘ ϕ_{G′,Γ}  (2.50)

that is, the square

Sig(int^{op} ∘ G)(Γ) ⟶^{ϕ_{G,Γ}} D_{p}(G)(int(Γ))
Sig(int^{∘}(r))_{Γ}↓  ↓^{D_{p}(r)_{int(Γ)}}
Sig(int^{op} ∘ G′)(Γ) ⟶^{ϕ_{G,Γ}} D_{p}(G′)(int(Γ))

(2.51)

commutes.

To construct ϕ_{G,Γ} we first compute using (2.3)

Sig(int^{op} ∘ G)(Γ) = ⨿_{T ∈Ob_{1}(Γ)}G(int(T))

and using (2.22)

D_{p}(G)(int(Γ)) = ⨿_{F:int(Γ)→U}G((int(Γ); F))

and define the function ϕ_{G,Γ} by the formula

ϕ_{G,Γ}((T, g)) = (u_{1,Γ}(T), g)  (2.52)

where the right hand side is defined because of (2.39). The function ϕ_{G,Γ} is a bijection as the total function of the bijection u_{1,Γ} and the family of bijections, namely the identity functions.

To prove equality (2.48) we compute using (2.4)

Sig(int ∘ G)(f)(T, g) = (f^{∗}(T), G(int(q(f, T)))(int(T)))

and using (2.23)

D_{p}(G)(int(f))(F, g) = (int(f) ∘ F, G(Q(int(f), F))(g))

Equality (2.48) follows now from (2.38) and (2.41).

To prove equality (2.50) we compute using (2.5)

Sig(int^{∘}(r))_{Γ}(T, g) = (T, r_{int(T)}(g))

and using (2.24)

D_{p}(r)_{int(Γ)}(F, g) = (F, r_{(int(Γ);F)}(g))

and (2.50) follows from (2.39).

This completes Construction 2.4.2.

2.5. Isomorphisms of presheaves u_{n} and ũ_{n} for n ≥ 2. In this section we continue to consider a universe category (C, p). For any such (C, p) and any n ≥ 1, we construct isomorphisms of presheaves on CC(C, p) of the form

u_{n} : Ob_{n} → int^{∘}(D_{p}^{n−1}(Y o(U)))  (2.53)

and

ũ_{n} : Õb_{n} → int^{∘}(D_{p}^{n−1}(Y o(Ũ)))  (2.54)

where D_{p}^{0} = Id_{P reShv(C)}, and u_{1} and ũ_{1} are the isomorphisms constructed in Section 2.3. We show that

ũ_{n} ∘ int^{∘}(D_{p}^{n−1}(Y o(p))) = ∂ ∘ ũ_{n}  (2.55)

Let us fix a universe category (C, p).

2.5.1. Problem. Let n ≥ 2. To construct an isomorphism of presheaves on CC(C, p) of the form (2.53).

2.5.2. Construction. We proceed by induction on n starting with n = 1. Observe that SD_{p,G} is an isomorphism of the form

Sig(int^{∘}(G)) → int^{∘}(D_{p}(G))  (2.56)

The isomorphism u_{1} was constructed in Section 2.3. For the successor, define u_{n+1} as the following composition

\begin{aligned}Ob_{n+1} & ⟶^{SOb_{n}^{−1}} & Sig(Ob_{n}) & ⟶^{Sig(u_{n})} & Sig(int^{∘}(D_{p}^{n−1}(Y o(U)))) & ⟶^{SD_{p,D{n−1 \atop p}(Y o(U))}} \\ & & int^{∘}(D_{p}(D_{p}^{n−1}(Y o(U)))) & & int^{∘}(D_{p}^{n}(Y o(U))) \end{aligned}

The isomorphism u_{n+1,Γ} is of the form

T ↦ (ft^{n}(T), T) ↦ (ft^{n}(T), u_{n,ft^{n}(T)}(T)) ↦ (u_{1,Γ}(ft^{n}(T)), u_{n,ft^{n}(T)}(T))  (2.57)

where the form of the first map is by (2.9), the second by (2.5) and the third by (2.52). In particular, for n = 1 we get

u_{2,Γ}(T) = (u_{1,Γ}(ft(T)), u_{1,ft(T)}(T))

2.5.3. Problem. Let n ≥ 2. To construct an isomorphism of presheaves on CC(C, p) of the form (2.54).

2.5.4. Construction. We proceed by induction on n starting with n = 1. The isomorphism ũ_{1} was constructed in Section 2.3. For the successor, define ũ_{n+1} as the following composition, where we use that SD_{p,G} is of the form (2.56),

\begin{aligned}Õb_{n+1} & ⟶^{SÕb_{n}^{−1}} & Sig(Õb_{n}) & ⟶^{Sig(ũ_{n})} & Sig(int^{∘}(D_{p}^{n−1}(Y o(Ũ)))) & ⟶^{SD_{p,D{n−1 \atop p}(Y o(Ũ))}} \\ & & int^{∘}(D_{p}(D_{p}^{n−1}(Y o(Ũ)))) & & int^{∘}(D_{p}^{n}(Y o(Ũ))) \end{aligned}

The isomorphism ũ_{n+1,Γ} is of the form

o ↦ (ft^{n}(∂(o)), o) ↦ (ft^{n}(∂(o)), ũ_{n,ft^{n}(∂(o))}(o)) ↦ (u_{1,Γ}(ft^{n}(∂(o))), ũ_{n,ft^{n}(∂(o))}(o)) (2.58)

where the form of the first map is by (2.12), the second by (2.5) and the third by (2.52). In particular, for n = 1 we get

ũ_{2,Γ}(o) = (u_{1,Γ}(ft(∂(o))), ũ_{1,ft(∂(o))}(o))

2.5.5. Lemma. For any n ≥ 1, (2.55) holds, that is, the square

Õb_{n} \underrightarrow{ũ_{n}} int^{∘}(D_{p}^{n−1}(Y o(Ũ)))
∂↓  ↓^{int^{∘}(D_{p}^{n−1}(Y o(p)))}
Ob_{n} ⟶^{u_{n}} int^{∘}(D_{p}^{n−1}(Y o(U)))

commutes.

Proof. We proceed by induction on n starting at n = 1. For n = 1 it is shown in Lemma 2.3.10.

For the successor of n we have the diagram

Õb_{n+1} ⟶^{SÕb_{n}^{−1}} Sig(Õb_{n}) ⟶^{Sig(ũ_{n})} Sig(int^{∘}(D_{p}^{n}(Y o(Ũ)))) ⟶^{SD_{p}} int^{∘}(D_{p}(D_{p}^{n}(Y o(Ũ))))
∂↓  ^{Sig(∂)}↓  ^{Sig(int^{∘}(D_{p}^{n}(Y o(p))))}↓  ^{int^{∘}(D_{p}(D_{p}^{n}(Y o(p))))}↓
Ob_{n+1} ⟶^{SOb_{n}^{−1}} Sig(Ob_{n}) ⟶^{Sig(u_{n})} Sig(int^{∘}(D_{p}^{n}(Y o(U)))) ⟶^{SD_{p}} int^{∘}(D_{p}(D_{p}^{n}(Y o(U))))

where the composition of the upper horizontal arrows is ũ_{n} and the composition of the lower horizontal ones is u_{n}. To prove the lemma it is sufficient to show that the three squares of the diagram commute.

The commutativity of the left square follows easily from Lemma 2.1.10. The middle square commutes by the inductive assumption using the fact that Sig is a functor. The right square commutes because SD_{p} is an isomorphism of functors, that is, it is natural in morphisms of presheaves.

2.6. The case of a locally cartesian closed C - isomorphisms η_{n} and μ_{n}. In this section C is a locally cartesian closed category (see Appendix 4.2) with a binary product structure (see Appendix 4.1).

The main construction of this section is Construction 2.6.4 for Problem 2.6.3 that provides, for a universe p in a category C as above, representations for the presheaves D_{p}(Y o(Y)). As a corollary we provide constructions for Problems 2.6.5 and 2.6.8.

For a morphism p : Ũ → U in C and an object Y of C let

I_{p}(Y) := \underline{Hom}_{U}((Ũ, p), (U × Y, pr_{1}))

and let

prI_{p}(Y) = p△pr_{1} : I_{p}(Y) → U

be the canonical morphism.

For a morphism f : Y → Y′ let

I_{p}(f) = \underline{Hom}_{U}((Ũ, p), U × f)

By (4.10),(4.11) and Definition 4.1.4(3) we have

I_{p}(Id_{Y}) = Id_{I_{p}(Y)}

and for f′ : Y′ → Y′′ we have

I_{p}(f ∘ f′) = I_{p}(f) ∘ I_{p}(f′)

which shows that the mappings Y ↦ I_{p}(Y) and f ↦ I_{p}(f) define a functor from C to itself.

The main goal of this section is to construct an isomorphism η between functors from C to P reShv(C) of the form:

η : Y o ∘ D_{p} → I_{p} ∘ Y o

This isomorphism provides, in particular, a family, parametrized by Y ∈ C, of representations for the functors D_{p}(Y o(Y)).

Note that I_{p} depends on the choice of both the locally cartesian closed and the binary product structures on C, but does not depend on the universe structure. On the other hand, the construction of the functors D_{p}(F) requires a universe structure on p but does not require either the locally cartesian closed or the binary product structure on C.

The computations below are required because we have to deal with this fact. In particular, we have to take into the account that for F : X → U the fiber product (X, F) ×_{U} (Ũ, p) that we have from the structure of a category with pullbacks on C need not be equal to (X; F) that we have from the universe structure on p.

Let p : Ũ → U be a universe and Y an object of C. We assume that C is equipped with a locally cartesian closed and a binary product structures. For F : X → U there is a unique morphism

ι_{F} : (X; F) → (X, F) ×_{U} (Ũ, p)

such that

\begin{matrix}ι_{F} ∘ pr_{1} = p_{F} \\ ι_{F} ∘ pr_{2} = Q(F) \end{matrix}  (2.59)

which is a particular case of the morphisms ι of Lemma 4.1.3. The evaluation morphism in the case of I_{p}(Y) is a morphism in C/U of the form

evI_{p} : (I_{p}(Y), prI_{p}(Y)) ×_{U} (U × Y, pr_{1}) → (U × Y, pr_{1})

Define a morphism

st_{p}(Y) : (I_{p}(Y); prI_{p}(Y)) → Y

as the composition:

st_{p}(Y) := ι_{prI_{p}(Y)} ∘ evI_{p}(Y) ∘ pr_{2}  (2.60)

We will need to use some properties of these morphisms.

2.6.1. Lemma. Let f : Y → Y′ be a morphism, then one has

Q(I_{p}(f), prI_{p}(Y′)) ∘ st_{p}(Y′) = st_{p}(Y) ∘ f

Proof. Let pr = prI_{p}(Y), pr′ = prI_{p}(Y′), ι = ι_{pr}, ι′ = ι_{pr′}, ev = evI_{p}(Y) and ev′ = evI_{p}(Y′). Then we have to verify that the outer square of the following diagram commutes:

(I_{p}(Y); pr) ⟶^{ι} (I_{p}(Y), pr) ×_{U} (Ũ, p) ⟶^{ev} U × Y ⟶^{pr_{2}} Y
Q(I_{p}(f),pr′)↓  ^{I_{p}(f)×IdŨ} ↓  ^{Id_{U} ×f}↓  ↓^{f}
(I_{p}(Y′); pr′) ⟶^{ι′} (I_{p}(Y′), pr′) ×_{U} (Ũ, p) ⟶^{ev′} U × Y′ ⟶^{pr_{2}} Y′

The commutativity of the left square is a particular case of Lemma 4.1.3. The commutativity of the right square is an immediate corollary of the definition of Id_{U} × f. The commutativity of the middle square is a particular case of (4.7).

2.6.2. Remark. In [3] generalized polynomial functors are defined as functors isomorphic to functors of the form I_{p}.

2.6.3. Problem. Let C be a locally cartesian closed category with a binary product structure and p a universe in C. To construct, for all Y ∈ C, isomorphisms of presheaves

η_{Y} : D_{p}(Y o(Y)) → Y o(I_{p}(Y))

that are natural in Y, i.e., such that for all f : Y → Y′ the square

D_{p}(Y o(Y)) ⟶^{D_{p}(Y o(f))} D_{p}(Y o(Y′))
η_{Y} ↓  ↓^{η_{Y′}}
Y o(I_{p}(Y)) ⟶^{Y o(I_{p}(f))} Y o(I_{p}(Y′))

commutes.

2.6.4. Construction. We will use the notation introduced before Remark 2.2.5. We need to construct bijections

η_{Y,X} : D_{p}(X, Y) → Mor_{C}(X, I_{p}(Y))

such that for all f : Y → Y′, X ∈ C and d ∈ D_{p}(X, Y) one has

η_{Y,X}(d) ∘ I_{p}(f) = η_{Y′,X}(d ∘ f)  (2.61)

and for any f : X′ → X and d ∈ D_{p}(Y o(Y))(X) one has

f ∘ η_{Y,X}(d) = η_{Y,X′}(f ∘ d)  (2.62)

We will construct bijections

η_{Y,X}^{!} : Mor(X, I_{p}(Y)) → D_{p}(X, Y)

such that for all g : X → I_{p}(Y) one has:

1. for all f : Y → Y′ one has

η^{!}(g) ∘ f = η^{!}(g ∘ I_{p}(f))  (2.63)

2. for all f : X′ → X one has

f ∘ η^{!}(g) = η^{!}(f ∘ g)  (2.64)

and then define η_{Y,X} as the inverse to η_{Y,X}^{!}. One proves easily that (2.61) implies (2.63) and (2.62) implies (2.64).

By (2.27) we have

D_{p}(X, Y) = ⨿_{F:X→U}Mor_{C}((X; F), Y)

For g : X → I_{p}(Y) we set

η_{Y,X}^{!}(g) := (g ∘ prI_{p}(Y), Q(g, prI_{p}(Y)) ∘ st_{p}(Y))  (2.65)

as can be seen on the diagram

Y
↑^{st_{p}(Y)}
(X; g ∘ prI_{p}(Y)) ⟶^{Q(g,prI_{p}(Y))} (I_{p}(Y); prI_{p}(Y)) ⟶^{Q(prI_{p}(Y))} Ũ
↓  ↓  ↓^{p}
X  ⟶^{g}  I_{p}(Y)  ⟶^{prI_{p}(Y)} U

To see that this is a bijection observe first that it equals the composition

Mor(X, I_{p}(Y)) → ⨿_{F:X→U}Mor_{U}((X, F), (I_{p}(Y), prI_{p}(Y))) → ⨿_{F:X→U}Mor((X; F), Y)

where the first function is given by the formula g ↦ (g ∘ prI_{p}(Y), g) and the second is the sum over all F : X → U of functions g ↦ Q(g, prI_{p}(Y)) ∘ st_{p}(Y).

The first function is a function of the form A → ⨿_{b∈B}h^{−1}(b), which is defined and is a bijection for any function of sets h : A → B. It remains to show that the second one is a bijection for every F.

By definition of the \underline{Hom}_{U} structure we know that for each F the function

adj : Mor_{U}((X, F), (I_{p}(Y), prI_{p}(Y))) → Mor_{U}((X, F) ×_{U} (Ũ, p), (U × Y, pr_{1}))

given by g ↦ (g ×_{U} Id_{(Ũ,p)}) ∘ evI_{p}(Y) is a bijection.

By definition of the binary product, the function of post-composition with pr_{2},

Mor_{U}((X, F) ×_{U} (Ũ, p), (U × Y, pr_{1})) → Mor((X, F) ×_{U} (Ũ, p), Y)

is a bijection. By Lemma 4.1.2, ι_{F} is an isomorphism and therefore the pre-composition with it is a bijection. Now we have two functions

Mor_{U}((X, F), (I_{p}(Y), prI_{p}(Y))) → Mor((X; F), Y)

given by g ↦ ι_{F} ∘ (g ×_{U} IdŨ) ∘ evI_{p}(Y) ∘ pr_{2} and g ↦ Q(g, prI_{p}(Y)) ∘ st_{p}(Y) of which the first one is the bijection. It remains to show that these functions are equal. In view of (2.60) it is sufficient to show that

ι_{F} ∘ (g ×_{U} IdŨ) = Q(g, prI_{p}(Y)) ∘ ι_{prI_{p}(Y)}

To do it we have to show that the compositions of the left and right hand sides with pr_{1} (to I_{p}(Y)) and pr_{2} (to Ũ) are equal.

For pr_{1} we have

ι_{F} ∘ (g ×_{U} IdŨ) ∘ pr_{1} = ι_{F} ∘ pr_{1} ∘ g = p_{F} ∘ g

Q(g, prI_{p}(Y)) ∘ ι_{prI_{p}(Y)} ∘ pr_{1} = Q(g, prI_{p}(Y)) ∘ p_{prI_{p}(Y)} = p_{g∘prI_{p}(Y)} ∘ g = p_{F} ∘ g

where we used the defining equations (2.59) of ι, the definition (2.18) of Q(−, −) and the fact that g is a morphism over U.

For pr_{2} we have

ι_{F} ∘ (g ×_{U} IdŨ) ∘ pr_{2} = ι_{F} ∘ pr_{2} ∘ IdŨ = ι_{F} ∘ pr_{2} = Q(F)

Q(g, prI_{p}(Y)) ∘ ι_{prI_{p}(Y)} ∘ pr_{2} = Q(g, prI_{p}(Y)) ∘ Q(prI_{p}(Y)) = Q(g ∘ prI_{p}(Y)) = Q(F)

where we used the defining equations (2.59) of ι, (2.19) and the fact that g is a morphism over U.

We now have to check the behavior of η^{!} with respect to morphisms in Y (equality (2.63)) and X (equality (2.64).

Let pr = prI_{p}(Y) and pr′ = prI_{p}(Y′). Let g : X → I_{p}(Y) be as above. For f : Y → Y′ we have

η^{!}(g) ∘ f = D_{p}(Y o(f))_{X}(g ∘ pr, Q(g, pr) ∘ st_{p}(Y)) = (g ∘ pr, Q(g, pr) ∘ st_{p}(Y) ∘ f)

where the first equality is by (2.65) and the second by (2.29) and

η^{!}(g ∘ I_{p}(f)) = (g ∘ I_{p}(f) ∘ pr′, Q(g ∘ I_{p}(f), pr′) ∘ st_{p}(Y′))

where the equality is by (2.65). We have pr = I_{p}(f) ∘ pr′ because I_{p}(f) is a morphism over U. It remains to check that

Q(g, pr) ∘ st_{p}(Y) ∘ f = Q(g ∘ I_{p}(f), pr′) ∘ st_{p}(Y′)

By [6, Lemma 2.5] we have

Q(g ∘ I_{p}(f), pr′) = Q(g, pr) ∘ Q(I_{p}(f), pr′)

and the remaining equality

Q(g, pr) ∘ st_{p}(Y) ∘ f = Q(g, pr) ∘ Q(I_{p}(f), pr′) ∘ st_{p}(Y′)

follows from Lemma 2.6.1.

Consider now f : X′ → X. Then

f ∘ η^{!}(g) = D_{p}(Y o(Y))(f)(g ∘ pr, Q(g, pr) ∘ st_{p}(Y)) =
(f ∘ g ∘ pr, Q(f, g ∘ pr) ∘ Q(g, pr) ∘ st_{p}(Y))

and

η^{!}(f ∘ g) = (f ∘ g ∘ pr, Q(f ∘ g, pr) ∘ st_{p}(Y))

where we used (2.65) and (2.28) and the required equality follows from [6, Lemma 2.5].

2.6.5. Problem. For a locally cartesian closed category C with a binary product structure and a universe p in C to construct, for all n ≥ 0 and Y ∈ C, isomorphisms of presheaves

η_{n,Y} : D_{p}^{n}(Y o(Y)) → Y o(I_{p}^{n}(Y))

that are natural in Y, i.e., such that for all f : Y → Y′ the square

\begin{matrix}D_{p}^{n}(Y o(Y)) & ⟶^{D_{p}^{n}(Y o(f))} & D_{p}^{n}(Y o(Y′)) \\ ^{η_{n,Y}} ↓ & & ↓^{η_{n,Y′}} \\ Y o(I_{p}^{n}(Y)) & ⟶^{Y o(I_{p}^{n}(f))} & Y o(I_{p}^{n}(Y′)) \end{matrix}  (2.66)

commutes.

2.6.6. Construction. Proceed by induction on n starting with n = 0. By our convention, D_{p}^{0} = Id_{P reShv(C)} and I_{p}^{0} = Id_{C}. We set η_{0,Y} = Id_{Y o(Y)}. For the successor we define η_{n+1,Y} as the composition

D_{p}^{n+1}(Y o(Y)) =
D_{p}(D_{p}^{n}(Y o(Y))) ⟶^{D_{p}(η_{n,Y} )} D_{p}(Y o(I_{p}^{n}(Y))) ⟶^{η_{1,I^{n}_{p}(Y )}} Y o(I_{p}(I_{p}^{n}(Y))) =
Y o(I_{p}^{n+1}(Y))

The naturality in Y is easily proved by induction.

Note that we can write η_{n,Y,X} as a function of the form

D_{p}^{n}(X, Y) → Mor_{C}(X, I_{p}^{n}(Y))

Let us spell out the formulas expressing the fact that η_{n,Y} is a morphism of presheaves and the naturality of η_{n,Y} in Y in the ∘-notation. Let d ∈ D_{p}^{n}(X, Y). Then for f : X′ → X one has

η_{n}(f ∘ d) = f ∘ η_{n}(d)  (2.67)

and for g : Y → Y′ one has

η_{n}(d ∘ g) = η_{n}(d) ∘ I_{p}^{n}(g)  (2.68)

Indeed, the first formula is an expression of the fact that the family of functions η_{n,Y,−} is a morphism of presheaves and the second formula an expression of the commutativity of the square (2.66).

We let η_{n,Y}^{!} denote the isomorphism inverse to η_{n,Y}. For m : X → I_{p}^{n}(Y) we have the following formulas that follow from (2.67) and (2.68). For f : X → X′ one has

f ∘ η_{n}^{!}(m) = η_{n}^{!}(f ∘ m)  (2.69)

and for g : Y → Y′ one has

η_{n}^{!}(m) ∘ g = η_{n}^{!}(m ∘ I_{p}^{n}(g))  (2.70)

Let us also introduce the following notation that will be useful below. For Y ∈ C let

Id_{Y}^{n} = η_{n}^{!}(Id_{I_{p}^{n}(Y)}) ∈ D_{p}^{n}(I_{p}^{n}(Y), Y)  (2.71)

We have the following formulas.

2.6.7. Lemma. In the notations introduced above one has:

1. for m : X → I_{p}^{n}(Y) one has

m ∘ Id_{Y}^{n} = η_{n}^{!}(m)  (2.72)

2. for g : Y → Y′ one has

Id_{Y}^{n} ∘ g = η_{n}^{!}(I_{p}^{n}(g))  (2.73)

Proof. For the first formula we have

m ∘ Id_{Y}^{n} = m ∘ η_{n}^{!}(Id_{I_{p}^{n}(Y)}) = η_{n}^{!}(m ∘ Id_{I_{p}^{n}(Y)}) = η_{n}^{!}(m)

where the first equality is by the definition of Id_{Y}^{n}, the second by (2.69) and the third by the identity axiom of C.

For the second formula we have

Id_{n}^{Y} ∘ g = η_{n}^{!}(Id_{I_{p}^{n}(Y)}) ∘ g = η_{n}^{!}(Id_{I_{p}^{n}(Y)} ∘ I_{p}^{n}(g)) = η_{n}^{!}(I_{p}^{n}(g))

where the first equality is by the definition of Id_{Y}^{n}, the second by (2.70) and the third by the identity axiom of C. The lemma is proved.

Note that (2.72) implies in particular that we have

η_{n}(d) ∘ Id_{Y}^{n} = η_{n}^{!}(η_{n}(d)) = d  (2.74)

2.6.8. Problem. For C as above, a universe p : Ũ → U in C and n ≥ 1 to construct isomorphisms of presheaves

μ_{n} : Ob_{n} → int^{∘}(Y o(I_{p}^{n−1}(U)))

and

μ̃_{n} : Õb_{n} → int^{∘}(Y o(I_{p}^{n−1}(Ũ)))

such that the square

\begin{matrix}Õb_{n} & \underrightarrow{μ̃_{n}} & int^{∘}(Y o(I_{p}^{n−1}(Ũ))) \\ ^{∂}↓ & & ↓^{int^{∘}(Y o(I_{p}^{n−1}(p)))} \\ Ob_{n} & ⟶^{μ_{n}} & int^{∘}(Y o(I_{p}^{n−1}(U))) \end{matrix}  (2.75)

commutes.

2.6.9. Construction. Compose isomorphism u_{n} of Construction 2.5.2 (resp. isomorphism ũ_{n} of Construction 2.5.4) with the isomorphism int^{∘}(η_{n−1,U}) (resp. int^{∘}(η_{n−1,Ũ})) where η_{n−1,U} (resp. η_{n−1,Ũ}) is the isomorphism of Construction 2.6.6.

To prove the commutativity of (2.75) consider the diagram

Õb_{n} \underrightarrow{ũ_{n}} int^{∘}(D_{p}^{n−1}(Y o(Ũ))) ⟶^{int^{∘}(η_{n−1,Ũ})} int^{∘}(Y o(I_{p}^{n−1}(Ũ)))
∂↓ ^{int^{∘}(D_{p}^{n−1}(Y o(p)))}↓  ↓^{int^{∘}(Y o(I_{p}^{n−1}(p)))}
Ob_{n} ⟶^{u_{n}} int^{∘}(D_{p}^{n−1}(Y o(U))) ⟶^{int^{∘}(η_{n−1,U})} int^{∘}(Y o(I_{p}^{n−1}(U)))

The composition of the upper arrows is μ̃_{n} and the composition of the lower ones is μ_{n}. It remains to show that the two squares commute. The left square commutes by Lemma 2.5.5. The right square commutes because int^{∘} is a functor and η_{n−1,Y} is natural in Y.

Observe that for Γ ∈ CC(C, p), T ∈ Ob_{n}(Γ) and o ∈ Õb_{n}(Γ) one has:

μ_{n,Γ}(T) = η_{n−1,U,int(Γ)}(u_{n,Γ}(T)) ∈ int^{∘}(Y o(I_{p}^{n−1}(U)))(Γ) = Mor_{C}(int(Γ), I_{p}^{n−1}(U))

(2.76)

and

μ̃_{n,Γ}(o) = η_{n−1,Ũ,int(Γ)}(ũ_{n,Γ}(o)) ∈ int^{∘}(Y o(I_{p}^{n−1}(Ũ)))(Γ) = Mor_{C}(int(Γ), I_{p}^{n−1}(Ũ)) (2.77)

and the commutativity of (2.75) is equivalent to the assertion that for all Γ and o as above one has

μ_{n,Γ}(∂(o)) = μ̃_{n,Γ}(o) ∘ I_{p}^{n}(p)  (2.78)

3. Functoriality

3.1. Universe category functors and the D_{p} construction. Let (C, p, pt) and (C′, p′, pt′) be two universe categories. Recall from [6] the following definition.

3.1.1. Definition. A universe category functor from (C, p, pt) to (C′, p′, pt′) is a triple Φ = (Φ, ϕ, ϕ̃) where Φ is a functor C → C′ and ϕ : Φ(U) → U′, ϕ̃ : Φ(Ũ) → Ũ′ are two morphisms such that one has:

1. Φ takes pt to a final object,

2. Φ takes the canonical pullbacks based on p to pullbacks,

3. the square

\begin{matrix}Φ(Ũ) & \underrightarrow{ϕ̃} & Ũ′ \\ ^{Φ(p)}↓ & & ↓^{p′} \\ Φ(U) & ⟶^{ϕ} & U′ \end{matrix}  (3.1)

is a pullback.

3.1.2. Problem. Let Φ = (Φ, ϕ, ϕ̃) be a universe category functor (C, p) → (C′, p′). To construct a functor morphism

ΦD : Φ^{∘} ∘ D_{p} → D_{p′} ∘ Φ^{∘}  (3.2)

3.1.3. Construction. Both the left and the right hand side of (3.2) are functors of the form

P reShv(C′) → P reShv(C)

Therefore, we need, for any presheaf G′ on C′ and any X ∈ C, to construct a function

ΦD_{G′,X} : D_{p}(Φ^{∘}(G′))(X) → Φ^{∘}(D_{p′}(G′))(X)  (3.3)

and to prove that

1. the family ΦD_{G′,−} is a morphism of presheaves, that is, for any a : X → Y in C, the square

D_{p}(Φ^{∘}(G′))(Y) ⟶^{ΦD_{G′,Y}} Φ^{∘}(D_{p′}(G′))(Y)
D_{p}(Φ^{∘}(G′))(a)↓  ↓^{Φ^{∘}(D_{p′}(G′))(a)}
D_{p}(Φ^{∘}(G′))(X) ⟶^{ΦD_{G′,X}} Φ^{∘}(D_{p′}(G′))(X)

(3.4)

commutes,

2. ΦD is a natural transformation of functors to presheaves, that is, for any f′ : F′ → G′ and any X ∈ C the square

D_{p}(Φ^{∘}(F′))(X) ⟶^{ΦD_{F′,X}} Φ^{∘}(D_{p′}(F′))(X)
D_{p}(Φ^{∘}(f′))_{X} ↓  ↓^{Φ^{∘}(D_{p′}(f′))_{X}}
D_{p}(Φ^{∘}(G′))(X) ⟶^{ΦD_{G′,X}} Φ^{∘}(D_{p′}(G′))(X)

(3.5)

commutes.

Computing the left and right hand side of (3.3) we see that ΦD_{G′,X} should be a function of the form

∐_{F:X→U} G′(Φ((X; F))) → ∐_{F′:Φ(X)→U′} G′((Φ(X); F′))

Let F : X → U. Consider (Φ(X); Φ(F) ∘ ϕ). Since (3.1) is a pullback there is a unique morphism q such that q ∘ ϕ̃ = Q(Φ(F) ∘ ϕ) and q ∘ Φ(p) = p_{Φ(X),Φ(F)∘ϕ} ∘ Φ(F). Then the external square in the diagram

(Φ(X); Φ(F) ∘ ϕ) ⟶^{q} Φ(Ũ) \underrightarrow{ϕ̃} Ũ′
↓^{p_{Φ(X),Φ(F)∘ϕ}}  ^{Φ(p)}↓  ↓^{p′}
Φ(X)  ⟶^{Φ(F)} Φ(U) ⟶^{ϕ} U′

is a pullback and since the right hand side square is a pullback, the left hand side square is a pullback as well. Together with the fact that Φ takes pullback squares based on p to pullback squares this implies that we obtain two pullbacks based on Φ(F) ad Φ(p).

By Lemma 4.2.1 and Lemma 4.1.2 we have a unique morphism, which is an isomorphism,

ι_{Φ}^{X,F} : (Φ(X); Φ(F) ∘ ϕ) → Φ((X; F))

such that

ι_{Φ}^{X,F} ∘ Φ(p_{X,F}) = p_{Φ(X),Φ(F)∘ϕ}  (3.6)
ι_{Φ}^{X,F} ∘ Φ(Q(F)) ∘ ϕ̃ = Q(Φ(F) ∘ ϕ)  (3.7)

and we define:

ΦD_{G′,X}(F, γ′) = (Φ(F) ∘ ϕ, G′(ι_{Φ}^{X,F})(γ′))  (3.8)

When no confusion is likely, we will omit the indexes at ι. To prove that (3.4) commutes let

(F : Y → U, γ′ ∈ G′(Φ((Y; F)))) ∈ D_{p}(Φ^{∘}(G′))(Y)

Then one path in the square gives us

(Φ^{∘}(D_{p′}(G′))(a))(ΦD_{F′,X}((F, γ′))) =
(Φ^{∘}(D_{p′}(G′))(a))((Φ(F) ∘ ϕ, G′(ι)(γ′)) = D_{p′}(G′)(Φ(a))((Φ(F) ∘ ϕ, G′(ι)(γ′))) =
(Φ(a) ∘ Φ(F) ∘ ϕ, G′(Q(Φ(a), Φ(F) ∘ ϕ))(G′(ι)(γ′))) =
(Φ(a ∘ F) ∘ ϕ, G′(Q(Φ(a), Φ(F) ∘ ϕ) ∘ ι)(γ′))

where the first equality is by (3.8), the second by the definition of Φ^{∘}, the third by (2.23) and the fourth by the composition axiom of Φ and G′.

The other path gives us

ΦD_{G′,X}(D_{p}(Φ^{∘}(G′))(a)((F, γ′)) =

ΦD_{G′,X}((a ∘ F, Φ^{∘}(G′)(Q(a, F))(γ′))) = ΦD_{G′,X}((a ∘ F, G′(Φ(Q(a, F)))(γ′))) =

(Φ(a ∘ F) ∘ ϕ, G′(ι)(G′(Φ(Q(a, F)))(γ′))) =
(Φ(a ∘ F) ∘ ϕ, G′(ι ∘ Φ(Q(a, F)))(γ′))

where the first equality is by (2.23), the second by the definition of Φ^{∘}, the third by (3.8) and the fourth by the composition axiom of G′.

It remains to show that

Q(Φ(a), Φ(F) ∘ ϕ) ∘ ι = ι ∘ Φ(Q(a, F))  (3.9)

We have four pullbacks

\begin{matrix}(Φ(X); Φ(a ∘ F) ∘ ϕ) & ⟶^{Q(Φ(a∘F)∘ϕ)} & Ũ′ \\ ^{p_{Φ(X),Φ(a∘F)∘ϕ}}↓ & & ↓^{p′} \\ Φ(X) & ⟶^{Φ(a∘F)∘ϕ} & U′ \end{matrix} \begin{matrix}(Φ(Y); Φ(F) ∘ ϕ) & ⟶^{Q(Φ(F)∘ϕ)} & Ũ′ \\ ^{p_{Φ(Y ),Φ(F)∘ϕ}}↓ & & ↓^{p′} \\ Φ(Y) & ⟶^{Φ(F)∘ϕ} & U′ \end{matrix}

and

\begin{matrix}Φ((X; a ∘ F)) & ⟶^{Φ(Q(a∘F))∘ϕ̃} & Ũ′ \\ ^{Φ(p_{X,a∘F})}↓ & & ↓^{p′} \\ Φ(X) & ⟶^{Φ(a∘F)∘ϕ} & U′ \end{matrix} \begin{matrix}Φ((Y; F)) & ⟶^{Φ(Q(F))∘ϕ̃} & Ũ′ \\ ^{Φ(p_{Y,F})}↓ & & ↓^{p′} \\ Φ(Y) & ⟶^{Φ(F)∘ϕ} & U′ \end{matrix}

and a morphism Φ(a) : Φ(X) → Φ(Y) such that Φ(a ∘ F) ∘ ϕ = Φ(a) ∘ Φ(F) ∘ ϕ. Applying to these pullbacks Lemma 4.2.1 and then applying Lemma 4.1.3 we obtain a commutative square

(Φ(X); Φ(a ∘ F) ∘ ϕ) ⟶^{c_{1}(Φ(a),IdŨ′)} (Φ(Y); Φ(F) ∘ ϕ)
ι↓  ↓^{ι}
Φ((X; a ∘ F)) ⟶^{c_{2}(Φ(a),IdŨ′)} Φ((Y; F))

To prove (3.9) it remains to show that

c_{1}(Φ(a), Id′ ; Ũ) = Q(Φ(a), Φ(F) ∘ ϕ)  (3.10)

and

c_{2}(Φ(a), Id′ ; Ũ) = Φ(Q(a, F))  (3.11)

In view of the definition of the morphisms c_{1}, c_{2} given in Lemma 4.1.3 to prove (3.10) we need to show that

Q(Φ(a), Φ(F) ∘ ϕ) ∘ p_{Φ(Y),Φ(F)∘ϕ} = p_{Φ(X),Φ(a∘F)∘ϕ} ∘ Φ(a)
Q(Φ(a), Φ(F) ∘ ϕ) ∘ Q(Φ(F) ∘ ϕ) = Q(Φ(a ∘ F) ∘ ϕ)

The first equality follows from (2.18). The second equality follows from (2.19). In both cases we need also to use that Φ(a ∘ F) = Φ(a) ∘ Φ(F).

To prove (3.11) we need to show that

Φ(Q(a, F)) ∘ Φ(p_{Y,F}) = Φ(p_{X,a∘F}) ∘ Φ(a)
Φ(Q(a, F)) ∘ Φ(Q(F)) ∘ ϕ̃ = Φ(Q(a ∘ F)) ∘ ϕ̃

The first equality again follows from (2.18) and the composition axiom for Φ and the second equality follows from (2.19) and the composition axiom for Φ. This completes the proof of commutativity of (3.4).

To prove that (3.5) commutes let

(F : X → U, β′ ∈ F′(Φ((X; F)))) ∈ D_{p}(Φ^{∘}(F′))(X)

Then one path in the square gives us

Φ^{∘}(D_{p′}(f′))_{X}(ΦD_{F′,X}((F, β′)) =
Φ^{∘}(D_{p′}(f′))_{X}((Φ(F) ∘ ϕ, F′(ι)(β′))) = D_{p′}(f′)_{Φ(X)}((Φ(F) ∘ ϕ, F′(ι)(β′))) =
(Φ(F) ∘ ϕ, f′_{(Φ(X);Φ(F)∘f)}(F′(ι)(β′)))

where the first equality is by (3.8), the second by the definition of Φ^{∘} and the third by (2.24).

The other path gives us

ΦD_{G′,X}(D_{p}(Φ^{∘}(f′))_{X}((F, β′))) =
ΦD_{G′,X}((F, (Φ^{∘}(f′))_{(X;F)}(β′))) = ΦD_{G′,X}((F, f′_{Φ((X;F))}(β′))) =
(Φ(F) ∘ ϕ, G′(ι)(f′_{Φ((X;F))}(β′)))

where the first equality is by (2.24), the second by the definition of Φ^{∘} and the third by (3.8).

It remains to show that

f′_{(Φ(X);Φ(F)∘f)}(F′(ι)(β′)) = G′(ι)(f′_{Φ((X;F))}(β′))

which follows from the axiom of compatibility with morphisms of the natural transformation f′ : F′ → G′. This completes the proof of commutativity of (3.5) and with it Construction 3.1.3.

3.1.4. Problem. Let Φ : (C, p) → (C′, p′) be a universe category functor. Let F ∈ P reShv(C), F′ ∈ P reShv(C′) and let

m : F → Φ^{∘}(F′)

be a morphism of presheaves. Let n ∈ N. To construct a morphism of presheaves

D_{Φ}^{n}(m) : D_{p}^{n}(F) → Φ^{∘}(D_{p′}^{n}(F′))

3.1.5. Construction. We proceed by induction on n.

For n = 0 we set D_{Φ}^{0}(m) = m.

For the successor of n we need to construct a morphism

D_{Φ}^{n+1}(m) : D_{p}(D_{p}^{n}(F)) → Φ^{∘}(D_{p′}(D_{p′}^{n}(F′)))

We define it as the composition

D_{p}(D_{p}^{n}(F)) ⟶^{D_{p}(D_{Φ}^{n}(m))} D_{p}(Φ^{∘}(D_{p′}^{n}(F′))) ⟶^{ΦD_{D{n \atop p′} (F′)}} Φ^{∘}(D_{p′}(D_{p′}^{n}(F′)))

The explicit form of the morphism D_{p}^{n}(m) when n ≥ 1 is given by the following lemma.

3.1.6. Lemma. In the context of Problem 3.1.4, let n ≥ 1, X ∈ C, and

(F, a) ∈ ⨿_{F:X→U}D_{p}^{n−1}(F)((X; F)) = D_{p}^{n}(F)(X)

Then one has

D_{Φ}^{n}(m)_{X}((F, a)) = (Φ(F) ∘ ϕ; D_{p′}^{n−1}(F′)(ι)(D_{Φ}^{n−1}(m)_{(X;F)}(a)))

where

ι = ι_{Φ}^{X,F} : (Φ(X); Φ(F) ∘ ϕ) → Φ((X; F))

is the morphism defined by (3.6) and (3.7).

Proof. We have

D_{Φ}^{n}(m)_{X}((F, a)) =
ΦD_{D_{p′}^{n−1}(F′),X}(D_{p}(D_{Φ}^{n−1}(m))_{X}((F, a))) = ΦD_{D_{p′}^{n−1}(F′),X}((F, D_{Φ}^{n−1}(m)_{(X;F)}(a))) =
(Φ(F) ∘ ϕ; D_{p′}^{n−1}(F′)(ι)(D_{Φ}^{n−1}(m)_{(X;F)}(a)))

where the first equality is by definition of D_{Φ}^{n}(m), the second by (2.24) and the third by (3.8). The lemma is proved.

3.1.7. Lemma. In the context of Problem 3.1.4 consider a commutative square in P reShv(C) of the form

\begin{matrix}F_{1} & ⟶^{m_{1}} & Φ^{∘}(F′_{1}) \\ ^{v}↓ & & ↓^{Φ^{∘}(v′)} \\ F_{2} & ⟶^{m_{2}} & Φ^{∘}(F′_{2}) \end{matrix}  (3.12)

Then, for any n ∈ N, the square

\begin{matrix}D_{p}^{n}(F_{1}) & ⟶^{D_{Φ}^{n}(m_{1})} & Φ^{∘}(D_{p′}^{n}(F′_{1})) \\ ^{D_{p}^{n}(v)}↓ & & ↓^{Φ^{∘}(D_{p′}^{n}(v′))} \\ D_{p}^{n}(F_{2}) & ⟶^{D_{Φ}^{n}(m_{2})} & Φ^{∘}(D_{p′}^{n}(F′_{2})) \end{matrix}  (3.13)

commutes.

Proof. We proceed by induction on n.

For n = 0 the square (3.13) coincides with the square (3.12).

For the successor of n, (3.13) is the external square of the diagram

D_{p}(D_{p}^{n}(F_{1})) ⟶^{D_{p}(D_{Φ}^{n}(m_{1}))} D_{p}(Φ^{∘}(D_{p′}^{n}(F′_{1}))) ⟶^{ΦD_{D{n \atop p′} (F′_{1})}} Φ^{∘}(D_{p′}(D_{p′}^{n}(F′_{1})))
D_{p}(D_{p}^{n}(v))↓  ^{D_{p}(Φ^{∘}(D_{p′}^{n}(v′)))}↓  ↓^{Φ^{∘}(D_{p′}(D_{p′}^{n}(v′)))}
D_{p}(D_{p}^{n}(F_{2})) ⟶^{D_{p}(D_{Φ}^{n}(m_{2}))} D_{p}(Φ^{∘}(D_{p′}^{n}(F′_{2}))) ⟶^{ΦD_{D{n \atop p′} (F′_{2})}} Φ^{∘}(D_{p′}(D_{p′}^{n}(F′_{2})))

The left hand side square in this diagram is obtained by applying D_{p} to the square (3.13) for n. It is commutative because D_{p} is a functor and in particular satisfies the composition axiom (2.26).

The right hand side square is commutative because ΦD is a natural transformation of functors that satisfies the axiom of compatibility with morphisms of presheaves. In our particular case this axiom is applied to the morphism of presheaves D_{p′}^{n}(v′).

This completes the proof of the lemma.

The following problem and construction are the only ones in this section where we change our context from considering a universe category functor to simply a functor between two categories.

3.1.8. Problem. Given a functor Φ : C → C′ between two categories to construct, for each Y ∈ C, a morphism of presheaves

yo^{Φ,Y} : Y o(Y) → Φ^{∘}(Y o(Φ(Y)))

and to show that for a morphism g : Y → Y′ the square

Y o(Y) ⟶^{yo^{Φ,Y}} Φ^{∘}(Y o(Φ(Y)))
Y o(g)↓  ↓^{Φ^{∘}(Y o(Φ(g)))}
Y o(Y′) ⟶^{yo^{Φ,Y′}} Φ^{∘}(Y o(Φ(Y′)))

(3.14)

commutes.

3.1.9. Construction. We need to define, for all X ∈ C, functions

Y o(Y)(X) = Mor_{C}(X, Y) → Mor_{C′}(Φ(X), Φ(Y)) = Φ^{∘}(Y o(Φ(Y)))(X)

which we define as the restriction of Φ_{Mor} to Mor_{C}(X, Y):

yo_{X}^{Φ,Y} (f) = Φ(f)  (3.15)

Let us show that this family is a morphism of presheaves, i.e., that for any a : X′ → X the square

Y o(Y)(X) ⟶^{yo_{X}^{Φ,Y}} Φ^{∘}(Y o(Φ(Y)))(X)
Y o(Y)(a)↓  ↓^{Φ^{∘}(Y o(Φ(Y)))(a)}
Y o(Y)(X′) ⟶^{yo_{X′}^{Φ,Y}} Φ^{∘}(Y o(Φ(Y)))(X′)

(3.16)

commutes. Note that for an element f′ : Φ(X) → Φ(Y) of Φ^{∘}(Y o(Φ(Y)))(X) we have

Φ^{∘}(Y o(Φ(Y)))(a)(f′) = Φ(a) ∘ f′  (3.17)

Let f : X → Y be an element of Y o(Y)(X).

Applying one path in (3.16) to f we get

Φ^{∘}(Y o(Φ(Y)))(a)(yo_{X}^{Φ,Y} (f)) = Φ^{∘}(Y o(Φ(Y)))(a)(Φ(f)) = Φ(a) ∘ Φ(f)

where the first equality is by (3.15) and the second is by (3.17).

Applying another path we get

yo_{X′}^{Φ,Y} (Y o(Y)(a)(f)) = ΦY o(Y)_{X′}(a ∘ f) = Φ(a ∘ f)

where the first equality is by definition of Y o(Y) and the second by (3.15).

We conclude that (3.16) commutes by the composition axiom of Φ.

Let g : Y → Y′ be a morphism. Note that for an element f′ : Φ(X) → Φ(Y) of Φ^{∘}(Y o(Φ(Y)))(X) we have

Φ^{∘}(Y o(Φ(g)))(f′) = f′ ∘ Φ(g)  (3.18)

Let us show that the square (3.14) commutes. Let X ∈ C and f ∈ Y o(Y)(X). Applying one path in (3.14) to f we get

Φ^{∘}(Y o(Φ(g)))(yo^{Φ,Y} (f)) = Φ^{∘}(Y o(Φ(g)))(Φ(f)) = Φ(f) ∘ Φ(g)

where the first equality is by (3.15) and the second by (3.18).

Applying another path we get

yo^{Φ,Y′}(Y o(g)(f)) = yo^{Φ,Y′}(f ∘ g) = Φ(f ∘ g)

where the first equality is by the definition of Y o(g) and the second by (3.15). We conclude that (3.14) commutes by the composition axiom of Φ.

This completes the construction.

Recall that for X, Y ∈ C and n ≥ 0 we have defined in (2.30) the set D_{p}^{n}(X, Y) as follows:

D_{p}^{n}(X, Y) = D_{p}^{n}(Y o(Y))(X)

We also introduced before Remark 2.2.5 the ∘-notation that we will use below.

3.1.10. Problem. With assumptions as above, to define, for all X, Y ∈ C and n ≥ 0, functions

Φ_{X,Y}^{n} : D_{p}^{n}(X, Y) → D_{p′}^{n}(Φ(X), Φ(Y))

3.1.11. Construction. Applying Construction 3.1.5 to the morphism of presheaves yo^{Φ,Y} of Construction 3.1.9 we obtain morphisms of presheaves

D_{Φ}^{n}(yo^{Φ,Y}) : D_{p}^{n}(Y o(Y)) → Φ^{∘}(D_{p′}^{n}(Y o(Φ(Y))))

Evaluating this morphism on X we obtain a function

D_{p}^{n}(X, Y) = D_{p}^{n}(Y o(Y))(X) → Φ^{∘}(D_{p}^{n}(Y o(Φ(Y))))(X) = D_{p′}^{n}(Φ(X), Φ(Y)) (3.19)

For n = 0 we have

D_{p}^{0}(X, Y) = Y o(Y)(X) = Mor_{C}(X, Y)

and

Φ_{X,Y}^{0} = Φ_{X,Y}  (3.20)

that is, the restriction of Φ_{Mor} to the subset Mor_{C}(X, Y) of Mor(C).

The explicit form of the function Φ_{X,Y}^{n} when n ≥ 1 is given by the following lemma. 3.1.12. Lemma. In the context of Problem 3.1.10, let n ≥ 1, X, Y ∈ C and

(F, a) ∈ ⨿_{F:X→U}D_{p}^{n−1}((X; F), Y) = D_{p}(D_{p}^{n−1}(Y o(Y)))(X) = D_{p}^{n}(X, Y) Then one has

Φ_{X,Y}^{n} ((F, a)) = (Φ(F) ∘ ϕ, ι ∘ Φ_{(X;F),Y}^{n−1} (a))

where ι : (Φ(X), Φ(F) ∘ ϕ) → Φ((X; F)) is the morphism defined by (3.6) and (3.7). Proof. By construction we have Φ_{X,Y}^{n} = D_{Φ}^{n}(yo^{Φ,Y})_{X}. By Lemma 3.1.6 we have

D_{Φ}^{n}(yo^{Φ,Y})_{X}((F, a)) = (Φ(F) ∘ ϕ, D_{p′}^{n−1}(Y o(Φ(Y)))(ι)(D_{Φ}^{n−1}(yo^{Φ,Y})_{(X;F)}(a))) Again by construction we have Φ_{(X;F),Y}^{n−1} = D_{Φ}^{n−1}(yo^{Φ,Y})_{(X;F)} and D_{p′}^{n−1}(Y o(Φ(Y)))(ι) = D_{p′}^{n−1}(ι, Y) = ι ∘ −. The lemma is proved. 3.1.13. Lemma. In the context of Construction 3.1.11 one has:

1. let f : X′ → X be a morphism, then the square

D_{p}^{n}(X, Y) ⟶^{Φ_{X,Y}^{n}} D_{p′}^{n}(Φ(X), Φ(Y))
D_{p}^{n}(f,Y)↓  ↓^{D_{p′}^{n}(Φ(f),Φ(Y))}
D_{p}^{n}(X′, Y) ⟶^{Φ_{X′,Y}^{n}} D_{p′}^{n}(Φ(X′), Φ(Y))

(3.21)

commutes,

2. let g : Y → Y′ be a morphism, then the square

D_{p}^{n}(X, Y) ⟶^{Φ_{X,Y}^{n}} D_{p′}^{n}(Φ(X), Φ(Y))
D_{p}^{n}(X,g)↓  ↓^{D_{p′}^{n}(Φ(X),Φ(g))}
D_{p}^{n}(X, Y′) ⟶^{Φ_{X,Y′}^{n}} D_{p′}^{n}(Φ(X), Φ(Y′))

(3.22)

commutes. Proof. Commutativity of (3.21) follows from (3.19) and the fact that D_{Φ}^{n}(yo^{Φ,Y}) is a morphism of presheaves.

Commutativity of (3.22) follows from (3.19), the commutativity of (3.14) and Lemma 3.1.7.

In the ∘-notation the assertion of Lemma 3.1.13 looks as follows. Let d ∈ D_{p}^{n}(X, Y). Then for f : X′ → X one has

Φ(f) ∘ Φ^{n}(d) = Φ^{n}(f ∘ d)  (3.23)

and for g : Y → Y′ one has

Φ^{n}(d) ∘ Φ(g) = Φ^{n}(d ∘ g)  (3.24)

3.2. Universe category functors and isomorphisms u_{n} and ũ_{n}. By [6, Construction 4.7] any universe category functor Φ = (Φ, ϕ, ϕ̃) from (C, p) to (C′, p) defines a homomorphism of C-systems

H : CC(C, p) → CC(C′, p′)

Let ψ_{0} : pt′ → Φ(pt) be the unique morphism. To define H on objects, one uses the fact that

Ob(CC(C, p)) = ⨿_{n≥0}Ob_{n}(C, p)

and defines H(n, A) as (n, H_{n}(A)) where

H_{n} : Ob_{n}(C, p) → Ob_{n}(C′, p′)

To obtain H_{n} one defines by induction on n, pairs (H_{n}, ψ_{n}) where H_{n} is as above and ψ_{n} is a family of isomorphisms

ψ_{n}(A) : int_{n}(H_{n}(A)) → Φ(int_{n}(A))

as follows:

1. for n = 0, H_{0} is the unique function from a one point set to a one point set and ψ_{0}(A) = ψ_{0},

2. for the successor of n one has

H_{n+1}(A, F) = (H_{n}(A), ψ_{n}(A) ∘ Φ(F) ∘ ϕ)  (3.25)

and ψ_{n+1}(A, F) is the unique morphism int(H(A, F)) → Φ(int(A, F)) such that

ψ_{n+1}(A, F) ∘ Φ(Q(F)) ∘ ϕ̃ = Q(ψ_{n}(A) ∘ Φ(F) ∘ ϕ)  (3.26)

and

ψ_{n+1}(A, F) ∘ Φ(p_{F}) = p_{ψ_{n}(A)∘Φ(F)∘ϕ} ∘ ψ_{n}(A)  (3.27)

The function H : Ob(CC(C, p)) → Ob(CC(C′, p′)) is the sum of functions H_{n}. For Γ = (n, A) in Ob(CC(C, p)) we let ψ(Γ) = ψ_{n}(A) so that ψ is the sum of families ψ_{n}:

ψ(Γ) : int(H(Γ)) → Φ(int(Γ))

The action of H on morphisms is given by the condition that for f : Γ′ → Γ, H(f) is a unique morphism of the form H(Γ′) → H(Γ) such that

int(H(f)) = ψ(Γ′) ∘ Φ(int(f)) ∘ ψ(Γ)^{−1}  (3.28)

We will often write H also for the functions H_{n} and ψ for the functions ψ_{n}.

3.2.1. Lemma. The family of morphisms

ψ(Γ) : int(H(Γ)) → Φ(int(Γ))

is a natural isomorphism of functors

ψ : H ∘ int → int ∘ Φ

Proof. By construction, ψ(Γ) is a family of morphisms of the form (H ∘ int)(Γ) → (int ∘ Φ)(Γ). It remains to verify that for f : Γ′ → Γ one has

ψ(Γ) ∘ (int ∘ Φ)(f) = (H ∘ int)(f) ∘ ψ(Γ′)

This equality is equivalent to (3.28).

The following lemma describes the interaction between the isomorphisms u_{1} and ũ_{1} and universe category functors.

3.2.2. Lemma. Let (Φ, ϕ, ϕ̃) be universe category functor. Then:

1. for T ∈ Ob_{1}(Γ) one has

u_{1,H(Γ)}(H(T)) = ψ(Γ) ∘ Φ(u_{1,Γ}(T)) ∘ ϕ

2. for o ∈ Õb_{1}(Γ) one has

ũ_{1,H(Γ)}(H(o)) = ψ(Γ) ∘ Φ(ũ_{1,Γ}(o)) ∘ ϕ̃

Proof. Let Γ = (n, A).

In the case of T ∈ Ob_{1}(Γ), if T = (n + 1, (A, F)) then

u_{1}(H(T)) = u_{1}(n + 1, H(A, F)) = u_{1}(n + 1, (H(A), ψ(Γ) ∘ Φ(F) ∘ ϕ)) = ψ(Γ) ∘ Φ(F) ∘ ϕ

where the last equality is by (2.37).

In the case of o ∈ Õb_{1}(Γ), if ∂(o) = (n + 1, (A, F)) then ∂(H(o)) = (n + 1, H(A, F)). Since o : Γ → ∂(o) we have

H(o) = ψ(Γ) ∘ Φ(int(o)) ∘ ψ(A, F)^{−1}  (3.29)

and

ũ_{1}(H(o)) = H(o) ∘ Q(u_{1}(n + 1, H(A, F))) = H(o) ∘ Q(ψ(A) ∘ Φ(F) ∘ ϕ) =

H(o) ∘ ψ(A, F) ∘ Φ(Q(F)) ∘ ϕ̃ = ψ(Γ) ∘ Φ(int(o)) ∘ ψ(A, F)^{−1} ∘ ψ(A, F) ∘ Φ(Q(F)) ∘ ϕ̃ =

ψ(Γ) ∘ Φ(int(o)) ∘ Φ(Q(F)) ∘ ϕ̃ = ψ(Γ) ∘ Φ(int(o) ∘ Q(F)) ∘ ϕ̃ =
ψ(Γ) ∘ Φ(ũ_{1}(o)) ∘ ϕ̃

where the first equality is by (2.44), the second by (3.25) and (2.37), the third by (3.26), the fourth by (3.29) and the seventh again by (2.44).

We now want to express the assertion of Lemma 3.2.2 in terms of the commutativity of a diagram of natural transformations of presheaves on CC(C, p).

We will use the natural transformation ψ^{∘} that ψ defines on the corresponding functors between the categories of presheaves. Note that for a natural transformation a : Φ_{1} → Φ_{2} of functors of the form C → C′ and a presheaf F′ on C′ we have

Φ_{2}^{∘}(F′)(X) = F′(Φ_{2}(X)) → F′(Φ_{1}(X)) = Φ_{1}^{∘}(F′)(X)

that is, for a : Φ_{1} → Φ_{2} we have a^{∘} : Φ_{2}^{∘} → Φ_{1}^{∘}. In particular, in the case of ψ we have:

ψ^{∘} : Φ^{∘} ∘ int^{∘} = (int ∘ Φ)^{∘} → (H ∘ int)^{∘} = int^{∘} ∘ H^{∘}

3.2.3. Lemma. In the context of Lemma 3.2.2 the following two diagrams of natural transformations of presheaves on CC(C, p) commute:

\begin{aligned}Ob_{1} & ⟶^{u_{1}} & int^{∘}(Y o(U)) \\ ↓ & int^{∘}(yo^{Φ,U}) \\ & & int^{∘}(Φ^{∘}(Y o(Φ(U)))) \\ ↓^{HOb_{1}} & & ↓^{int^{∘}(Φ^{∘}(Y o(ϕ)))} \\ & & int^{∘}(Φ^{∘}(Y o(U′))) \\ ↓ & ψ_{Y o(U′)}^{∘} \\ H^{∘}(Ob_{1}) & ⟶^{H^{∘}(u_{1})} & H^{∘}(int^{∘}(Y o(U′)) \end{aligned}  \begin{aligned}Õb_{1} & \underrightarrow{ũ_{1}} & int^{∘}(Y o(Ũ)) \\ ↓ & int^{∘}(yo^{Φ,Ũ}) \\ & & int^{∘}(Φ^{∘}(Y o(Φ(Ũ)))) \\ ↓_{HÕb_{1}} & & ↓^{int^{∘}(Φ^{∘}(Y o(ϕ̃)))} \\ & & int^{∘}(Φ^{∘}(Y o(Ũ′))) \\ ↓ & ψ_{Y o(Ũ′)}^{∘} \\ H^{∘}(Õb_{1}) & ⟶^{H^{∘}(ũ_{1})} & H^{∘}(int^{∘}(Y o(Ũ′)) \end{aligned}

Proof. Consider the first diagram. For Γ and T ∈ Ob_{1}(Γ) one path in the diagram applied to T gives us

ψ^{∘}(int^{∘}(Φ^{∘}(Y o(ϕ)))(int^{∘}(yo^{Φ,U}(u_{1,Γ}(T))))) = ψ^{∘}(int^{∘}(Φ^{∘}(Y o(ϕ)))(Φ(u_{1,Γ}(T)))) =
ψ^{∘}(Φ(u_{1,Γ}(T)) ∘ ϕ) = ψ(Γ) ∘ Φ(u_{1,Γ}(T)) ∘ ϕ

while the other path gives

H^{∘}(u_{1})(HOb_{1}(T)) = u_{1,H(Γ)}(H(T))

The equality of these two expressions is the statement of Lemma 3.2.2(1).

The case of the second diagram is strictly parallel. The lemma is proved.

Consider now isomorphisms u_{n} and ũ_{n} for general n ≥ 1.

3.2.4. Lemma. Let Φ = (Φ, ϕ, ϕ̃) be a universe category functor and n ≥ 1. Then

1. for T ∈ Ob_{n}(Γ) one has

u_{n,H(Γ)}(H(T)) = ψ(Γ) ∘ (Φ_{int(Γ),U}^{n−1}(u_{n,Γ}(T)) ∘ ϕ)  (3.30)

2. for o ∈ Õb_{n}(Γ) one has

ũ_{n,H(Γ)}(H(o)) = ψ(Γ) ∘ (Φ_{int(Γ),Ũ}^{n−1}(ũ_{n,Γ}(o)) ∘ ϕ̃)  (3.31)

Proof. Let us verify first that the right hand side of (3.30) is defined and belongs to the same set as the left hand side.

By (2.36) and (2.53), we have u_{n,Γ}(T) ∈ D_{p}^{n−1}(int(Γ), U). Therefore,

Φ_{int(Γ),U}^{n−1}(u_{n,Γ}(T)) ∈ D_{p′}^{n−1}(Φ(int(Γ)), Φ(U))

Since ϕ : Φ(U) → U′ and ψ(Γ) : int(H(Γ)) → Φ(int(Γ)) we have

ψ(Γ) ∘ (Φ_{int(Γ),U}^{n−1}(u_{n,Γ}(T)) ∘ ϕ) ∈ D_{p′}^{n−1}(int(H(Γ)), U′)

on the other hand u_{n,H(Γ)}(H(T)) is an element of D_{p′}^{n−1}(int(H(Γ)), U′) as well. Therefore, (3.30) is an equality between two elements of the same set.

To prove (3.30) we proceed by induction on n. For n = 1 this equality is the same as the equality of Lemma 3.2.2(1).

For the successor of n ≥ 1 we reason as follows. Let T′ = ft^{n}(T) ∈ Ob_{1}(Γ) and let us abbreviate u_{i,−} to u_{n}. By (2.57) and since H commutes with ft we have

u_{n+1}(H(T)) = (u_{1}(ft^{n}(H(T))), u_{n}(H(T))) = (u_{1}(H(T′)), u_{n}(H(T)))  (3.32)

By the inductive assumption we have

u_{n}(H(T)) = ψ(T′) ∘ (Φ_{int(T′),U}^{n−1}(u_{n}(T)) ∘ ϕ)  (3.33)

On the other hand, by (2.57), Lemma 3.1.12 and (2.39) we have

Φ_{int(Γ),U}^{n}(u_{n+1}(T)) = Φ_{int(Γ),U}^{n}((u_{1}(T′), u_{n}(T))) =

(Φ(u_{1}(T′)) ∘ ϕ, ι ∘ Φ_{(int(Γ);u_{1}(T′)),U}^{n−1}(u_{n}(T))) = (Φ(u_{1}(T′)) ∘ ϕ, ι ∘ Φ_{int(T′),U}^{n−1}(u_{n}(T)))

where

ι = ι_{Φ}^{int(Γ),u_{1}(T′)} : (Φ(int(Γ)); Φ(u_{1}(T′)) ∘ ϕ) → Φ((int(Γ); u_{1}(T′))) = Φ(int(T′))

is defined by the obvious analogs of (3.6) and (3.7).

By Lemma 2.2.4(2) we have

(Φ(u_{1}(T′)) ∘ ϕ, ι ∘ (Φ_{int(T′),U}^{n−1}(u_{n}(T)))) ∘ ϕ = (Φ(u_{1}(T′)) ∘ ϕ, (ι ∘ Φ_{int(T′),U}^{n−1}(u_{n}(T))) ∘ ϕ)

Next, by Lemma 2.2.4(1) we have

ψ(Γ) ∘ (Φ(u_{1}(T′)) ∘ ϕ, (ι ∘ Φ_{int(T′),U}^{n−1}(u_{n}(T))) ∘ ϕ) =
(ψ(Γ) ∘ Φ(u_{1}(T′)) ∘ ϕ, Q(ψ(Γ), Φ(u_{1}(T′)) ∘ ϕ) ∘ ((ι ∘ Φ_{int(T′),U}^{n−1}(u_{n}(T))) ∘ ϕ))

It remains to compare the last expression with (3.32). Both expressions are pairs. The first components of these pairs are equal by Lemma 3.2.2(1). To show that the second components are equal we need, in view of (3.33), to show that

Q(ψ(Γ), Φ(u_{1}(T′)) ∘ ϕ) ∘ ((ι ∘ Φ_{int(T′),U}^{n−1}(u_{n}(T))) ∘ ϕ) = ψ(T′) ∘ (Φ_{int(T′),U}^{n−1}(u_{n}(T)) ∘ ϕ)

In view of the “associativities” of Lemma 2.2.3 it is sufficient to show that

Q(ψ(Γ), Φ(u_{1}(T′)) ∘ ϕ) ∘ ι = ψ(T′)  (3.34)

where

ι = ι_{Φ}^{int(Γ),u_{1}(T′)} : (Φ(int(Γ)); Φ(u_{1}(T′)) ∘ ϕ) → Φ((int(Γ); u_{1}(T′)))

Let Γ = (m, A) and F = u_{1,Γ}(T′). Then T′ = (m + 1, (A, F)) and ψ(T′) = ψ((A, F)) is the unique morphism that satisfies the equations (3.26) and (3.27). Therefore, to prove (3.34) we need to show that the following equalities hold:

Q(ψ(A), Φ(F) ∘ ϕ) ∘ ι_{Φ}^{int(A),F} ∘ Φ(Q(F)) ∘ ϕ̃ = Q(ψ(A) ∘ Φ(F) ∘ ϕ)  (3.35)

Q(ψ(A), Φ(F) ∘ ϕ) ∘ ι_{Φ}^{int(A),F} ∘ Φ(p_{F}) = p_{ψ(A)∘Φ(F)∘ϕ} ∘ ψ(A)  (3.36)

For (3.35) we have

Q(ψ(A), Φ(F)∘ϕ)∘ι∘Φ(Q(F))∘ϕ̃ = Q(ψ(A), Φ(F)∘ϕ)∘Q(Φ(F)∘ϕ) = Q(ψ(A)∘Φ(F)∘ϕ)

where the first equality is by (3.7) and the second one by (2.19).

For (3.36) we have

Q(ψ(A), Φ(F) ∘ ϕ) ∘ ι ∘ Φ(p_{F}) = Q(ψ(A), Φ(F) ∘ ϕ) ∘ p_{Φ(F)∘ϕ} = p_{ψ(A)∘Φ(F)∘ϕ} ∘ ψ(A)

where the first equality is by (3.6) and the second one by (2.18) and (2.16). A strictly parallel reasoning applies to the proof of (3.31). This completes the proof of Lemma 3.2.4.

From (3.30), using the fact that u_{n} is a bijection, for d ∈ D_{p}^{n−1}(int(Γ), U), we have

H(u_{n}^{−1}(d)) = u_{n}^{−1}(ψ(Γ) ∘ (Φ^{n−1}(d) ∘ ϕ))  (3.37)

and from (3.31), using the fact that ũ_{n} is a bijection, for d ∈ D_{p}^{n−1}(int(Γ), Ũ), we have

H(ũ_{n}^{−1}(d)) = ũ_{n}^{−1}(ψ(Γ) ∘ (Φ^{n−1}(d) ∘ ϕ̃))  (3.38)

3.3. Universe category functors and the I_{p} construction. Let (C, p) and (C′, p′) be locally cartesian closed universe categories with binary product structure as considered in Section 2.6. Let Φ : (C, p) → (C′, p′) be a universe category functor. No assumption is made about the compatibility of Φ with the locally cartesian closed or binary product structures.

In what follows we omit the indexes at η_{n}, η_{n}^{!} and Φ^{n} where no confusion is possible.

3.3.1. Problem. In the context introduced above to construct, for any n ≥ 0 and Y ∈ C, a morphism

χ_{Φ,n}(Y) : Φ(I_{p}^{n}(Y)) → I_{p′}^{n}(Φ(Y))

such that for any g : Y → Y′ the square

Φ(I_{p}^{n}(Y)) ⟶^{χ_{Φ,n}(Y)} I_{p′}^{n}(Φ(Y))
Φ(I_{p}^{n}(g))↓  ↓^{I_{p′}^{n}(Φ(g))}
Φ(I_{p}^{n}(Y′)) ⟶^{χ_{Φ,n}(Y′)} I_{p′}^{n}(Φ(Y′))

(3.39)

commutes.

3.3.2. Construction. We set

χ_{Φ,n}(Y) = η_{n}(Φ^{n}(Id_{Y}^{n}))

where Id_{Y}^{n} is defined in (2.71). In what follows we often omit the index Φ at χ. Let g : Y → Y′. Let us show that the square (3.39) commutes. We have

χ_{n}(Y) ∘ I_{p′}^{n}(Φ(g)) =
η_{n}(Φ^{n}(Id_{Y}^{n})) ∘ I_{p′}^{n}(Φ(g)) = η_{n}(Φ^{n}(Id_{Y}^{n}) ∘ Φ(g)) = η_{n}(Φ^{n}(Id_{Y}^{n} ∘ g)) =
η_{n}(Φ^{n}(η_{n}^{!}(I_{p}^{n}(g))))

where the first equality is by the definition of χ_{n}, the second by (2.68), the third by (3.24), and the fourth by (2.73).

On the other hand we have,

Φ(I_{p}^{n}(g)) ∘ χ_{n}(Y′) =

Φ(I_{p}^{n}(g)) ∘ η_{n}(Φ^{n}(Id_{Y′}^{n})) = η_{n}(Φ(I_{p}^{n}(g)) ∘ Φ^{n}(Id_{Y′}^{n})) = η_{n}(Φ^{n}(I_{p}^{n}(g) ∘ Id_{Y′}^{n})) =

η_{n}(Φ^{n}(η_{n}^{!}(I_{p}^{n}(g))))

where the first equality is by the definition of χ_{n}, the second by (2.67), the third by (3.23), and the fourth by (2.72).

This shows that the square (3.39) commutes and completes the construction.

We have

χ_{0}(Y) = Id_{Φ(Y)}  (3.40)

Indeed,

χ_{0}(Y) = η_{0}(Φ^{0}(Id_{Y}^{n})) = η_{0}(Φ^{0}(η_{0}^{!}(Id_{I_{p}^{0}(Y)}))) = Φ^{0}(Id_{Y}) = Φ(Id_{Y}) = Id_{Φ(Y)}

where the first equality is by the definition of ξ_{n} in Construction 3.3.2, the second by the definition of Id_{Y}^{n} in (2.71), the third by the fact that η_{0} = Id by the definition of η_{n} in Construction 2.6.6, the fourth by (3.20) and the fifth by the identity axiom of the functor Φ.

We will also use the following formula.

3.3.3. Lemma. In the notation introduced above and d ∈ D_{p}^{n}(X, Y) one has

η_{n}(Φ^{n}(d)) = Φ(η_{n}(d)) ∘ χ_{n}(Y)

Proof. We have

Φ(η_{n}(d)) ∘ χ_{n}(Y) =
Φ(η_{n}(d)) ∘ η_{n}(Φ^{n}(Id_{Y}^{n})) = η_{n}(Φ(η_{n}(d)) ∘ Φ^{n}(Id_{Y}^{n})) = η_{n}(Φ^{n}(η_{n}(d) ∘ Id_{Y}^{n})) =
η_{n}(Φ^{n}(d))

where the first equality is by the definition of χ_{n}, the second by (2.67), the third by (3.23), and the fourth by (2.74).

3.4. Universe category functors and the isomorphisms μ_{n} and μ̃_{n}. For a universe category functor (Φ, ϕ, ϕ̃) and n ≥ 0 let us denote by

ξ_{Φ,n} : Φ(I_{p}^{n}(U)) → I_{p′}^{n}(U′)

the composition χ_{Φ,n}(U) ∘ I_{p′}^{n}(ϕ) and by

ξ̃_{Φ,n} : Φ(I_{p}^{n}(Ũ)) → I_{p′}^{n}(Ũ′)

the composition χ_{Φ,n}(Ũ) ∘ I_{p′}^{n}(ϕ̃).

From (3.40) we have

ξ_{0} = ϕ  ξ̃_{0} = ϕ̃  (3.41)

In view of the commutativity of the squares (3.39) and (3.1) and the composition axiom for the functor I_{p′}^{n} the squares

\begin{matrix}Φ(I_{p}^{n}(Ũ)) & \underrightarrow{ξ̃_{Φ,n}} & I_{p′}^{n}(Ũ′) \\ ^{Φ(I_{p}^{n}(∂))}↓ & & ↓^{I_{p′}^{n}(∂)} \\ Φ(I_{p}^{n}(U)) & ⟶^{ξ_{Φ,n}} & I_{p′}^{n}(U′) \end{matrix}  (3.42)

commute.

3.4.1. Lemma. Let (Φ, ϕ, ϕ̃) be a universe category functor, Γ ∈ Ob(CC(C, p)) and n ≥ 1. Then one has:

1. for T ∈ Ob_{n}(Γ)

μ_{n,H(Γ)}(H(T)) = ψ(Γ) ∘ Φ(μ_{n,Γ}(T)) ∘ ξ_{Φ,n−1}  (3.43)

2. for o ∈ Õb_{n}(Γ)

μ̃_{n,H(Γ)}(H(o)) = ψ(Γ) ∘ Φ(μ̃_{n,Γ}(o)) ∘ ξ̃_{Φ,n−1}  (3.44)

Proof. Let us show first that the right hand sides of (3.43) and (3.44) are defined and belong to the same sets as the left hand sides.

Indeed, by (2.76), μ_{n,Γ}(T) is an element of Mor_{C}(int(Γ), I_{p}^{n−1}(U)) and therefore Φ(μ_{n,Γ}(T)) is an element of Mor_{C′}(Φ(int(Γ)), Φ(I_{p}^{n−1}(U))).

The morphism ψ(Γ) is of the form int(H(Γ)) → Φ(int(Γ)) and the morphism ξ_{Φ,n−1} is of the form Φ(I_{p}^{n−1}(U)) → I_{p′}^{n−1}(U′). Therefore, the composition on the right hand side of (3.43) is defined and belongs to the same set Mor_{C′}(int(H(Γ)), I_{p′}^{n−1}(U′)) as μ_{n,H(Γ)}(H(T)).

A parallel reasoning shows that the right hand side of (3.44) is defined and both sides are elements of the set Mor_{C′}(int(H(Γ)), I_{p′}^{n−1}(Ũ′)).

Next, we have

μ_{n,H(Γ)}(H(T)) = int^{∘}(η_{n−1,U′})_{H(Γ)}(u_{n}(H(T))) = η_{n−1,U′,int(H(Γ))}(u_{n}(H(T))) =

η_{n−1,U′,int(H(Γ))}(ψ(Γ) ∘ (Φ^{n−1}(u_{n}(T)) ∘ ϕ)) = ψ(Γ) ∘ η_{n−1,U′,Φ(int(Γ))}(Φ^{n−1}(u_{n}(T)) ∘ ϕ) =

ψ(Γ) ∘ η_{n−1,Φ(U),Φ(int(Γ))}(Φ^{n−1}(u_{n}(T))) ∘ I_{p′}^{n−1}(ϕ)

where the first equality is by the definition of μ_{n} (cf. Construction 2.6.9), the second by the definition of int^{∘}, the third by (3.30), the fourth by (2.67) and the fifth by (2.68).

Next

η_{n−1}(Φ^{n−1}(u_{n}(T))) ∘ I_{p′}^{n−1}(ϕ) =
Φ(η_{n−1}(u_{n}(T))) ∘ χ_{n−1}(U) ∘ I_{p′}^{n−1}(ϕ) = Φ(η_{n−1}(u_{n}(T))) ∘ ξ_{n−1} =
Φ(μ_{n}(T)) ∘ ξ_{n−1}

where the first equality holds by Lemma 3.3.3, the second one by the definition of ξ_{n} and the third one by the definition of μ_{n}. This reasoning proves (3.43).

The proof of (3.44) is strictly parallel to the proof of (3.43).

The lemma is proved.

From (3.43), using the fact that μ_{n} is a bijection, for F ∈ Mor_{C}(int(Γ), I_{p}^{n−1}(U)), we have

H(μ_{n}^{−1}(F)) = μ_{n}^{−1}(ψ(Γ) ∘ Φ(F) ∘ ξ_{n−1})  (3.45)

and from (3.44), using the fact that μ̃_{n} is a bijection, for F ∈ Mor_{C}(int(Γ), I_{p}^{n−1}(Ũ)), we have

H(μ̃_{n}^{−1}(F)) = μ̃_{n}^{−1}(ψ(Γ) ∘ Φ(F) ∘ ξ̃_{n−1})  (3.46)

4. Appendices

The facts discussed and proved in the following appendices are certainly well known. We had to repeat them here because we need to fix notations and because there is a number of facts whose proofs I could not find in the literature.

4.1. Categories with binary products and binary cartesian closed categories. Let C be a category.

4.1.1. Definition. A binary product diagram is a pair of morphisms of the form (pr_{1} : bp → X, pr_{2} : bp → Y) such that for all A ∈ C the function

Mor_{C}(A, bp) → Mor_{C}(A, X) × Mor_{C}(A, Y)  (4.1)

given by a ↦ (a ∘ pr_{1}, a ∘ pr_{2}) is a bijection.

The structure of binary products on C is a family, parametrized by pairs of objects (X, Y) ∈ C × C, of binary product diagrams (pr_{1}(X, Y) : bp(X, Y) → X, pr_{2}(X, Y) : bp(X, Y) → Y).

Unless another notation is given, as for the binary products in the slice categories considered below, the object bp(X, Y) is denoted by X × Y and the structural morphisms from X × Y to X and Y by pr_{1}^{X,Y} and pr_{2}^{X,Y} respectively. We will often abbreviate the notation pr_{i}^{X,Y} to pr_{i}.

The following lemma expresses the well know “uniqueness” property of the binary products. We need its explicit form because in the next lemma we will need to state and prove that the corresponding “canonical” isomorphisms are natural.

4.1.2. Lemma. Let (pr_{1,i} : bp_{i} → X, pr_{2,i} : bp_{i} → Y), where i = 1, 2, be two binary product diagrams. Let ι_{1,2} : bp_{1} → bp_{2} be the morphism such that ι_{1,2} ∘ pr_{1,2} = pr_{1,1} and ι_{1,2} ∘ pr_{2,2} = pr_{2,1} and ι_{2,1} : bp_{2} → bp_{1} be the morphism given by the symmetric condition. Then ι_{1,2} and ι_{2,1} are mutually inverse isomorphisms.

Proof. To show that ι_{1,2}∘ι_{2,1} = Id_{bp_{1}} we need to compare two morphisms whose codomain is a binary product. To do it it is sufficient, because of the injectivity of (4.1), to prove that their compositions with the two projections are equal. This follows by simple rewriting. The same applies to the second composition.

4.1.3. Lemma. Let C be a category. Consider four binary product diagrams (pr_{1,i} : bp_{i} → X, pr_{2,i} : bp_{i} → Y) and (pr′_{1,i} : bp′_{i} → X′, pr′_{2,i} : bp′_{i} → Y′) where i = 1, 2. Let ι = ι_{1,2} : pb_{1} → pb_{2} be as in Lemma 4.1.2 and similarly ι′ : pb′_{1} → pb′_{2}. Let a : X′ → X and b : Y′ → Y.

Let c_{i}(a, b) : pb′_{i} → pb_{i} be the unique morphisms such that c_{i}(a, b) ∘ pr_{1,i} = pr′_{1,i} ∘ a and c_{i}(a, b) ∘ pr_{2,i} = b ∘ pr′_{2,i}. Then the square

pb′_{1} ⟶^{c_{1}(a,b)} pb_{1}
ι′↓  ↓^{ι}
pb′_{2} ⟶^{c_{2}(a,b)} pb_{2}

commutes, i.e., c_{1}(a, b) ∘ ι = ι′ ∘ c_{2}(a, b).

Proof. Since (pr_{1,2}, pr_{2,2}) is a binary product diagram it is sufficient to prove that

c_{1}(a, b) ∘ ι ∘ pr_{1,2} = ι′ ∘ c_{2}(a, b) ∘ pr_{1,2}

and

c_{1}(a, b) ∘ ι ∘ pr_{2,2} = ι′ ∘ c_{2}(a, b) ∘ pr_{2,2}

For the first one we have:

c_{1}(a, b) ∘ ι ∘ pr_{1,2} = c_{1}(a, b) ∘ pr_{1,1} = pr′_{1,1} ∘ a

and

ι′ ∘ c_{2}(a, b) ∘ pr_{1,2} = ι′ ∘ pr′_{1,2} ∘ a = pr′_{1,1} ∘ a

The verification of the second equality is similar.

Given a category with binary products and morphisms a : X → X′, b : Y → Y′ denote by a × b : X × Y → X′ × Y′ the unique morphism such that (a × b) ∘ pr_{1} = pr_{1} ∘ a and (a × b) ∘ pr_{2} = pr_{2} ∘ b.

One has

Id_{X×Y} = Id_{X} × Id_{Y}  (4.2)

and for a, b as above and a′ : X′ → X′′, b′ : X′ → X” one has

(a × b) ∘ (a′ × b′) = (a ∘ a′) × (b ∘ b′)  (4.3)

One proves these two equalities by composing both sides with pr_{1} and pr_{2} and using the uniqueness part of the binary product axiom.

From (4.3) one derives

(a × Id_{Y}) ∘ (a′ × Id_{Y}) = (a ∘ a′) × Id_{Y}  (4.4)

and

(Id_{X} × b) ∘ (Id_{X} × b′) = Id_{X} × (b ∘ b′)  (4.5)

The definition of a binary cartesian closed structure given below differs slightly from the definition of the cartesian closed structure given in [4, IV.6] in that, that we do not require the specification of a final object but only of binary products. The rest of the definition is identical to the one in [4], but written more explicitly in order to introduce the notations that are used in proofs in the main part of the paper.

Since we never use the definition of [4, IV.6] we will often write “cartesian closed” instead of “binary cartesian closed”, though we are not assuming a final object.

4.1.4. Definition. The (binary) cartesian closed structure on a category C is a collection of data of the form:

1. the structure of a category with binary products on C,

2. for all X, Y ∈ C an object \underline{Hom}(X, Y),

3. for all X and b : Y → Y′ a morphism

\underline{Hom}(X, b) : \underline{Hom}(X, Y) → \underline{Hom}(X, Y′)

such that for all Y one has

\underline{Hom}(X, Id_{Y}) = Id_{\underline{Hom}(X,Y)}

and for all b : Y → Y′, b′ : Y′ → Y′′ one has

\underline{Hom}(X, b ∘ b′) = \underline{Hom}(X, b) ∘ \underline{Hom}(X, b′)

4. For all X, Y a morphism

ev_{Y}^{X} : \underline{Hom}(X, Y) × X → Y

such that for all W the function

adj_{Y}^{W,X} : Mor(W, \underline{Hom}(X, Y)) → Mor(W × X, Y)

given by

u ↦ (u × Id_{X}) ∘ ev_{Y}^{X}  (4.6)

is a bijection and such that for all b : Y → Y′ the square

\begin{matrix}\underline{Hom}(X, Y) × X & ⟶^{ev_{Y}^{X}} & Y \\ ^{\underline{Hom}(X,b)×Id_{X}} ↓ & & ↓^{b} \\ \underline{Hom}(X, Y′) × X & ⟶^{ev_{Y′}^{X}} & Y′ \end{matrix}  (4.7)

commutes.

A cartesian closed category is a category together with a cartesian closed structure on it.

By definition the objects \underline{Hom}(X, Y) are functorial only in Y. Their functoriality in X is a consequence of a lemma. For X, X′, Y and a : X → X′ let

\underline{Hom}(a, Y) : \underline{Hom}(X′, Y) → \underline{Hom}(X, Y)

be the unique morphism such that

adj(\underline{Hom}(a, Y)) = (Id_{\underline{Hom}(X′,Y)} × a) ∘ ev_{Y}^{X}  (4.8)

Then one has:

4.1.5. Lemma. The morphisms \underline{Hom}(−, Y) satisfy the equalities

\underline{Hom}(a ∘ a′, Y) = \underline{Hom}(a′, Y) ∘ \underline{Hom}(a, Y)
\underline{Hom}(Id_{X}, Y) = Id_{\underline{Hom}(X,Y)}

making \underline{Hom}(−, Y) into a contravariant functor from C to itself.

In addition, for all b : Y → Y′ the square

\underline{Hom}(X′, Y) ⟶^{\underline{Hom}(X,b)} \underline{Hom}(X′, Y′)
\underline{Hom}(a,Y))↓  ↓^{\underline{Hom}(a,Y′)}
\underline{Hom}(X, Y) ⟶^{\underline{Hom}(X′,b)} \underline{Hom}(X, Y′)

commutes.

Proof. It is a particular case of [4, Theorem 3, p.100]. The commutativity of the square is a part of the ”bifunctor” claim of the theorem.

4.1.6. Lemma. In a cartesian closed category let X, X′, Y be objects and let a : X → X′ be a morphism. Then the square

\underline{Hom}(X′, Y) × X ⟶^{Id_{\underline{Hom}(X′,Y )}×a} \underline{Hom}(X′, Y) × X′
\underline{Hom}(a,Y)×Id_{X} ↓  ↓^{ev_{Y}^{X′}}
\underline{Hom}(X, Y) × X  ⟶^{ev_{Y}^{X}}  Y

commutes.

Proof. Let us show that both paths in the square are adjoints to \underline{Hom}(a, Y). For the path that goes through the upper right corner it follows from the definition of \underline{Hom}(a, Y) as the morphism whose adjoint is (Id × a) ∘ ev. For the path that goes through the lower left corner it follows from the definition of adjoint applied to \underline{Hom}(a, Y). Indeed, the adjoint to this morphism is

adj(\underline{Hom}(a, Y)) = (\underline{Hom}(a, Y) × Id_{X}) ∘ ev_{Y}^{X}

4.1.7. Lemma. Let C be a cartesian closed category. Let X, Y, W ∈ C, then one has:

1. Let b : Y → Y′ be a morphism. Then for any r ∈ Mor(W, \underline{Hom}(X, Y′)) one has

adj(r ∘ \underline{Hom}(X, b)) = adj(r) ∘ b

2. Let a : X → X′ be a morphism. Then for any r ∈ Mor(W, \underline{Hom}(X′, Y)) one has

adj(r ∘ \underline{Hom}(a, Y)) = (Id_{W} × a) ∘ adj(r)

3. Let c : W → W′ be a morphism. Then for any r ∈ Mor(W′, \underline{Hom}(X, Y)) one has

adj(c ∘ r) = (c × Id_{X}) ∘ adj(r)

Proof. The proof of the first case is given by

adj(r ∘ \underline{Hom}(X, b)) = ((r ∘ \underline{Hom}(X, b)) × Id_{X}) ∘ ev_{Y}^{X} =
(r × Id_{X}) ∘ (\underline{Hom}(X, b)) × Id_{X}) ∘ ev_{Y}^{X} =
(r × Id_{X}) ∘ ev_{Y′}^{X} ∘ b = adj(r) ∘ b

where the first equality is by (4.6), second equality by Lemma 4.2.2, the third equality by the commutativity of (4.7) and the fourth equality again by (4.6).

The proof of the second case is given by the following sequence of equalities where we use the notation Hm for \underline{Hom}(a, Y) as well as a number of other abbreviations:

adj(r ∘ Hm) = ((r ∘ Hm) × Id) ∘ ev = (r × Id) ∘ (Hm × Id) ∘ ev = (r × Id) ∘ adj(Hm) =

(r × Id) ∘ (Id × a) ∘ ev = (r × a) ∘ ev = (Id × a) ∘ (r × Id) ∘ ev = (Id × a) ∘ adj(r)

where the first equality is by (4.6), the second by (4.4), the third by (4.6), the fourth by (4.8), the fifth by (4.3), the sixth by (4.3) and the seventh by (4.6).

The proof of the third case is given by

adj(c ∘ r) = ((c ∘ r) × Id_{X}) ∘ ev_{Y}^{X} = (c × Id_{X}) ∘ (r × Id_{X}) ∘ ev_{Y}^{X} =
(c × Id_{X}) ∘ adj(r)

where the first equality is by (4.6), second equality by (4.4) and the third equality by (4.6).

Lemma is proved.

4.2. Slice categories, pullbacks and locally cartesian closed categories. For a category C and Z ∈ C one denotes by C/Z the slice category of C over Z. When one works in set theory one has to choose one of the several possible definitions of C/Z. Indeed, the set of objects of C/Z can be defined as the set of pairs (X, f) where X ∈ C and f : X → Z or as the set of morphisms f ∈ Mor(C) such that codom(f) = Z. There is an obvious bijection between these two sets but they are not equal. We define Ob(C/Z) as the set of pairs (X, f). Even more choices exist in the definition of the set of morphisms of C/Z. One definition is the set of triples (((X, f), (Y, g)), a) where (X, f), (Y, g) ∈ Ob(C/Z) and a : X → Y is such that f = a ∘ g. Another one is the set of pairs (a, g) where a, g ∈ Mor(C) are such that codom(a) = dom(g) and codom(f) = Z. Again, these sets are obviously isomorphic but not equal. Various other choices are possible. We will use the second option. We denote the pair (a, g) by a^{g}.

The mappings (X, f) ↦ X and a^{g} ↦ a define a functor C/Z → C that we denote by π_{Z,#}. We will rarely write the functions (π_{Z,#})_{Ob} and (π_{Z,#})_{Mor} explicitly using them instead as “coercions”. Formally speaking, we will assume that (π_{Z,#})_{Ob} (resp. (π_{Z,#})_{Mor}) is inserted in our notation whenever an object (resp. a morphism) of C/Z is specified where an object (resp. a morphism) of C is required.

We will say that a : X → Y is a morphism over Z if a ∘ g = f. For given (X, f) and (Y, g), the function

a^{g} ↦ a  (4.9)

defines a bijection between morphisms (X, f) → (Y, g) in C/Z and morphisms X → Y over Z in C.

In a category with binary products the morphism Id_{Z} × b satisfies the equality

(Id_{Z} × b) ∘ pr_{1} = pr_{1}

and therefore defines a morphism from (Z ×Y, pr_{1}) to (Z ×Y′, pr_{1}) in C/Z. We will denote this morphism in the slice category by Z × b. Since (4.9) is injective, the equalities (4.2) and (4.3) imply that

Z × Id_{Y} = Id_{(Z×Y,pr_{1})}  (4.10)

and

Z × (b ∘ b′) = (Z × b) ∘ (Z × b′)  (4.11)

that is, that the mappings X ↦ (Z × Y, pr_{1}), b ↦ Z × b define a functor Z × − from C to C/Z.

The same holds for morphisms of the form a : X → X′. We denote the morphism in C/Z corresponding to the morphism a × Id_{Z} by a × Z and the resulting functor C → C/Z by − × Z.

4.2.1. Lemma. Let

\begin{matrix}X & ⟶^{a} & Y \\ _{a′}↓ & & ↓^{g} \\ Y′ & ⟶^{g′} & Z \end{matrix}  (4.12)

be a commutative square of morphisms in C and f = a ∘ g = a′ ∘ g′. Then

\begin{matrix}(X, f) & ⟶^{a^{g}} & (Y, g) \\ (a′)^{g′} & ↓ \\ (Y, g′) \end{matrix}  (4.13)

is a binary product diagram in C/Z if and only if (4.12) is a pullback in C.

Proof. Assume that (4.13) is a binary product diagram. Let W ∈ C and let d : W → Y, d′ : W → Y′ be such that d ∘ g = d′ ∘ g′. Let e = d ∘ g. Then d^{g} : (W, e) → (Y, g) and (d′)^{g′} : (W, e) → (Y′, g′) are morphisms in C/Z and therefore there exists c^{f} : (W, e) → (X, f) such that c^{f} ∘a^{g} = d^{g} and c^{f} ∘(a′)^{g′} = (d′)^{g′} in C/G, that is, c∘a = d and c∘a′ = d′ in C. Let c′ : W → X be another morphism in C such that c′ ∘a = d and c′ ∘a′ = d′. Then e = d ∘ g = c′ ∘ a ∘ g = c′ ∘ f and therefore (c′)^{f} is a morphism (W, e) → (X, f) in C/Z. Next, (c′)^{f} ∘ a^{g} = (c′ ∘ a)^{g} = d^{g} and (c′)^{f} ∘ (a′)^{g′} = (c′ ∘ a′)^{g′} = (d′)^{g′}. Therefore (c′)^{f} = c^{f}, that is, c = c′. This shows that (4.12) is a pullback in C.

Similar reasoning shows that if (4.12) is a pullback in C then (4.13) is a binary product diagram in C/Z.

Lemma 4.2.1, combined with a related statement about commutative squares, implies that a choice of binary product structures on all the slice categories C/Z is “the same as” the choice of pullbacks for all pairs of morphisms with the common codomain in C.

To be precise we have to say that how to construct a bijection between the set of families of binary product structures on the categories C/Z for all Z and the set of pullback structures on C.

We usually denote the distinguished binary product of (X, f) and (Y, g) in C/Z by (X, f) ×_{Z} (Y, g) and the canonical morphism from (X, f) ×_{Z} (Y, g) to Z by f ⋄ g.

For f : X → Z and g : Y → Z, the two commutative triangles formed by pr_{1} : (X, f)×_{Z} (Y, g) → (X, f), f, f ⋄g and pr_{2} : (X, f)×_{Z} (Y, g) → (Y, g), g, f ⋄g are adjacent and define the familiar commutative square of the pullback of f and g.

This defines a function in one direction.

For f : X → Z and g : Y → Z, the diagonal of the pullback square based on f and g is an object over Z and the two projections define morphisms from this object to (X, f) and (Y, g) respectively. The corresponding pair of morphisms in C/Z is a binary product diagram. This defines a morphism in the other direction.

The fact that these morphisms are inverse to each other follows readily from the construction.

Given a binary products structure on C/Z, morphisms f : X → Z, g : Y → Z and morphisms a : X′ → X, b : Y′ → Y we have a morphism a^{f} ×_{Z} b^{g} which is the unique morphism in C/Z of the form

a^{f} ×_{Z} b^{g} : (X′, a ∘ f) ×_{Z} (Y′, b ∘ g) → (X, f) ×_{Z} (Y, g)

such that

(a^{f} ×_{Z} b^{g}) ∘ pr_{1} = pr_{1} ∘ a^{f}  (4.14)

and

(a^{f} ×_{Z} b^{g}) ∘ pr_{2} = pr_{2} ∘ b^{g}  (4.15)

4.2.2. Lemma. In the setting introduced above one has:

1. Id_{(X,f)×_{Z}(Y,g)} = Id_{(X,f)} ×_{Z} Id_{(Y,g)},

2. suppose that we have in addition morphisms a′ : X′′ → X′ and b′ : Y′′ → Y′. Then

((a′)^{a∘f} ×_{Z} (b′)^{b∘g}) ∘ (a^{f} ×_{Z} b^{g}) = (a′ ∘ a)^{f} ×_{Z} (b′ ∘ b)^{g}

Proof. It is a particular case of (4.2) and (4.3).

Following the general case considered in Appendix 4.1 we will write (X, f)×_{Z} b^{g} (resp. a^{f} ×_{Z} (Y, g)) for the morphism in C/X (resp. C/Y) corresponding to Id_{(X,f)} ×_{Z} b^{g} (resp. a^{f} ×_{Z} Id_{(Y,g)}).

In view of Lemma 4.2.2 and (4.14), for any (X, f : X → Z), the functions

(Y, g) ↦ ((X, f) ×_{Z} (Y, g), pr_{1})
(b^{g} : (Y′, g′) → (Y, g)) ↦ (X, f) ×_{Z} b^{g}

form a functor from C/Z to C/X and similarly by Lemma 4.2.2 and (4.15), for any (Y, g : Y → Z) the functions

(X, f) ↦ ((X, f) ×_{Z} (Y, g), pr_{2})
(a^{f} : (X′, f′) → (X, f)) ↦ a^{f} ×_{Z} (Y, g)^{f}

form a functor from C/Z to C/Y.

4.2.3. Definition. A locally cartesian closed structure on a category C is a family of (binary) cartesian closed structures on the categories C/Z for all Z ∈ C.

We usually denote the binary product on C/Z as above.

We usually denote the internal-hom objects in C/Z by \underline{Hom}_{Z}((X, f), (Y, g)) and the canonical morphisms from \underline{Hom}_{Z}((X, f), (Y, g)) to Z by f△g.

The rest of the notations (\underline{Hom}_{Z}((X, f), b^{g}), ev_{(Y,g)}^{(X,f)}, adj_{(Y,g)}^{(W,h),(X,f)}, \underline{Hom}_{Z}(a^{f}, (Y, g))) immediately follow from the ones introduced previously.

A locally cartesian closed category is a category together with a locally cartesian closed structure on it.

The name “locally cartesian closed” follows naturally from this definition and the intuition based on the example of the category of open sets of a topological space or a Grothendieck site. If only the subsets of the open sets of a particular covering are known then one sometimes says that the space is known only locally, but the global structure that arises from gluing of all these subsets together is not known. Hence the “local” structure of a category is given by the structure of its slice categories.

4.2.4. Example. The following example shows that there can be many different structures of a category with pullbacks on a category and also many locally cartesian closed structures.

Let us take as our category the category F whose objects are natural numbers and

Mor(n, m) = F un({0, …, n − 1}, {0, …, m − 1})

Since every isomorphism class contains exactly one object every auto-equivalence of this category is an automorphism. Let Φ be such an automorphism. It is easy to see that it must be identity on the set of objects. Let X = {0, 1}. Consider Φ on End(X). Since Φ must respect identities and compositions, Φ must take Aut(X) to itself and must act on it by identity. If 1 and σ are the two elements of Aut(X) we conclude that Φ(1) = 1 and Φ(σ) = σ.

Let us choose now any structure of a category with pullbacks on F and let us consider two new structures str_{1} and str_{σ} that are obtained by modifying pullbacks as follows. In both structures we set all pullbacks to be as they were except for the pullback of the pair of morphisms (Id_{X}, Id_{X}). For this pair we set the pullbacks to be as follows:

\begin{matrix}X & ⟶^{Id_{X}} & X \\ ^{Id_{X}} ↓ & & ↓^{Id_{X}} \\ X & ⟶^{Id_{X}} & X \end{matrix} for str_{1} and  \begin{matrix}X & ⟶^{σ} & X \\ ^{σ}↓ & & ↓^{Id_{X}} \\ X & ⟶^{Id_{X}} & X \end{matrix} for str_{σ}.  (4.16)

The preceding discussion shows that there is no auto-equivalence which would transform str_{1} into str_{σ}.

The category F also has a locally cartesian closed structure and it can be shown that it can be modified so that its pullback components are str_{1} and str_{σ}. This shows that F has at least two locally cartesian closed structures that are not equivalent modulo the auto-equivalences of F.

The solution to this seeming paradox is that there is a category structure on the set of pullback structures (resp. locally cartesian closed structures) on a category. Any two pullback structures (resp. lcc structures) are isomorphic in this category and in this sense pullbacks on a category are “unique”.

4.2.5. Remark. The following remark is not used anywhere in the paper and we include it only as a comment for those readers who are familiar with the univalent foundations where there is a notion of a category and pre-category. There the types of pullback structures and of locally cartesian closed structures on a category (as opposed to those on a general pre-category) are of h-level 1, i.e., classically speaking are either empty or contain only one element.

In addition any such structure on a pre-category should define a structure of the same kind on the Rezk completion of this pre-category with all the different structures on the pre-category becoming equal on the Rezk completion. In the case of the previous example the Rezk completion of F is the category F Sets of finite sets and in view of the univalence axiom for finite sets the two pullbacks of 4.16 will become equal in F Sets.

5. Acknowledgements

I am grateful to the Department of Computer Science and Engineering of the University of Gothenburg and Chalmers University of Technology for its the hospitality during my work on the first version of the paper.

Work on this paper was supported by NSF grant 1100938.

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.

References

[1] John Cartmell. Generalised algebraic theories and contextual categories. Ph.D.

Thesis, Oxford University, 1978. http://www.cs.ru.nl/~spitters/Cartmell.pdf.

[2] John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32(3):209–243, 1986.

[3] Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Types for proofs and programs, volume 3085 of Lecture Notes in Comput. Sci., pages 210–225. Springer, Berlin, 2004.

[4] S. MacLane. Categories for the working mathematician, volume 5 of Graduate texts in Mathematics. Springer-Verlag, 1971.

[5] Thomas Streicher. Semantics of type theory. Progress in Theoretical Computer Science. Birkhäuser Boston Inc., Boston, MA, 1991. Correctness, completeness and independence results, With a foreword by Martin Wirsing.

[6] Vladimir Voevodsky. A C-system defined by a universe category. Theory Appl. Categ.,

30(37):1181–1215, 2015. http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf.

[7] Vladimir Voevodsky. Products of families of types in the C-systems defined by a universe category. arXiv 1503.07072, pages 1–30, 2015.

[8] Vladimir Voevodsky. Products of families of types and (Π, λ)- structures on C-systems. Theory Appl. Categ., 31(36):1044–1094, 2016.

http://www.tac.mta.ca/tac/volumes/31/36/31-36.pdf.

[9] Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In Conference on Mathematics and its Applications, (Kuwait City, 2014), number 658 in Contemporary Mathematics, pages 127–137, 2016.

[10] Vladimir Voevodsky. The (Π, λ)-structures on the C-systems defined by universe categories. In preparation, 2017.

School of Mathematics, Institute for Advanced Study, Princeton NJ, USA

Email: vladimir@ias.edu
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available from the journal’s server at http://www.tac.mta.ca/tac/. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e is required. Articles in PDF format may be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Utrecht University: i.moerdijk@uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: ross.street@mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Université du Québec à Montréal : tierney.myles4@gmail.com R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca