Theory and Applications of Categories, Vol. 30, No. 37, 2015, pp. 1181–1214.

A C-SYSTEM DEFINED BY A UNIVERSE CATEGORY

VLADIMIR VOEVODSKY

Abstract. This is the third paper in a series started in [9]. In it we construct a C-system CC(C, p) starting from a category C together with a morphism p : Ũ → U, a choice of pull-back squares based on p for all morphisms to U and a choice of a final object of C. Such a quadruple is called a universe category. We then define universe category functors and construct homomorphisms of C-systems CC(C, p) defined by universe category functors.

In the sections before the last section we give, for any C-system CC, three different constructions of pairs ((C, p), H) where (C, p) is a universe category and H : CC → CC(C, p) is an isomorphism.

In the last section we construct for any (set) category C with a choice of a final object and fiber products a C-system and an equivalence between C and the precategory underlying CC.

1. Introduction

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

In [8] we constructed for any pair (R, LM) where R is a monad on Sets and LM a left R-module with values in Sets a C-system CC(R, LM). In the particular case of pairs (R, LM) corresponding to binding signatures (cf. [1], [5], [6, p.228]) the regular sub-quotients of CC(R, LM) are the C-systems corresponding to dependent type theories of Martin-Löf genus.

In this paper we describe another construction that generates C-systems. This time the input data is a quadruple that consists of a category C, a morphism p : Ũ → U in this category, a choice of pull-back squares based on p for all morphisms to U and a choice

1. Work on this paper was supported by NSF grant 1100938 and Clay Mathematical Institute. 2. 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. 3. The views and conclusions contained herein are those of the authors 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 US Government or Carnegie Melon University.

Received by the editors 2015-02-02 and, in revised form, 2015-09-06. Transmitted by Martin Hyland. Published on 2015-09-17. 2010 Mathematics Subject Classification: 03F50, 03B15, 03G25 . Key words and phrases: contextual category, universe category, C-system. \begin{matrix}c \\ ◯ \end{matrix} Vladimir Voevodsky, 2015. Permission to copy for private use granted.

of a final object in C. Such a quadruple is called a universe category. For any universe category we construct a C-system that we denote by CC(C, p).

We then define the notion of a universe category functor and construct homomorphisms of C-systems of the form CC(C, p) corresponding to universe category functors. For universe category functors satisfying certain conditions these homomorphisms are isomorphisms. In particular, any equivalence F : C → C′ together with an isomorphism F (p) ≅ p′ (in the category of morphisms) defines a universe category functor whose associated homomorphism of C-systems is an isomorphism. This implies the C-systems that correspond to two different choices of final objects and pull-backs for the same C and p are connected by a given isomorphism which justifies our simplified notation CC(C, p).

To the best of our knowledge it is the only known construction of a C-system (or, equivalently, a contextual category) from category level data that transforms equivalences into isomorphisms. Because of this fact we find it important to present both the construction of the C-system and the construction of the homomorphisms defined by universe functors in detail.

This construction is also important as the starting point in the construction of the model of the inference rules of Martin-Löf type theory that satisfies the univalence axiom. The underlying C-system of the univalent model is obtained by application of our Construction 2.12 to the universal Kan fibration of well-ordered simplicial sets (in a given Grothendieck universe).

Next we explore the question of how to construct, for a given C-system CC, a universe category (C, p) together with an isomorphism CC → CC(C, p). It is clear from Lemma 4.8 that if this problem has a solution then it has many solutions. We construct three such solutions each having certain advantages and disadvantages.

The set of universe categories in a given Grothendieck universe has a structure of a 2-category suggested by Definition 4.1. It seems likely that our main construction extends to a construction of a functor from this 2-category to the 1-category of C-systems. We leave the investigations of the properties of this 2-category and of this functor for the future.

To avoid the abuse of language inherent in the use of the Theorem-Proof style of presenting mathematics when dealing with constructions we use the 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 statement when using both the statement and the proof. 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 often have to refer to the construction and not to the problem and we assign in this paper numbers both to Problems and to the Constructions.

Following the approach used in [9] we write the composition of morphisms in categories in the diagrammatic order, i.e., for f : X → Y and g : Y → Z their composition is written as f ∘g. This makes it much easier to translate between diagrams and equations involving morphisms.

The methods of this paper are fully constructive and the style we write in is the “formalization ready” style where the proofs are spelled out in detail even when the assertion may appear obvious to the practitioners of a particular tradition in mathematics. This particular paper is written having in mind the possibility of formalization both in the Zermelo-Fraenkel set theory (without the axiom of choice) and its constructive versions and in any type theory including Church’s type theory or HOL.

Following the distinction that becomes essential in the univalent formalization (cf. [2]) we use the word “category” in the contexts where the corresponding object is used in a way that is functorial for equivalences of categories and the word “precategory” otherwise.

The main construction of this paper was introduced in [7]. I am grateful to the Centre for Quantum Mathematics and Computation (QMAC) and the Mathematical Institute of the University of Oxford for their hospitality during my work on the previous version of the paper and 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 present version.

2. Construction of CC(C, p).

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 pull-back square

(X; f) ⟶^{Q(f)} Ũ
p_{X,f} ↓  ↓^{p}
X ⟶^{f} U

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

In what follows we will write (X; f_{1}, …, f_{n}) for (… ((X; f_{1}); f_{2}) …; f_{n}).

2.2. Example. Let G be a group. Consider the category BG with one object pt whose monoid of endomorphisms is G. Recall that any commutative square where all four arrows are isomorphisms is a pull-back square. Let p : pt → pt be the unit element of G. Then a universe structure on p can be defined by specifying, for every g : pt → pt, of the horizontal morphism Q(g) in the corresponding canonical square. There are no restrictions on the choice of Q(g) since for any such choice one can take the vertical morphism to be Q(g)g^{−1} obtaining a pull-back square. Therefore, the set of universe structures on p is G^{G}. The automorphisms of BG are given by Aut(G) (with two automorphisms being isomorphic as functors if they differ by an inner automorphisms of G). Therefore, there are (G^{G})/Aut(G) isomorphism classes of categories with universes with the underlying category BG and the underlying universe morphism being Id : pt → pt. Note that in this case all auto-equivalences of the category are automorphisms and so simply saying that we will consider universes up to an equivalence of the underlying category does not change the answer. To have, as is suggested by category-theoretic intuition, no more than one universe structure on a morphism one needs to consider categories with universes up to equivalences of categories with universes and then one has the obligation to prove that the constructions that are supposed to produce objects such as C-systems map equivalences of categories with universes to isomorphisms. In the case of the main construction of this paper it is achieved in Lemma 4.8.

Suppose that we are given a morphism F : X → U. Then for f : W → X and g : W → Ũ such that f ∘ F = g ∘ p we will denote by f ∗ g the unique morphism W → (X; F) such that

(f ∗ g) ∘ p_{X,F} = f
(f ∗ g) ∘ Q(F) = g

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

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

such that in particular

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

2.3. Lemma. The square

\begin{matrix}(X′; f ∘ F) & ⟶^{Q(f,F)} & (X; F) \\ ^{p_{X′,f∘F}} ↓ & & ↓^{p_{X,F}} \\ X′ & ⟶^{f} & X \end{matrix}  (2)

is a pull-back square.

Proof. Consider the diagram

(X′; f ∘ F) ⟶^{Q(f,F)} (X; F) ⟶^{Q(F)} Ũ
p_{X′,f∘F} ↓  ↓^{p_{X,F}}  ↓^{p}
X′  ⟶^{f} X ⟶^{F} U

The composition of two squares of this diagram equals the square with the sides p_{X′,f∘F}, f ∘ F, Q(f ∘ F) and p, which is a pull-back square. The right hand side square in this diagram is a pull-back square. This implies that the left hand side square is a pull-back square.

2.4. Lemma. If f : X′ → X is an isomorphism then Q(f, F) is an isomorphism.

Proof. It follows from Lemma 2.3 by general properties of pull-back squares.

2.5. Lemma. For f′ : X′′ → X′, f : X′ → X and F : X → U one has

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

Proof. Both sides of the equality are morphisms to (X; F), therefore it is sufficient to verify that

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

and

Q(f′, f ∘ F) ∘ Q(f, F) ∘ p_{X,F} = Q(f′ ∘ f, F) ∘ p_{X,F}

For the first one we have

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

and

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

and for the second one we have

Q(f′, f ∘ F) ∘ Q(f, F) ∘ p_{X,F} = Q(f′, f ∘ F) ∘ p_{X′,f∘F} ∘ f = p_{X′′,f′∘f∘F} ∘ f′ ∘ f

and

Q(f′ ∘ f, F) ∘ p_{X,F} = p_{X′′,f′∘f∘F} ∘ f′ ∘ f.

2.6. Definition. A universe category is a triple (C, p, pt) where C is a category, p : Ũ → U is a morphism in C with a universe structure on it and pt is a final object in C.

We will often denote a universe category by a pair (C, p).

Let (C, p) be a universe category. Define by induction on n pairs (Ob_{n}(C, p), int_{n}) where Ob_{n} = Ob_{n}(C, p) are sets and int_{n} : Ob_{n} → Ob(C) are functions, as follows:

1. Ob_{0} = unit where unit is the distinguished set with only one point tt and int_{0} maps this point to pt.

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

In what follows we will write int instead of int_{n} since n can usually be inferred.

Define for each n the function ft_{n+1} : Ob_{n+1} → Ob_{n} by the formula ft_{n+1}(A, F) = A and define ft_{0} as the identity function of Ob_{0}.

For each B = (ft(B), F) ∈ Ob_{n+1} define p_{B} : int(B) → int(ft(B)) as p_{int(ft(B)),F}. For B ∈ Ob_{0} define p_{B} as Id_{int(B)}.

For each A ∈ Ob_{m}, B = (ft(B), F) ∈ Ob_{n+1} and f : int(A) → int(ft(B)) define f^{∗}(B) ∈ Ob_{m+1} as

f^{∗}(B) = (A, f ∘ F)  (3)

and q(f, B) : int(f^{∗}(B)) → int(B) as

q(f, B) = Q(f, F)  (4)

Recall the concept of a C0-system defined in [9, Definition 2.1].

2.7. Problem. For each universe category (C, p, pt) to define a C0-system CC0(C, p).

2.8. Construction. We set

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

where Ob_{n} = Ob_{n}(C, p) are the sets introduced above. Let

int_{Ob} : Ob(CC0(C, p)) → C

be the sum of the functions int_{n}. Let

Mor(CC0(C, p)) = ⨿_{Γ,Γ′∈Ob(CC0(C,p))}Hom_{C}(int_{Ob}(Γ), int_{Ob}(Γ′))

Define the function

int_{Mor} : Mor(CC0(C, p)) → Mor(C)

by the formula

int_{Mor}(Γ, (Γ′, a)) = a

We will often write simply int for int_{Ob} and int_{Mor}.

The identity morphisms and the composition of morphisms are defined as in C. The proofs of the axioms of a category are straightforward.

The definition of the length function is obvious.

We define pt as the unique element (0, tt) of Ob(CC0(C, p)) of length zero.

The function ft : Ob(CC0) → Ob(CC0) is defined as the sum of functions ft_{n} defined above.

The p-morphisms p_{(n,A)} are defined such that int(p_{(n,A)}) = p_{A} where p_{A} where defined above.

Similarly one defines the morphisms q(f, (n + 1, B)) such that int(q(f, (n + 1, B))) = q(f, B).

Lemma 2.5 shows that the structure that we have defined satisfies the axioms of a C0-system given in [9, Definition 2.1].

Let us also note the following formulas. For Δ = (n + 1, (B, F)) and Γ = (n, B) one has

p_{Δ} = (Δ, (Γ, p_{int(B),F}))  (5)

For Γ′ = (m, A), Γ = (n, B) and f : Γ′ → Γ one has

f^{∗}(n + 1, (B, F)) = (m + 1, (A, int(f) ∘ F))  (6)

q(f, (n + 1, (B, F))) = (f^{∗}(Δ), (Δ, Q(int(f), F)))  (7)

2.9. Lemma. The functions int_{Ob} and int_{Mor} defined above form a fully faithful functor from the category underlying the C0-system CC0(C, p) to C.

Proof. Easy from the construction.

2.10. remark. The image of int on objects consists of those objects for which the unique morphism to pt can be represented as a composition of morphisms of the form p_{X,F}. Note that int need not be an injection on the sets of objects. For example, if C is the one point category with its unique structure of a universe category then Ob(CC(C, p)) will be isomorphic to the set of natural numbers.

2.11. Problem. For each universe category (C, p, pt) to define a C-system CC(C, p).

2.12. Construction. We will define CC(C, p) as an extension of CC0(C, p) using [9, Proposition 2.4]. In particular Ob(CC) = Ob(CC0), Mor(CC) = Mor(CC0) and similarly for the length function, ft, p-morphisms and q-morphisms.

The canonical squares of CC0(C, p) are of the form

\begin{matrix}f^{∗}(Γ) & ⟶^{q(f,Γ)} & Γ \\ ^{p_{f^{∗}(Γ)}}↓ & & ↓^{p_{Γ}} \\ Γ′ & ⟶^{f} & ft(Γ) \end{matrix}  (8)

For Γ = (n + 1, (B, F)) where B ∈ Ob_{n}(C, p) and F : int(A) → U, Γ′ = (m, A) where A ∈ Ob_{m}(C, p), and f = (Γ′, (Γ, a)) the image of this square under the functor int is of the form

(int(A); a ∘ F) ⟶^{Q(a,F)} (int(B); F)
p_{int(A),a∘F} ↓  ^{p_{int(B),F}} ↓
int(A)  ⟶^{F} int(B)

This is one of the squares of the form (2) and therefore by Lemma 2.3 it is a pull-back square. Since int is fully faithful by Lemma 2.9, the squares (8) are pull-back squares in the codomain of a fully faithful functor and therefore they are also pull-back squares in the domain of this functor, i.e., in CC0(C, p). In view of [9, Proposition 2.4] this implies that the C0-system CC0(C, p) has a unique structure of a C-system and we denote this C-system by CC(C, p).

2.13. remark. Recall that in [9] we suggested the notation Ob_{n}(CC) for the set of objects of length n of a C-system CC. We will avoid using this notation here because the sets Ob_{n}(C, p) are not equal to the subsets of elements of length n in CC(C, p). Indeed, the elements of {Γ ∈ Ob(CC(C, p)) | l(Γ) = n} are not the elements of Ob_{n}(C, p) but pairs of the form (n, A) where A ∈ Ob_{n}(C, p).

2.14. Example. An important example of a C-system of the form CC(C, p) is “the” C-system F am of families of sets considered in [3] and [4]. The definition of F am in [4, p.238] as well as the preceding it discussion in [4, p.232] is somewhat incomplete in that the notion of “a set” and moreover the notion of “a family of sets” are taken as being uniquely determined by some previous agreement that is never explicitly referred to.

To define F am as a C-system of the form CC(C, p) let us choose two Grothendieck universes U and U_{1} in our set theory such that U_{1} is an element of U. One then defines the category Sets(U) of sets as the category whose set of objects is U and such that for X, Y ∈ U the set of morphisms from X to Y in Sets(U) is the set of functions from X to Y in the ambient set theory (which automatically is an element of U). This category will contain U_{1} as an object and also, because of the closure conditions that U satisfies, it will contain as an object the set Ũ_{1} of pairs (X, x) where X ∈ U_{1} and x ∈ X. Since morphisms in Sets are the same as functions in the ambient set theory we also get p_{U_{1}} : Ũ_{1} → U_{1} that takes (X, x) to X. Using the standard construction of pull-backs in sets we obtain a universe structure on p. Now we can define:

F am(U, U_{1}) := CC(Sets(U), p_{U_{1}})

The explicit definition given in [4] avoids the use of the second universe (universe U in our notations) by constructing the same C-system “by hand”. In our approach we have to use U but the resulting C-system does not depend on U. Indeed, if our set theory assumes two Grothendieck universes U and U′ such that both contain U_{1} as an element then one can show that

CC(Sets(U), p_{U_{1}}) = CC(Sets(U′), p_{U_{1}})  (9)

where the equality means in particular that the sets of objects of these two C-systems are equal as sets. Because of this one can denote this C-system as F am(U_{1}).

3. On homomorphisms of C-systems

We will need below the concept of a homomorphism of C-systems. Homomorphisms of C-systems were defined in [9, Remark 2.8]. Let us recall it here in a more detailed form.

3.1. Definition. Let CC_{1}, CC_{2} be C-systems. A homomorphism F from CC_{1} to CC_{2} is a pair of functions F_{Ob} : Ob(CC_{1}) → Ob(CC_{2}), F_{Mor} : Mor(CC_{1}) → Mor(CC_{2}) such that:

1. F commutes with the length functions, i.e., for all X ∈ Ob(CC_{1}) one has

l(F_{Ob}(X)) = l(X)

2. F commutes with the ft function, i.e., for all X ∈ Ob(CC_{1}) one has

ft(F_{Ob}(X)) = F_{Ob}(ft(X))

3. F is a functor, i.e., one has:

(a) F_{Mor} and F_{Ob} commute with the domain and codomain functions,

(b) for all X ∈ Ob(CC_{1}) one has

F_{Mor}(Id_{X}) = Id_{F_{Mor}(X)}

(c) for all f, g ∈ Mor(CC_{1}) of the form f : X → Y, g : Y → Z one has

F_{Mor}(f ∘ g) = F_{Mor}(f) ∘ F_{Mor}(g)

4. F takes canonical projections to canonical projections, i.e., for all X ∈ Ob(CC_{1})

one has

p_{F_{Ob}(X)} = F_{Mor}(p_{X})

5. F takes q-morphisms to q-morphisms, i.e., for all X, Y ∈ Ob(CC_{1}) such that l(Y) > 0 and all f : X → ft(Y) one has

F_{Mor}(q(f, Y)) = q(F_{Mor}(f), F_{Ob}(Y))

6. F takes s-morphisms to s-morphisms, i.e., for all X, Y ∈ Ob(CC_{1}) such that l(Y) >

0 and f : X → Y one has

s_{F_{Mor}(f)} = F_{Mor}(s_{f})

In what follows we will write F for both F_{Ob} and F_{Mor} since the choice of which one is meant is determined by the type of the argument. Note that the condition that F commutes with the domain function together with the q-morphism condition implies that for all X, Y ∈ Ob(CC_{1}) such that l(Y) > 0 and all f : X → ft(Y) one has

F (f^{∗}(Y)) = F (f)^{∗}(F (Y))  (10)

3.2. Lemma. Let F : CC_{1} → CC_{2} and G : CC_{2} → CC_{3} be homomorphisms of C-systems. Then the compositions of functions F_{Ob} ∘ G_{Ob} and F_{Mor} ∘ G_{Mor} is a homomorphism of C-systems.

Proof. The proof is relatively straightforward but long and we leave it for the formal version(s) of the paper.

3.3. remark. Since homomorphisms of C-systems are pairs of functions between sets satisfying certain conditions and the composition is given by composition of these functions, the associativity and unitality of this composition follows easily from the associativity and unitality of the composition of functions between sets. Therefore, if we restrict our attention to the C-systems whose sets Ob and Mor are elements of a chosen set (“universe”) U that contains natural numbers and is closed under the power-set operation, then such C-systems, their homomorphisms, compositions of these homomorphisms and the identity homomorphisms form a category of C-systems in U.

3.4. Lemma. Let CC_{1}, CC_{2}, F_{ob} and F_{Mor} be as above. Assume further that these data satisfy all of the conditions of the definition except, possibly, the s-morphisms condition. Then (F_{Ob}, F_{Mor}) satisfies the s-morphisms condition and forms a homomorphism of Csystems.

Proof. Let f : X → Y be as in the s-morphism condition. We need to show that F (s_{f}) = s_{F (f)}. Observe first that the right hand side is well defined since l(F (Y)) = l(Y) > 0. We have F (s_{f}) : F (X) → F ((f ∘ p_{Y})^{∗}(Y)) and s_{F (f)} : F (X) → (F (f) ∘ p_{F (Y)})^{∗}(F (Y)). One proves that codomains of both morphisms are equal using that F is a functor, the p-morphisms condition and (10).

Since the canonical squares of CC_{2} are pull-back squares the object

(F (f) ∘ p_{F (Y)})^{∗}(F (Y))

is a fiber product with the projections q(F (f) ∘ p_{F (Y)}, F (Y)) and p_{F (f)^{∗}(F (Y)}. Therefore it is sufficient to check that one has

F (s_{f}) ∘ q(F (f) ∘ p_{F (Y)}, F (Y)) = s_{F (f)} ∘ q(F (f) ∘ p_{F (Y)}, F (Y))  (11)

and

F (s_{f}) ∘ p_{F (f)^{∗}(F (Y)} = s_{F (f)} ∘ p_{F (f)^{∗}(F (Y)}  (12)

We have

F (s_{f}) ∘ q(F (f) ∘ p_{F (Y)}, F (Y)) = F (s_{f}) ∘ q(F (f) ∘ F (p_{Y}), F (Y)) =

F (s_{f}) ∘ q(F (f ∘ p_{Y}), F (Y)) = F (s_{f}) ∘ F (q(f ∘ p_{Y} , Y)) = F (s_{f} ∘ q(f ∘ p_{Y} , Y)) = F (f)

where the first equality holds by condition (4) of Definition 3.1, the second and the fourth equalities by condition (3), the third equality by condition (5) and the fifth equality by axiom [9, Definition 2.3(3)] of the operation s for CC_{1}.

On the other hand

s_{F (f)} ∘ q(F (f) ∘ p_{F (Y)}, F (Y)) = F (f)

directly by the axiom [9, Definition 2.3(3)] of the operation s for CC_{2}. This proves (11). For the equation (12) we have

F (s_{f}) ∘ p_{F (f)^{∗}(F (Y)} = F (s_{f}) ∘ p_{F (f^{∗}(Y))} = F (s_{f}) ∘ F (p_{f^{∗}(Y)}) = F (s_{f} ∘ p_{f^{∗}(Y)}) =

F (Id_{X}) = Id_{F (X)}

where the first equation holds by (10), the second one by condition (4), the third one by condition (3), the fourth one by the axiom [9, Definition 2.3(2)] of the operation s for CC_{1} and the fifth one by condition (3).

On the other hand

s_{F (f)} ∘ p_{F (f)^{∗}(F (Y)} = Id_{F (X)}

directly by the axiom [9, Definition 2.3(2)] of the operation s for CC_{2}. This completes the proof of Lemma 3.4.

3.5. remark. As defined in [9], a C-system without operation s is called a C0-system. The pairs F_{Ob}, F_{Mor} that satisfy all of the conditions of Definition 3.1 other than, possibly, the s-morphism condition are homomorphisms of C0-systems. Therefore, if one defines a categories of C-systems and C0-systems based on a particular universe of sets as outlined in Remark 3.3 then Lemma 3.4 implies that the forgetting functor from the category of C-systems in U to C0-systems in U is a full embedding.

4. Functoriality of CC(C, p)

4.1. Definition. Let (C, p, pt) and (C′, p′, pt′) be universe categories. A functor of universe categories from (C, p, pt) to (C′, p′, pt′) is a triple (Φ, ϕ, ϕ̃) where Φ : C → C′ is a functor and ϕ : Φ(U) → U′, ϕ̃: Φ(Ũ) → Ũ′ are morphisms such that:

1. Φ takes the canonical pull-back squares based on p to pull-back squares,

2. Φ takes pt to a final object of C′,

3. the square

Φ(Ũ) \underrightarrow{ϕ̃} Ũ′
Φ(p)↓  ↓^{p′}
Φ(U) ⟶^{ϕ} U′

is a pull-back square.

Let

(Φ, ϕ, ϕ̃) : (C, p, pt) → (C′, p′, pt′)

be a functor of universes categories. Let Ob_{n} = Ob_{n}(C, p) and Ob′_{n} = Ob_{n}(C′, p′). Let int and int′ be the corresponding functions to C and C′.

Denote by ψ the isomorphism ψ : pt′ → Φ(pt). Define, by induction on n, pairs (H_{n}, ψ_{n}) where H_{n} : Ob_{n} → Ob′_{n} and ψ_{n} is a family of isomorphisms of the form

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

given for all A ∈ Ob_{n}. We set:

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

2. for the successor of n we set

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

and define

ψ_{n+1}(A, F) : (int(H_{n}(A)); ψ_{n}(A) ∘ Φ(F) ∘ ϕ) → Φ(int(A, F))

as the unique morphism such that the left hand side square of the diagram

int′(H_{n+1}(A, F)) ⟶^{ψ_{n+1}(A,F)} Φ(int(A, F)) ⟶^{Φ(Q(F))} Φ(Ũ) \underrightarrow{ϕ̃} Ũ′
p_{H_{n+1}(A,F)}↓  ↓^{Φ(p_{(A,F)})}  ↓^{Φ(p)}  ↓^{p′}
int′(H_{n}(A))  ⟶^{ψ_{n}(A)} Φ(int(A)) ⟶^{Φ(F)} Φ(U) ⟶^{ϕ} U′

(14)

commutes, i.e.,

ψ(A, F) ∘ Φ(p_{(A,F)}) = p_{H(A,F)} ∘ ψ(A)  (15)

and

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

Note that the existence and uniqueness of ψ_{n+1}(A, F) follows from the fact that the right hand side squares of (14) are pull-back squares as a corollary of the definition of a universe category functor and the fact that the canonical square for the morphism ψ_{n}(A)∘Φ(F)∘ϕ commutes.

Moreover since the outer square of (14) is a pull-back square, the left-most square commutes and the two right hand side squares are pull-back squares we conclude that the left hand side square is a pull-back square. In combination with the inductive assumption that ψ_{n}(A) is an isomorphism this implies that ψ_{n+1}(A, F) is an isomorphism.

In what follows we will write ψ(A) instead of ψ_{n}(A) since n can often be inferred.

4.2. Lemma. The functions H commute with the functions ft, i.e., for A ∈ Ob_{n} one has

ft(H(A)) = H(ft(A))

Proof. Immediate from the construction.

A C-SYSTEM DEFINED BY A UNIVERSE CATEGORY  1193

Let A ∈ Ob_{m}, A′ ∈ Ob_{m′} and a : int(A) → int(A′). Define a morphism

H(a) : int′(H(A)) → int′(H(A′))

as

H(a) = ψ(A) ∘ Φ(a) ∘ ψ(A′)^{−1}  (17)

4.3. Lemma. For Φ as above one has:

1. for A ∈ Ob_{n} one has H(Id_{int(A)}) = Id_{int(H(A))},

2. for a′ : int(A′′) → int(A′) and a : int(A′) → int(A) one has H(a′∘a) = H(a′)∘H(a). Proof. Immediate from the construction. 4.4. Lemma. For A ∈ Ob_{n} one has H(p_{A}) = p_{H(A)}. Proof. If n = 0 the statement is obvious. For (A, F) ∈ Ob_{n+1} we have

H(p_{(A,F)}) = ψ(A, F) ∘ Φ(p_{(A,F)}) ∘ ψ(A)^{−1}

Therefore we need to show that

ψ(A, F) ∘ Φ(p_{(A,F)}) = p_{H(A,F)} ∘ ψ(A)

which is (15). 4.5. Lemma. Let A ∈ Ob_{m}, B = (ft(B), F) ∈ Ob_{n+1} and a : int(A) → int(ft(B)) is a morphism. Then one has

H(a^{∗}(B)) = H(a)^{∗}(H(B))  (18)

and

H(q(a, B)) = q(H(a), H(B))  (19)

Proof. We have

H(a^{∗}(ft(B), F)) = H(A, a ∘ F) = (H(A), ψ(A) ∘ Φ(a ∘ F) ∘ ϕ)

and

H(a)^{∗}(H(ft(B), F)) = H(a)^{∗}(H(ft(B)), ψ(ft(B)) ∘ Φ(F) ∘ ϕ) =
(H(A), H(a) ∘ ψ(ft(B)) ∘ Φ(F) ∘ ϕ)

Therefore we need to check that ψ(A) ∘ Φ(a) = H(a) ∘ ψ(ft(B)) which follows from the definition of H(a).

To prove (19) it is sufficient, since ψ(B) is an isomorphism, to show that

H(q(a, B)) ∘ ψ(B) = q(H(a), H(B)) ∘ ψ(B)

In view of (18) both sides are morphisms from int(H(a^{∗}(B))) to

Φ(int(B)) = Φ((int(ft(B)); F))

Since the two right squares of (14) for (ft(B), F) are pull-back squares, Φ((int(ft(B)); F)) is a fiber product with projections Φ(Q(F)) ∘ ϕ̃ and Φ(p_{B}). Therefore it is sufficient to check two equalities

H(q(a, B)) ∘ ψ(B) ∘ Φ(Q(F)) ∘ ϕ̃ = q(H(a), H(B)) ∘ ψ(B) ∘ Φ(Q(F)) ∘ ϕ̃  (20)

and

H(q(a, B)) ∘ ψ(B) ∘ Φ(p_{B}) = q(H(a), H(B)) ∘ ψ(B) ∘ Φ(p_{B})  (21)

Note first that

H(q(a, B)) ∘ ψ(B) = ψ(a^{∗}(B)) ∘ Φ(q(a, (ft(B), F))) = ψ(A, a ∘ F) ∘ Φ(Q(a, F)) (22)

where the first equality is by (17) and the second by (4), and

q(H(a), H(B)) ∘ ψ(B) = q(H(a), (H(ft(B)), ψ(ft(B)) ∘ Φ(F) ∘ ϕ)) ∘ ψ(B) =
Q(H(a), ψ(ft(B)) ∘ Φ(F) ∘ ϕ) ∘ ψ(ft(B), F)  (23)

where the first equality is by (13) and the second equality is by (4). For (20) we have

H(q(a, B)) ∘ ψ(B) ∘ Φ(Q(F)) ∘ ϕ̃ = ψ(A, a ∘ F) ∘ Φ(Q(a, F)) ∘ Φ(Q(F)) ∘ ϕ̃ =

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

where the first equality is by (22), the second equality is by (1) and the third one by (16), and

q(H(a), H(B)) ∘ ψ(B) ∘ Φ(Q(F)) ∘ ϕ̃ =
Q(H(a), ψ(ft(B)) ∘ Φ(F) ∘ ϕ) ∘ ψ(ft(B), F) ∘ Φ(Q(F)) ∘ ϕ̃ =
Q(H(a), ψ(ft(B)) ∘ Φ(F) ∘ ϕ) ∘ Q(ψ(ft(B)) ∘ Φ(F) ∘ ϕ) =
Q(H(a) ∘ ψ(ft(B)) ∘ Φ(F) ∘ ϕ) =
Q(ψ(A) ∘ Φ(a) ∘ ψ(ft(B))^{−1} ∘ ψ(ft(B)) ∘ Φ(F) ∘ ϕ) = Q(ψ(A) ∘ Φ(a ∘ F) ∘ ϕ)

where the first equality is by (23), the second equality is by (16), the third one by (1), and the fourth one by (17). For (20) we have:

H(q(a, B))∘ψ(B)∘Φ(p_{B}) = ψ(A, a∘F)∘Φ(Q(a, F))∘Φ(p_{B}) = ψ(a^{∗}(B))∘Φ(Q(a, F)∘p_{B}) =

ψ(a^{∗}(B)) ∘ Φ(q(a, B) ∘ p_{B}) = ψ(a^{∗}(B)) ∘ Φ(p_{a^{∗}(B)}) ∘ Φ(a)

where the first equality is by (22), the second by (3) and the assumption that Φ is a functor, the third one by (4) and the fourth one by the commutativity of the canonical squares and the assumption that Φ is a functor.

For the other side we have:

q(H(a), H(B)) ∘ ψ(B) ∘ Φ(p_{B}) = q(H(a), H(B)) ∘ p_{H(B)} ∘ ψ(ft(B)) =

p_{H(a^{∗}(B))} ∘ H(a) ∘ ψ(ft(B)) = p_{H(a^{∗}(B))} ∘ ψ(A) ∘ Φ(a) = ψ(a^{∗}(B)) ∘ Φ(p_{a^{∗}(B)}) ∘ Φ(a)

Where the first equality is by (15), the second by the commutativity of the canonical squares, the third by (17) and the fourth again by (15). This completes the proof of Lemma 4.5.

4.6. Problem. Let

(Φ, ϕ, ϕ̃) : (C, p, pt) → (C′, p′, pt′)

be a functor of universes categories. To define a homomorphism H = H(Φ, ϕ, ϕ̃) from CC(C, p) to CC(C′, p′).

4.7. Construction. We define H_{Ob} as the sum of functions H_{n} constructed above and for

(Γ, (Γ′, a)) ∈ Mor(CC(C, p))

we set

H_{Mor}(Γ, (Γ′, a)) = (H_{Ob}(Γ), (H_{Ob}(Γ′), H(a)))

where H(a) was constructed above.

The fact that H_{Ob} commutes with the length functions is immediate from the construction. The fact that it commutes with the ft functions follows from Lemma 4.2, the fact that H_{Ob} and H_{Mor} form a functor follows from Lemma 4.3. The fact that H_{Mor} satisfies the p-condition follows from Lemma 4.4. The fact that H_{Mor} satisfies the q-condition follows from Lemma 4.5.

Applying Lemma 3.4 we conclude that H = (H_{Ob}, H_{Mor}) is a homomorphism of Csystems.

4.8. Lemma. Let (Φ, ϕ, ϕ̃) be as in Problem 4.6 and let H be the solution given by Construction 4.7. Then one has:

1. If Φ is a faithful functor and ϕ is a monomorphism then H is an injection of Csystems.

2. If Φ is a fully faithful functor and ϕ is an isomorphism then H is an isomorphism.

Proof. Both statements in relation to objects have straightforward proofs by induction on the length. In relation to morphisms the statements follow from the ones about the objects and the fact that int is fully faithful.

Lemma 4.8 can be further specialized into the following example.

4.9. Example. Let C be a category and p : Ũ → U a morphism in C. Let now (p_{X,F} , Q(F)) and (p′_{X,F} , Q′(F)) be two universe structures on p and pt and pt′ be two final objects in C. These data give us two universe categories. Let us denote them by UC and UC′. The identity functor Φ = Id_{C} on C together with the identity morphisms ϕ = Id_{U} and ϕ̃ = IdŨ define a universe category functor Φ : UC → UC′. The corresponding homomorphism of C-systems H_{Φ} : CC(UC) → CC(UC′) is an isomorphism with the inverse isomorphism given by the same triple considered as a universe functor from UC to UC′. This example shows that, up to a “canonical” isomorphism, the C-system defined by a universe category depends only on the category C and the morphism p.

4.10. Problem. Let (C, p) be a universe category. Let CC be a C-system. Given the following collection of data:

1. A functor I : CC → C from the underlying category of CC to C,

2. For each Γ ∈ CC a function

u_{Γ} : Ob_{1}(Γ) → Hom_{C}(I(Γ), U)

3. For each Γ ∈ CC, Δ ∈ Ob_{1}(Γ) an isomorphism

γ_{Δ} : (I(Γ); u(Δ)) → I(Δ)

such that

1. the morphism π_{I(pt)} : I(pt) → pt is an isomorphism

2. for each f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ) one has u_{Γ′}(f^{∗}(Δ)) = I(f) ∘ u_{Γ}(Δ),

3. for each f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ) one has p_{I(Γ),u(Δ)} = γ_{Δ} ∘ I(p_{Δ}),

4. for each f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ) one has γ_{f^{∗}(Δ)}∘I(q(f, Δ)) = Q(I(f), u(Δ))∘γ_{Δ}

to construct a C-system homomorphism

H(I, u, γ) : CC → CC(C, p)

In what follows we will often write u instead of u_{Γ}.

4.11. Construction. First we construct by induction on n pairs (H_{n}, ψ_{n}) where

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

is a function and ψ_{n} is a family of isomorphisms of the form

ψ_{n}(Γ) : int(H(Γ)) → I(Γ)

given for all Γ ∈ Ob_{n}(CC) as follows (we will sometimes write ψ instead of ψ_{n} and H instead of H_{n}):

1. For n = 0 we set

H(pt) = pt
ψ(pt) = (π_{I(pt)})^{−1} : pt → I(pt)

2. For the successor of n, Γ such that H_{n}(Γ) = B and Δ ∈ Ob_{1}(Γ) we set

H_{n+1}(Δ) = (B, ψ(Γ) ∘ u(Δ))  (24)

and

ψ(Δ) = Q(ψ(Γ), u(Δ)) ∘ γ_{Δ}  (25)

The fact that ψ(Δ) is an isomorphism follows from the inductive assumption, the assumption that γ_{Δ} is an isomorphism and Lemma 2.4.

The functions H_{n} define a function

H_{Ob} : Ob(CC) → Ob(CC(C, p))

where H_{Ob}(Γ) = (l(Γ), H_{l}(Γ)) that commutes with the length functions and functions ft. For f : Γ′ → Γ define

H_{Mor}(f) = (H_{Ob}(Γ′), (H_{Ob}(Γ), ψ(Γ′) ∘ I(f) ∘ ψ(Γ)^{−1}))

This gives us a function

H_{Mor} : Mor(CC) → Mor(CC(C, p))

Note that we can also define H_{Mor}(f) as the unique morphism such that

int(H_{Mor}(f)) = ψ(Γ′) ∘ I(f) ∘ ψ(Γ)^{−1}  (26)

Without using any more assumptions on I, γ and u one verifies easily that the pair H = (H_{Ob}, H_{Mor}) is a functor from the underlying category of CC to the underlying category of CC(C, p).

In view of Lemma 3.4 it remains to verify that H satisfies the p-morphism and the q-morphism conditions of Definition 3.1.

For the p-condition we need to verify that H(p_{Γ}) = p_{H(Γ)} for all Γ. Since both sides have the same domain and codomain and int is bijective on morphisms with the a given domain and codomain it is sufficient to verify that

int(H(p_{Γ})) = int(p_{H(Γ)})

We proceed by induction on n = l(Γ):

1. for n = 0

int(H(Id_{pt})) = int(Id_{pt}) = int(p_{pt}) = int(p_{H(pt)})

2. for the successor of n let Δ ∈ Ob_{n+1}(CC) and Γ = ft(Δ). Then Δ ∈ Ob_{1}(Γ) and

int(H(p_{Δ})) = ψ(Δ) ∘ I(p_{Δ}) ∘ ψ(Γ)^{−1} = Q(ψ(Γ), u(Δ)) ∘ γ_{Δ} ∘ I(p_{Δ}) ∘ ψ(Γ)^{−1} =

Q(ψ(Γ), u(Δ)) ∘ p_{I(Γ),u(Δ)} ∘ ψ(Γ)^{−1}

where the first equality is by (26), the second one by (25) and the third one by condition (3) of the problem. On the other hand we have

int(p_{H(Δ)}) = int(p_{(n+1,(H_{n}(Γ),ψ(Γ)∘u(Δ)))}) = p_{int(H(Γ)),ψ(Γ)∘u(Δ)}

where the first equality is by (24) and the second by (5). Composing with ψ(Γ) we get

int(H(p_{Δ})) ∘ ψ(Γ) = Q(ψ(Γ), u(Δ)) ∘ p_{I(Γ),u(Δ)}
int(p_{H(Δ)}) ∘ ψ(Γ) = p_{int(H(Γ)),ψ(Γ)∘u(Δ)} ∘ ψ(Γ)

and these expressions are equal by commutativity of the squares (2).

To prove the q-condition let us verify first that for f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ) one has

H(f^{∗}(Δ)) = H(f)^{∗}(H(Δ))  (27)

Let H(Γ′) = (m, A) and H(Γ) = (n, B). Then

H(f^{∗}(Δ)) = (m + 1, (A, ψ(Γ′) ∘ u(f^{∗}(Δ))))

by (24) and

H(f)^{∗}(H(Δ)) = H(f)^{∗}(n + 1, (B, ψ(Γ) ∘ u(Δ))) = (m + 1, (A, int(H(f)) ∘ ψ(Γ) ∘ u(Δ)))

where the first equality holds by (24) and the second by (6). Next one has

ψ(Γ′) ∘ u(f^{∗}(Δ)) = ψ(Γ′) ∘ I(f) ∘ u(Δ)

by condition (2) of the problem and

int(H(f)) ∘ ψ(Γ) ∘ u(Δ) = ψ(Γ′) ∘ I(f) ∘ ψ(Γ)^{−1} ∘ ψ(Γ) ∘ u(Δ) = ψ(Γ′) ∘ I(f) ∘ u(Δ) by (26).

The equality (27) implies that the morphisms H(q(f, Δ)) and q(H(f), H(Δ)) have the same domain and codomain. Therefore to prove that they are equal it is sufficient to prove that they become equal after application of int. We further compose both sides with ψ(Δ). Then we have

int(H(q(f, Δ))) ∘ ψ(Δ) = ψ(f^{∗}(Δ)) ∘ I(q(f, Δ)) =
Q(ψ(Γ′), I(f) ∘ u(Δ)) ∘ γ_{f^{∗}(Δ)} ∘ I(q(f, Δ)) =
Q(ψ(Γ′), I(f) ∘ u(Δ)) ∘ Q(I(f), u(Δ)) ∘ γ_{Δ} = Q(ψ(Γ′) ∘ I(f), u(Δ)) ∘ γ_{Δ}

where the first equality is by (26), the second by (25), the third by condition (4) of the problem and the fourth by Lemma 2.5. On the other hand

int(q(H(f), H(Δ))) ∘ ψ(Δ) = int(q(H(f), (n + 1, (B, ψ(Γ) ∘ u(Δ))))) ∘ ψ(Δ) =

Q(int(H(f)), ψ(Γ) ∘ u(Δ)) ∘ ψ(Δ) = Q(int(H(f)), ψ(Γ) ∘ u(Δ)) ∘ Q(ψ(Γ′), u(Δ)) ∘ γ_{Δ} =

Q(int(H(f)) ∘ ψ(Γ), u(Δ)) ∘ γ_{Δ} = Q(ψ(Γ′) ∘ I(f), u(Δ)) ∘ γ_{Δ}

where the first equality is by (24), the second by (7), the third by (25), the fourth by Lemma 2.5 and the fifth by (26). This completes Construction 4.11.

4.12. remark. The homomorphisms H(Φ, ϕ, ϕ̃) can be obtained as particular cases of the homomorphisms H(I, u, γ). More precisely, we can state without a proof that

H(Φ, ϕ, ϕ̃) = H(I, u, γ)

where:

1. I(Γ) = Φ(int(Γ)) and I(f) = Φ(int(f)),

2. for Γ = (n, B) and Δ = (n + 1, (B, F)),

u_{Γ}(Δ) = Φ(F) ∘ ϕ

3. for Γ = (n, B) and Δ = (n + 1, (B, F)), γ_{Δ} is the “natural” isomorphism from (Φ(int(B)); Φ(F) ∘ ϕ) to Φ(int(B); F). More precisely

γ_{Δ} = ((p_{Φ(int(B)),Φ(F)∘ϕ}) ∗ (Q(Φ(F) ∘ ϕ̃)))^{−1}

4.13. Lemma. Let I, u and γ be as in Problem 4.10 and let H be the corresponding homomorphism of Construction 4.11. Then one has:

1. If I is a faithful functor and u_{Γ} are injective then H is an injection of C-systems.

2. If I is a fully faithful functor and u_{Γ} are bijective then H is an isomorphism of C-systems.

Proof. Both statements in relation to objects have straightforward proofs by induction on the length. In relation to morphisms the statements follow from the ones about the objects and the fact that int is fully faithful and formula (26).

5. Every C-system is isomorphic to a C-system of the form CC(C, p)

5.1. Problem. Let CC be a C-system. Construct a universe category (C, p) and an isomorphism CC ≅ CC(C, p).

We will provide three different constructions for this problem - Constructions 5.2, 5.6 and 5.7 with the two latter constructions using the first one.

It is customary in the modern mathematics to use “the” category of sets Sets. In fact, every set X in the Zermelo-Fraenkel theory defines a category S(X) where:

Ob(S(X)) = X
Mor(S(X)) = ⨿_{x_{1},x_{2}∈X}F un(x_{1}, x_{2})

where F un(x_{1}, x_{2}) is the set of functions from x_{1} to x_{2}. This definition makes sense since elements of Zermelo-Fraenkel sets are themselves Zermelo-Fraenkel sets.

Taking X to be sets satisfying particular conditions, e.g. Grothendieck universes, one obtains categories that can be equipped with various familiar structures such as fiber products, internal Hom-objects etc. When one says consider “the” category of sets one presumably means the category S(GU) for a chosen Grothendieck universe GU.

The first construction that we provide assumes that we are working in set theory with a chosen Grothendieck universe (or in type theory with a chosen type theoretic universe) that contains the sets of objects and morphisms of our C-system. In the case of a type theory we will actually need two universes in order to have a type of which the first universe is an object.

In what follows we use the notations

Õb(CC) = {s ∈ Mor(CC) | s : ft(X) → X, l(X) > 0, s ∘ p_{X} = Id_{X}}

and ∂ : Õb(CC) → Ob(CC), ∂(s) = codom(s) that were introduced in [9]. We may sometimes abbreviate Ob(CC) to CC.

We will write Õb_{1}(Γ) for the subset of Õb that consists of s such that ft(∂(s)) = Γ. For f : Γ′ → Γ we have the function s ↦ f^{∗}(s, 1) (see [9]) that maps s to the element of Õb_{1}(Γ) that is the pull-back of the section s relative to f. We will denote this function by f^{∗}. It is easy to verify from the definitions that

(Id_{Γ})^{∗}(s) = s  (28)

and for g : Γ′′ → Γ′, f : Γ′ → Γ and s ∈ Õb_{1}(Γ) one has

g^{∗}(f^{∗}(s)) = (g ∘ f)^{∗}(s).  (29)

i.e., that the maps f^{∗} define on the family of sets Õb_{1} the structure of a presheaf. We continue using the notation Õb_{1} for this presheaf.

5.2. Construction. Denote by P reShv(CC) the category of presheaves on the precategory underlying CC, i.e., the category of contravariant functors from the precategory underlying CC to Sets.

Let Ob_{1} be the presheaf that takes an object Γ ∈ CC to the set Ob_{1}(Γ) and a morphism f : Γ′ → Γ to the map Δ ↦ f^{∗}(Δ). It is a functor due to the composition and unity axioms for f^{∗}.

Let Õb_{1} be the presheaf that takes Γ to Õb_{1}(Γ) described above.

Let further ∂ : Õb_{1} → Ob_{1} be the morphism that takes s to ∂(s). It is well defined as a morphisms of families of sets and forms a morphism of presheaves since ∂(f^{∗}(s)) = f^{∗}(∂(s)).

The morphism ∂ carries a universe structure that is defined by the standard pull-back squares in the category of presheaves.

We are going to construct a homomorphism CC → CC(P reShv(CC), ∂) using Construction 4.11 and to show that it is an isomorphism using Lemma 4.13.

We set Y o to be the Yoneda embedding.

We set

v_{Γ} : Ob_{1}(Γ) → Hom_{P reShv}(Y o(Γ), Ob_{1})

to be the standard bijections between sections of the presheaf Ob_{1} on an object Γ and morphisms from the corresponding representable presheaf Y o(Γ) to Ob_{1} in the category of presheaves. It follows easily from the definitions that for f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ) one has

v_{Γ′}(f^{∗}(Δ)) = Y o(f) ∘ v_{Γ}(Δ)  (30)

We also set

ṽ_{Γ} : Õb_{1}(Γ) → Hom_{P reShv}(Y o(Γ), Õb_{1})

to be the bijections of the same form for Õb_{1}. Again, it follows easily from the definitions that for f : Γ′ → Γ and s ∈ Õb_{1}(Γ) one has

ṽ_{Γ′}(f^{∗}(s)) = Y o(f) ∘ ṽ_{Γ}(s)  (31)

To construct γ we first need to prove a lemma. Recall that for Δ ∈ CC such that l(Δ) > 0 we let δ(Δ) : Δ → p_{Δ}^{∗}(Δ) denote the section of p_{p_{Δ}^{∗}(Δ)} given by the diagonal. We have

δ(Δ) ∈ Õb_{1}(Δ)

5.3. Lemma. Let Γ ∈ Ob(CC) and Δ ∈ Ob_{1}(Γ). Then the square

\begin{matrix}Y o(Δ) & ⟶^{ṽ(δ(Δ))} & Õb_{1} \\ ^{Y o(p_{Δ})}↓ & & ↓^{∂} \\ Y o(Γ) & ⟶^{v(Δ)} & Ob_{1} \end{matrix}  (32)

is a pull-back square.

Proof. We have to show that for any Γ′ ∈ CC the function

Hom(Γ′, Δ) → Hom(Γ′, Γ) ×_{Ob_{1}(Γ′)} Õb_{1}(Γ′)  (33)

defined by the square (32) is a bijection. Unfolding the definitions we see that this function sends g : Γ′ → Δ to the pair (g ∘ p_{Δ}, g^{∗}(δ(Δ))) and that the fiber product is relative to the function from Hom(Γ′, Γ) to Ob_{1}(Γ′) that sends f to f^{∗}(Δ) and the function from Õb_{1}(Γ′) to Ob_{1}(Γ′) that sends s to ∂(s).

Note that g^{∗}(δ(Δ)) = s_{g} where s is the s-operation of C-systems (see [9, Definition 2.3]) and g ∘ p_{Δ} is the morphism that we denoted in [9] by ft(g).

Let f_{1}, f_{2} : Γ′ → Δ be two morphisms such that their images under (33) coincide, i.e., such that ft(f_{1}) = ft(f_{2}) and s_{f_{1}} = s_{f_{2}}. This implies that f_{1} = f_{2} in view of [9, Definition 2.3(3)]. Therefore the function (33) is injective.

Let f : Γ′ → Γ be a morphism and s ∈ Õb_{1}(Γ′) a section such that ∂(s) = f^{∗}(Δ). Then the composition s ∘ q(f, Δ) is a morphism f′ : Γ′ → Δ such that f′ ∘ p_{Δ} = f. We also have

s_{f′} = s_{s∘q(f,Δ)} = s_{s} = s

which proves that (32) is surjective. This completes the proof of Lemma 5.3.

Let Γ ∈ Ob(CC) and Δ ∈ Ob_{1}(Γ). By construction, (Y o(Γ); v(Δ)) is the standard fiber product of the morphisms v(Δ) and ∂ in the category of presheaves. On the other hand Y o(Δ) is a fiber product of the same two morphisms by Lemma 5.3. Therefore there exists a unique isomorphism

γ_{Δ} : (Y o(Γ); v(Δ)) → Y o(Δ)

such that

γ_{Δ} ∘ ṽ(δ(Δ)) = Q(v(Δ))  (34)

and

γ_{Δ} ∘ Y o(p_{Δ}) = p_{Y o(Γ),v(Δ)}  (35)

It remains to verify the four conditions of Problem 4.10 since the conditions of Lemma 4.13(2) are obviously satisfied.

We have that Y o(pt) → pt is an isomorphism.

The second condition is (30).

The third condition is (35).

It remains to verify the fourth condition. Let f : Γ′ → Γ and Δ ∈ Ob_{1}(Γ). We need to show that

γ_{f^{∗}(Δ)} ∘ Y o(q(f, Δ)) = Q(Y o(f), v(Δ)) ∘ γ_{Δ}  (36)

Two of the morphisms that are involved in the condition can be seen on the diagram

(Y o(Γ′); v(f^{∗}(Δ))) ⟶^{γ_{f^{∗}(Δ)}} Y o(f^{∗}(Δ)) ⟶^{Y o(q(f,Δ))} Y o(Δ) ⟶^{ṽ(δ(Δ))} Õb_{1}
p_{Y o(Γ′),v(f^{∗}(Δ))}↓  ^{Y o(p_{f^{∗}(Δ)})}↓  ↓^{Y o(p_{Δ})}  ↓^{p}
Y o(Γ′)  Y o(Γ′)  ⟶^{Y o(f)} Y o(Γ) ⟶^{v(Δ)} Ob_{1}

By Lemma 5.3, Y o(Δ) is a fiber product with the projections Y o(p_{Δ}) and ṽ(δ(Δ)). Therefore it is sufficient to verify that the compositions of the two sides of (36) with the projections are equal, i.e., we have to prove two equalities:

γ_{f^{∗}(Δ)} ∘ Y o(q(f, Δ)) ∘ Y o(p_{Δ}) = Q(Y o(f), v(Δ)) ∘ γ_{Δ} ∘ Y o(p_{Δ})  (37)

and

γ_{f^{∗}(Δ)} ∘ Y o(q(f, Δ)) ∘ ṽ(δ(Δ)) = Q(Y o(f), v(Δ)) ∘ γ_{Δ} ∘ ṽ(δ(Δ))  (38)

For (37) we have

γ_{f^{∗}(Δ)} ∘ Y o(q(f, Δ)) ∘ Y o(p_{Δ}) = γ_{f^{∗}(Δ)} ∘ Y o(p_{f^{∗}(Δ)}) ∘ Y o(f) =
p_{Y o(Γ′),v(f^{∗}(Δ))} ∘ Y o(f) = p_{Y o(Γ′),Y o(f)∘v(Δ)} ∘ Y o(f)

where the first equality is by the commutativity of the canonical squares in CC and the fact that Y o is a functor, the second by (34) and the third one by (30). On the other hand

Q(Y o(f), v(Δ)) ∘ γ_{Δ} ∘ Y o(p_{Δ}) = Q(Y o(f), v(Δ)) ∘ p_{Y o(Γ),v(Δ)} = p_{Y o(Γ′),Y o(f)∘v(Δ)} ∘ Y o(f)

where the first equality is by (34) and the second by the commutativity of the squares (2).

For (38) we have

γ_{f^{∗}(Δ)} ∘ Y o(q(f, Δ)) ∘ ṽ(δ(Δ)) = γ_{f^{∗}(Δ)} ∘ ṽ(q(f, Δ)^{∗}(δ(Δ))) =
γ_{f^{∗}(Δ)} ∘ ṽ(δ(f^{∗}(Δ))) = Q(v(f^{∗}(Δ)))

where the first equality is by (31), the second follows from a simple computation in CC and the third one is by (34). On the other hand one has

Q(Y o(f), v(Δ))∘γ_{Δ}∘ṽ(δ(Δ)) = Q(Y o(f), v(Δ))∘Q(v(Δ)) = Q(Y o(f)∘v(Δ)) = Q(f^{∗}(Δ))

where the first equality is by (34), the second one by Lemma 2.5 and the third one by (30).

This completes Construction 5.2.

The second construction that we provide for Problem 5.1 is as follows. For a set M let Rp_{n}(M) be the set of subsets of (… (M × M) × …) × M where M occurs in the expression n + 1 times. Let Rp(M) be the category with

Ob(Rp(M)) = ⨿_{n≥0}Rp_{n}(M)
Mor(Rp(M)) = ⨿_{(m,X),(n,Y)}F un(X, Y)

where F un(X, Y) is the set of functions from X to Y and the identity morphisms and compositions of morphisms are given in the obvious way.

If our theory has a universe then the category Sets is defined and there is a functor F F : Rp(M) → Sets that sends (n, X) to X and acts on morphisms in the obvious way. This functor is fully faithful. (Note that it is not an inclusion of categories since, for example, the empty subset is an element of each of Rp_{n}(M) so that there are objects (n, ∅) for all n which are all mapped by F F to the one empty set of Sets).

Let CC be a C-system. Consider C = F unct(CC^{op}, Rp(Mor(CC))). Define a universe (p : Õ → O, p , Q(−)) in C as follows.

For Γ ∈ CC let

Ob′_{1}(Γ) = {f ∈ Mor(CC)| f = Id_{codom(f)})

and let ι_{Γ} : Ob′_{1}(Γ) → Ob_{1}(Γ) be the bijection defined by the codomain function codom. These bijections together with the structure of a presheaf on the family of sets Ob_{1}(Γ) define a structure of a presheaf on the family of sets Ob′_{1}(Γ). Let

O(Γ) = (0, Ob′_{1}(Γ)) ∈ Rp(Mor(CC))

The structure of a presheaf of sets on Ob′_{1} defines a structure of an element of C on O.

Next let

Õ(Γ) = (0, Õb_{1}(Γ)) ∈ Rp(Mor(C))

The structure of a presheaf on Õb_{1} provide Õ with a structure of an object of C. The morphism of presheaves ∂ defines in an obvious way a morphism p : Õ → O in C. Let us construct a universe structure on p.

Let X ∈ C and F : X → O. For Γ ∈ CC let X(Γ) = (n, X_{0}(Γ)) where X_{0}(Γ) is an element of Rp_{n}(Mor(CC)). Then

(X; F)_{0}(Γ) = {(x_{0}, s) ∈ X_{0}(Γ) × Õb_{1}(Γ) | F (x_{0}) = Id_{codom(s)}} ∈ Rp_{n+1}(Mor(CC))

is an element of Rp_{n+1}(Mor(CC)) and (X; F)(Γ) = (n + 1, (X; F)_{0}(Γ)) is an element of Rp(Mor(CC)).

It is easy to equip the family (X; F)(Γ) of elements of Rp(Mor(CC)) with a structure of an object of C and equally easy to define morphisms p_{X,F} : (X; F) → X and Q(F) : (X; F) → Õ.

We have also a functor I : CC → C that extends the family of sets

X ↦ (Y ↦ (0, Mor(X, Y)))

The image of the final object of CC under this functor is a final object in C which completes the description of a universe category structure on C.

5.4. Lemma. For any F : X → O the square

\begin{matrix}(X; F) & ⟶^{Q(F)} & Õ \\ ^{p_{X,F}} ↓ & & ↓^{p} \\ X & ⟶^{F} & O \end{matrix}  (39)

is a pull-back square in C.

Proof. One can either give a direct proof which would not require an extra universe or one can argue that the functor F F defines a functor Φ : C → P reShv(CC) which is fully faithful and which maps squares (39) to standard pull-back squares in the category of presheaves of sets.

5.5. Problem. To construct an isomorphism H : CC → CC(C, p) where (C, p) is the universe category constructed above.

There are two constructions for this problem. One we don’t describe here because giving its detailed description would take a lot of space and add little understanding. It is a direct construction based on Construction 4.11 and Lemma 4.13 that parallels Construction 5.2. This direct construction would not use any extra universes and, in combination with the construction of (C, p) based on the direct proof of Lemma 5.4 would provide a construction for Problem 5.1 that does not require any additional universes.

The construction that we give below uses Construction 5.2 and therefore requires an extra universe.

5.6. Construction. Let Φ : C → P reShv(CC) be the functor defined by F F. Since F F is fully faithful so is Φ. We have, by definition

Φ(O) = Ob′_{1}
Φ(Õ) = Õb_{1}

The bijections ι_{Γ} give us an isomorphism of presheaves

ι : Φ(O) = Ob′_{1} → Ob_{1}

which commute with Φ(p) and ∂ and together with Φ form a universe category functor (Φ, ι, Id_{Õb_{1}}). This universe category functor satisfies the conditions of Lemma 4.8(2) and therefore the homomorphism H(Φ, ι, Id_{Õb_{1}}) is an isomorphism. Composing the isomorphism of Construction 5.2 the inverse to this isomorphism we obtain a solution to Problem 5.5.

The direct construction of the universe category (C, p) does not increase the universe level but it uses the operation of taking the set of subsets that in type theory requires the propositional resizing rule in order to be defined inside a given universe. Here is an outline of a third construction that gives an even “tighter” universe category (C, p) with an isomorphism CC → CC(C, p).

5.7. Construction. Define by induction on n pairs (C_{n}, Φ_{n}) where C_{n} is a set and Φ_{n} : C_{n} → P reShc(CC) is a function as follows:

1. for n = 0 we set C_{0} = {pt, U, Ũ} and

Φ_{0}(pt) = pt
Φ_{0}(U) = Ob_{1}

Φ_{0}(Ũ) = Õb_{1}

where on the right hand side of the first equality is the final object of P reShv(CC),

2. for the successor of n we set

C_{n+1} = ⨿_{X∈C_{n}}Hom_{P reShv(CC)}(Φ_{n}(X), Ob_{1})

and

Φ_{n+1}(X, F) = (Φ_{n}(X); F)

where (X; F) is defined using standard fiber products in P reShv(CC).

We then define

Ob(C) = ⨿_{n≥0}C_{n}
Mor(C) = ⨿_{(m,X),(n,Y)∈Ob(C)}Hom_{P reShv(CC)}(Φ_{m}(X), Φ_{n}(Y))

The composition and the identity morphisms are defined in such a way as to make the pair of maps

Φ_{Ob} = ⨿_{n}Φ_{n}
Φ_{Mor} = ⨿_{(m,X),(n,Y)∈Ob(C)}i(Φ_{m}(X), Φ_{n}(Y))

where i(F, G) is the inclusion of Hom_{P reShv(CC)}(F, G) into Mor(P reShv(CC)), into a functor. This functor, which we denote by Φ, is then fully faithful.

One proves easily that pt is a final object of C. One defines the universe morphism in C as the morphism p : Ũ → U that is mapped by Φ to ∂. Given (m, X) ∈ Ob(C) and a morphism F : (m, X) → U one defines ((m, X); F) as (m + 1, (X, Φ(F))). This object is a vertex of the square

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

that is defined by the condition that it is mapped by Φ to the square

\begin{matrix}(Φ_{m}(X); Φ(F)) & ⟶^{Q(Φ(F))} & Õb_{1} \\ ^{p_{Φm(X),Φ(F)}}↓ & & ↓^{p} \\ Φ_{m}(X) & ⟶^{Φ(F)} & Õb_{1} \end{matrix}  (41)

Since Φ is fully faithful and the square (41) is a pull-back square, the square (40) is a pull-back square. This provides us with a universe structure on p and completes the construction of the universe category (C, p).

The functor Φ together with two identity morphisms forms a universe category functor Φ = (Φ, Id_{Ob_{1}}, Id_{Õb_{1}}) that satisfies the conditions of Lemma 4.13(2). Therefore Φ defines an isomorphism

CC(C, p) → CC(P reShv(CC), ∂)

composing the isomorphism of Construction 5.2 with the inverse to this isomorphism we obtain a solution to Problem 5.1. This completes Construction 5.7.

5.8. remark. The category C of Construction 5.7 has all of the structures of a C-system and these structures satisfy all of the required properties except for the property that l^{−1}(0) = {pt}. We would like to call such objects “generalized C-systems”. They seem to appear also in other examples and may play an important role in the future.

6. A universe category defined by a precategory

The following problem was inspired by a question from an anonymous referee of [9]. Here we have to use the word precategory as in the definition of a C-system since the construction for this problem is not invariant under equivalences. Let us recall the following definition that also introduces the notations to be used below.

6.1. Definition. A category with fiber products is a category together with, for all pairs of morphisms of the form f : X → Z, g : Y → Z, fiber squares

(X, f) ×_{Z} (Y, g) ⟶^{pr_{2}^{(X,f),(Y,g)}} Y
pr_{1}^{(X,f),(Y,g)}↓  ↓^{g}
X  ⟶^{f} Z

We will often abbreviate these main notations in various ways. The morphism pr_{2} ∘ g = pr_{1} ∘ f from (X, f) × (Y, g) to Z is denoted by f ⋄ g.

6.2. Problem. Let C be a precategory with a final object pt and fiber products. To construct a C-system CC and an equivalence of categories J_{∗} : CC → C, J^{∗} : C → CC.

6.3. remark. In the univalent formalization an extra condition that C is a set-category, i.e., that the type of objects of C is a set is required for the construction that we provide to work.

6.4. remark. The construction that we provide increases the universe level. It might be possible to provide another construction for Problem 6.2 that does not increase the universe level.

6.5. remark. Note that if we required an isomorphism CC → C then the problem would have no solution since, for example, there is no C-system whose set of objects is the set with two elements. Indeed, one of these elements, let us denote it by X, will have to have length n > 0. Then l(p_{X}^{∗}(X)) = l(X) + 1. Therefore p_{X}^{∗}(X) ≠ X and p_{X}^{∗}(X) ≠ pt which contradicts the assumption that CC has only two objects.

We start with a general construction that does not require C to have fiber products or a final object. The parts of it that do not concern C-systems must certainly have been known for a long time but we do not know where it was originally introduced.

For a precategory C let U_{C} be the presheaf such that

U_{C}(X) = {(f, g) where f : X → Y and g : Z → Y }

and for a : X′ → X,

U_{C}(a)(f, g) = (a ∘ f, g)

One proves easily that this presheaf data defines a presheaf.

Let Ũ_{C} be the presheaf such that

Ũ_{C}(X) = {(f′, g) where f′ : X → Z and g : Z → Y }

and for a : X′ → X,

Ũ_{C}(a)(f′, g) = (a ∘ f′, g)

Again one proves easily that Ũ_{C} this presheaf data defines a presheaf.

Let p_{C} : Ũ_{C} → U_{C} be the morphism given by

(p_{C})_{X}(f′, g) = (f′ ∘ g, g)

One proves easily that this family of maps of sets is a morphism of presheaves. As in Construction 5.2 let Y o be the Yoneda embedding and let

v_{X} : U_{C}(X) → Hom_{P reShv}(Y o(X), U_{C})
ṽ_{X} : Ũ_{C}(X) → Hom_{P reShv}(Y o(X), Ũ_{C})

be the standard bijections which we will often write as v and ṽ.

6.6. Lemma. For (f, g) ∈ U_{C}(X), (f′, g′) ∈ Ũ_{C}(X′) and u : X′ → X the square

\begin{matrix}Y o(X′) & ⟶^{ṽ(f′,g′)} & Ũ_{C} \\ ^{Y o(u)}↓ & & ↓^{p_{C}} \\ Y o(X) & ⟶^{v(f,g)} & U_{C} \end{matrix}  (42)

commutes if and only if g′ = g and the square

\begin{matrix}X′ & ⟶^{f′} & Z \\ ^{u}↓ & & ↓^{g} \\ X & ⟶^{f} & Y \end{matrix}  (43)

commutes. The square (42) is a pull-back square if and only if g = g′ and the square (43) is a pull-back square.

Proof. The assertion about commutativity is obvious. The proof of the assertion about being a pull-back square is as follows. The square (6.6) is a pull-back square if and only of for all X′′ the corresponding square of sections on X′′ is a pull-back square of sets. This square of sections is of the form

\begin{matrix}Hom(X′′, X′) & ⟶^{r_{1}} & \{(f′_{0} : X′′ → Z_{0}, g_{0} : Z_{0} → Y_{0})\} \\ ^{s_{1}}↓ & & ↓^{r_{2}} \\ Hom(X′′, X) & ⟶^{s_{2}} & \{(f_{0} : X′′ → Y_{0}, g_{0} : Z_{0} → Y_{0})\} \end{matrix}  (44)

where r_{1}(a′) = (a′ ∘ f′, g′), r_{2}(f′_{0}, g′_{0}) = (f′_{0} ∘ g′_{0}, g′_{0}), s_{1}(a) = a ∘ u, s_{2}(a) = (a ∘ f, g).

To check that (44) is a pull-back square it is sufficient to check that for every a ∈ Hom(X′′, X) the map s_{1}^{−1}(a) → r_{2}^{−1}(s_{2}(a)) defined by r_{1} is a bijection. We have

s_{1}^{−1}(a) = {a′ : X′′ → X′ | a′ ∘ u = a}

and

r_{2}^{−1}(s_{2}(a)) = {(v : X′′ → Z, g) | v ∘ g = a ∘ f}  (45)

and the map defined by r_{1} maps a′ to (a′ ∘ v, g).

Applying the same reasoning to the condition that the square is (43) is pull-back we see that it is equivalent to the condition that for all X′′ and all a : X′′ → X the map from the set

(− ∘ u)^{−1}(a) = {a′ : X′′ → X′ | a′ ∘ u = a}

to the set

(− ∘ g)^{−1}(a ∘ f) = {v : X′′ → Z | v ∘ g = a ∘ f}  (46)

given by a′ ↦ a′ ∘ f′, is a bijection. Since g in (45) the sets on the right hand sides of (45) and (46) are in the obvious bijection that is compatible with the functions from {a′ : X′′ → X′ | a′ ∘ u = a} and therefore these two conditions are equivalent.

Applying our main construction to (P reShv(CC), p_{C}) we obtain, for any precategory C, a C-system CC(C) = CC(P reShv(CC), p_{C}).

6.7. Problem. Let C be a precategory with a final object pt. To construct a function J_{1}^{∗} : Ob(C) → Ob_{1}(P reShv(C), p_{C}) and a family of isomorphisms j_{X} : Y o(X) → int(J^{∗}(X)).

6.8. Construction. Let X ∈ Ob(C). The pull-back square

X ⟶^{Id_{X}} X
π_{X} ↓  ↓^{π_{X}}
pt ⟶^{Id_{pt}} pt

defines by Lemma 6.6 a pull-back square

\begin{matrix}Y o(X) & ⟶^{ṽ(Id_{X},π_{X})} & Ũ_{C} \\ ^{Y o(π_{X})}↓ & & ↓^{p_{C}} \\ Y o(pt) & ⟶^{v(Id_{pt},π_{X})} & U_{C} \end{matrix}  (47)

Let ψ : pt → Y o(pt) be the unique isomorphism. Set

J^{∗}(X) = (pt, ψ ∘ v(Id_{pt}, π_{X}))

Then

π_{Y o(X)} ∘ ψ = Y o(π_{X})

and therefore π_{Y o(X)} ∗ ṽ(Id_{X}, π_{X}) is a well defined morphism from Y o(X) to J^{∗}(X). It is easy to prove now that since (47) is a pull-back square this morphism is an isomorphism.

6.9. remark. For C with a final object pt, the set Ob_{1}(P reShv(CC), p_{C}) is in a constructive bijection with the set of pairs (f : pt → Y, g : Z → Y) which is given, in the notation of Construction 6.8, by the map (f, g) ↦ ψ ∘v(f, g). After composition with this bijection the function J^{∗} takes X to (Id : pt → pt, π_{X} : X → pt). The function (f, g) ↦ dom(g) defines a one-sided inverse to J_{1}^{∗} so that J_{1}^{∗} is always a split monomorphism.

6.10. Problem. Suppose that C is a category with a final object pt and fiber products. To construct a function J_{∗} : Ob(CC(C)) → Ob(C) and for every Γ ∈ Ob(CC(C)) an isomorphism σ_{Γ} : Y o(J_{∗}(Γ)) → int(Γ).

6.11. Construction. We first construct by induction on n, pairs (J_{n}, σ_{n}) where

J_{n} : Ob_{n}(P reShv, p_{C}) → Ob(C)

and σ_{n} is a family of isomorphisms

σ_{n}(A) : Y o(J_{n}(A)) → int_{n}(A)

given for all A ∈ Ob_{n}(P reShv, p_{C}) as follows (we write J instead of J_{n} and σ instead of σ_{n}):

1. For n = 0 we set J(A) = pt and σ(A) : Y o(pt) → pt is the unique isomorphism,

2. For the successor of n we proceed as follows. Let (B, F) ∈ Ob_{n+1} where B ∈ Ob_{n} and F : int(B) → U_{C}. Then

v^{−1}(σ_{B} ∘ F) ∈ U_{C}(J(B))

is of the form

v^{−1}(σ_{B} ∘ F) = (f : J(B) → Z, g : Y → Z)

Let

J(B, F) = (J(B), f) ×_{Z} (Y, g)

To define σ(B, F) consider the diagram

Y o(J(B, F)) ⟶^{ι} (Y o(J(B)), σ(B) ∘ F) ⟶^{Q(σ(B),F)} (int(B); F) ⟶^{Q(F)} Ũ_{C}
Y o(pr_{1})↓  ^{p_{Y o(J(B)),σ(B)∘F}} ↓  ^{p_{int(B),F}} ↓  ↓^{p_{C}}
Y o(J(B))  Y o(J(B))  ⟶^{σ(B)}  int(B) ⟶^{F} U_{C}

where ι is the morphism Y o(pr_{1}) ∗ ṽ(pr_{2}, g). This morphism is defined because

Y o(pr_{1}) ∘ σ(B) ∘ F = Y o(pr_{1}) ∘ v(f, g) = (pr_{1} ∘ f, g)

and

ṽ(pr_{2}, g) ∘ p_{C} = (pr_{2} ∘ g, g)

and pr_{1} ∘ f = pr_{2} ∘ g. By Lemma 6.6 the square

Y o(J(B, F)) ⟶^{ṽ(pr_{2},g)} Ũ_{C}
Y o(pr_{1})↓  ↓^{p_{C}}
Y o(J(B)) ⟶^{v(f,g)} U_{C}

is a pull-back square which implies that ι is an isomorphism. We define

σ(B, F) = ι ∘ Q(σ_{B}, F)

The morphism Q(σ(B), F) is an isomorphism by Lemma 2.4 and therefore σ(B, F) is an isomorphism.

We now define J_{∗} as the sum over n ∈ N of J_{n}. This completes Construction 6.11.

6.12. remark. Using the bijection of Remark 6.9 we can look at the function from pairs (f : pt → Z, g : Z → Y) to Ob(C) corresponding to J_{1}. This function is given by

(f, g) ↦ (pt, f) ×_{Z} (Y, g)

When we compose it with J^{∗} and consider J_{∗}(J^{∗}(X)) we obtain (pt, Id_{pt}) ×_{p} t(X, π_{X}). Depending on the choice of the fiber product this element of Ob(C) may be equal to X or not but in any case there is a natural in X isomorphism X → J_{∗}(J^{∗}(X)).

We can now provide the following construction for Problem 6.2.

6.13. Construction. Let J^{∗} : Ob(C) → Ob(CC(C)) be the composition of the function J_{1}^{∗} of Construction 6.8 with the inclusion of Ob_{1}(P reShv, p_{C}) into Ob(CC(P reShv, p_{C})). We can extend it to the data for a functor setting:

J_{Mor}^{∗}(f : X → Y) = int_{J^{∗}(X),J^{∗}(Y)}^{−1}(j_{X}^{−1} ∘ Y o(f) ∘ j_{Y})

where int_{Γ,Γ′} is the bijection

Hom_{CC(C)}(Γ, Γ′) → Hom(int(Γ), int(Γ′))

defined by the functor int. It is easy to prove from definitions that it is a functor and, using the fact that both Y o and int are fully faithful, that J^{∗} is fully faithful.

Similarly we can extend J_{∗} of Construction 6.11 to the data for a functor setting

(J_{∗})_{Mor}(f : Γ′ → Γ) = Y o_{J_{∗}(Γ′),J_{∗}(Γ)}^{−1}(σ_{Γ′} ∘ int(f) ∘ σ_{Γ}^{−1})

where Y o_{X,Y} is the bijection

Hom_{C}(X, Y) → Hom_{P reShv}(Y o(X), Y o(Y))

defined by the Yoneda embedding. Again it is easy to prove from definitions that this functor data is a functor and using the fact that both int and Y o are fully faithful that J_{∗} is fully faithful.

After J_{∗} and J^{∗} have been extended to morphisms it makes sense to ask whether the families of isomorphisms j_{X} and σ_{Γ} are natural in X and Γ respectively and one verifies easily that they indeed are.

Let X ∈ Ob(C) then we have an isomorphism

Y o(J_{∗}(J^{∗}(X))) ⟶^{σ_{J^{∗}(X)}} int(J^{∗}(X)) ⟶^{j_{X}^{−1}} Y o(X)

which is natural in X and applying to it Y o_{J_{∗}(J^{∗}(X)),X}^{−1} we get an isomorphism

J_{∗}(J^{∗}(X)) → X

which is again natural in X, i.e., we obtained a functor isomorphism J_{∗} ∘ J^{∗} → Id. Similarly, starting with,

int(Γ) ⟶^{σ_{Γ}^{−1}} Y o(J_{∗}(Γ)) ⟶^{j_{J∗(Γ)}} int(J^{∗}(J_{∗}(Γ)))

one obtains a functor isomorphism Id → J^{∗} ∘ J_{∗}. This completes the Construction 6.13.

6.14. remark. The construction of the C-system CC(C) does not require a choice of a final object or fiber products in C and in particular does not depend on such choices.

The functor J^{∗} : C → CC(C) requires a choice of a final object for its construction and depends on this choice. Let B be the bijection

Ob_{1}(P reShv(CC), p_{C}) → {(f : pt_{1} → Z, g : Y → Z)}

of Remark 6.9 defined by the choice of a final object pt_{1}. Let J_{1,1}^{∗} and J_{1,2}^{∗} be the functions Ob(C) → Ob_{1}(P reShv, p_{C}) of Construction 6.7 defined by the choice of the final object pt_{1} and a final object pt_{2} respectively. Then one has

B(J_{1,1}^{∗}(X)) = (Id : pt_{1} → pt_{1}, π_{X,1} : X → pt_{1})

and

B(J_{1,2}^{∗}(X)) = (a : pt_{1} → pt_{2}, π_{X,2} : X → pt_{2})

where a : pt_{1} → pt_{2} is the unique morphism. This shows that J_{1,1}^{∗} ≠ J_{1,2}^{∗} if pt_{1} ≠ pt_{2} and in particular that J^{∗} depends on the choice of the final object.

The fact that J_{∗} depends on the choice of fiber products is seen from the formula for J_{∗}(J^{∗}(X)) given in Remark 6.12.

6.15. Conjecture. Let C be a category, CC be a C-system and M : CC → C a functor such that M(pt_{CC}) is a final object of C and M maps distinguished squares of CC to pull-back squares of C. Then there exists a universe p_{M} : Ũ_{M} → U_{M} in P reShv(C) and a C-system homomorphism M′ : CC → CC(P reShv(C), p_{M}) such that the square

CC  ⟶^{M}  C
↓_{M′}  ↓
CC(P reShv(C), p_{M}) ⟶^{int} P reShv(C)

where the right hand side vertical arrow is the Yoneda embedding, commutes up to a functor isomorphism.

References

[1] Peter  Aczel.  A  general  Church-Rosser  theorem.

   http://www.ens-lyon.fr/LIP/REWRITING/MISC/AGeneralChurch-RosserTheorem.pdf,

1978.

[2] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Math. Structures Comput. Sci., 25(5):1010–1039, 2015.

[3] John Cartmell. Generalised algebraic theories and contex-

tual categories.  Ph.D. Thesis,  Oxford University,  1978.

   https://uf-ias-2012.wikispaces.com/Semantics+of+type+theory.

[4] John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32(3):209–243, 1986.

[5] Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding (extended abstract). In 14th Symposium on Logic in Computer Science (Trento, 1999), pages 193–202. IEEE Computer Soc., Los Alamitos, CA, 1999.

[6] André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Logic, language, information and computation, volume 4576 of Lecture Notes in Comput. Sci., pages 218–237. Springer, Berlin, 2007.

[7] Vladimir  Voevodsky.  Notes  on  type  systems.

   https://github.com/vladimirias/old_notes_on_type_systems,  2009–

2012.

[8] Vladimir Voevodsky. C-system of a module over a monad on sets. arXiv 1407.3394, submitted, pages 1–20, 2014.

[9] Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In Conference on Mathematics and its Applications, (Kuwait City, 2014), number to appear, pages 1–11, 2015.

School of Mathematics, Institute for Advanced Study, Princeton NJ, USA.

Email: vladimir@math.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: 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, Radboud University Nijmegen: i.moerdijk@math.ru.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: street@math.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