{'fraction_non_alphanumeric': 0.05750806080147398, 'fraction_numerical': 0.01303546752648549, 'mean_word_length': 3.552899234560134, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Martin-Lof identity types in the C-systems defined by a universe category

This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Lof type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.


Introduction
The concept of a C-system in its present form was introduced in [16]. The type of the C-systems is constructively equivalent to the type of contextual categories defined by Cartmell in [3] and [2] but the definition of a C-system is slightly different from the Cartmell's foundational definition.
In the past decade or more, it has been a tradition in the study of type theories to consider, as the main mathematical object associated with a type theory, not a C-system by a category with families (see [4]). As was observed recently all of the constructions of [13], [15] and of the present paper (but not of [16] or [14]!) can be either used directly or reformulated in a very straightforward way to provide very similar results for categories with families. This modification will be discussed in a separate paper or papers.
In this introductory explanation we will distinguish between the syntactic and semantic Csystems. By a syntactic C-system we will mean a C-system that is a regular sub-quotient of a C-system of the form CC(R, LM) where R is a monad on sets and LM is a left module over R, see [14] and [16]. In particular, the C-systems of all of the various versions of dependent type theory of Martin-Lof "genus" are syntactic type systems in the sense of this definition.
By a semantic C-system we will mean a C-system whose underlying category is a full subcategory in a category of "mathematical" nature such as the category of sets or the category of sheaves of sets.
Usually one knows some good properties (i.e. consistency) of a given semantic C-system and tries to prove similar good properties of a syntactic C-system by constructing a functor from the syntactic one to the semantic one.
To construct such a functor one tries to show that the syntactic C-system is an initial one among C-systems equipped with some collection of additional operations and then to construct operations of the required form on the semantic one. A pioneering example of this approach can be found in [8].
In this paper we investigate the set of three interconnected operations on C-systems that, in the case of the syntactic C-systems, corresponds to the set of inference rules that is known as the rules for identity types in intensional Martin-Lof type theories (first published in [6]) 4 . Since the key ingredient of this structure is known in type theory as the J-eliminator we call it the J-structure.
We do not use the "sequent" notation that is so widespread in the literature on type theory for general C-systems restricting its use only to examples where we assume the C-system to be a syntactic one.
The reason for this restriction is that translating the sequent-like notations into the algebraic notation of C-systems or categories with families requires considerable mastery of various conventions connected to the use of dependently typed systems. An example of such a trans-lation is the description of an object IdxT (T ) corresponding to the sequent-like expression (Γ, x : T, y : T, e : IdT T x y ; ) in Construction 1.4.
Some of the difficulties that arise here can already be seen on the translation of the sequentlike expression (Γ, x : T, y : T ; ). Here the same letter T is used to refer to objects of two different types -the first T refers to an element on Ob 1 (Γ) and the second T refers to an element in Ob 1 (T ). It is "understood" that the second T is the image of the first T under the map p * T : Ob 1 (Γ) → Ob 1 (T ) but this understanding is a part of a tradition and is not reflected in any mathematical statement that one can refer to.
For the syntactic C-systems we are allowed to use the sequent notation for the following reason. First, since CC in this case is a sub-quotient of CC(R, LM) our notation only needs to provide a reference to elements of sets associated with CC(R, LM) itself. There, the first T refers to an element of LM({1, . . . , l}) where l is the length of Γ and LM(X) is the set of type expressions in the raw syntax with free variables from a set X and the second T refers to an element of LM({1, . . . , l + 1}) that is the image of the first T under the map LM({1, . . . , l}) → LM({1, . . . , l + 1}) defined by the inclusion {1, . . . , l} ⊂ {1, . . . , l + 1}. In this case the map does not depend on T . We should distinguish between IdT as a structure on the C-system and the corresponding syntactic construction (because they have different types). If we denote the syntactic "identity types" by IdT s T t 1 t 2 then for the sequence Γ, x : T, y : T, e : IdT s T x y; to define an element of Ob(CC(LM, R)), the expression IdT s T x y must refer to an element of LM({1, . . . , l + 2}) and its form shows that we assume that there is an operation IdT s : LM × R × R → R (a natural transformation of functors that is a linear morphism of left R-modules) and IdT s T x y is the "named variables" notation for IdT s 1,...,l+2 (T, l + 1, l + 2). We do not continue this explanation of how to construct J-structures on syntactic C-systems. This will be done in a separate paper. Let us remark however that constructing J-structures on syntactic C-systems is relatively easy and that the difficult questions about J-structures on such C-systems are the ones related to the initially properties of the resulting objects.
While constructing J-structures on the syntactic C-systems relatively straightforward, constructing non-degenerate 5 J-structures on semantic C-systems or categories with families proved to be very difficult.
The first instance of such a construction, due to Martin Hofmann and Thomas Streicher, appeared in [5]. It was done in the language of categories with families and the underlying category there was the category of groupoids.
The construction of Hofmann and Streicher was substantially extended and generalized in the Ph.D. thesis of Michael Warren [17], [18] and his subsequent papers such as [19].
Further important advances were achieved in the work of Richard Garner and Benno van den Berg [10].
Two main results of the first part of this paper provide a new approach to the construction of J-structures on semantic C-systems, an approach that can be used to construct the Jstructure on the C-system of the univalent model. Construction 2.10 provides a simple way of extending a J1-structure on a universe p in a category C to a full J-structure. Construction 4.15 provides a method of constructing a J-structure on the C-system CC(C, p) from a J-structure on p.
Combined together they provide a method of constructing a J-structure on CC(C, p) from a J1-structure on p.
We also discuss two sets of conditions on a pair of classes of morphisms T C and F B in a locally cartesian closed category that can be used in combination with Construction 2.10 to construct J-structures. These conditions often hold for the classes of trivial cofibrations and fibrations in model categories (or categories with weak factorization systems) providing a way of constructing C-systems with J-structures starting from such categories.
In this paper we continue to use the diagrammatic order of writing composition of morphisms, i.e., for f : X → Y and g : Y → Z the composition of f and g is denoted by f • g.
In this paper, as in the preceding papers [13] and [15], we often have to consider structures on categories that are not invariant under equivalences and their interaction with structures that are invariant under the equivalences.
The methods used in this paper are fully constructive and the paper is written in "formalization ready" style with all the proofs provided in enough detail to ensure that there are no hidden difficulties for the formalization of all of the results presented here.
Except for the section that discusses the use of classes T C and F B, the methods we use are also completely elementary in the sense that they rely only on the essentially algebraic language of categories with various structures.
The key Definition 2.8 and its relation to the J-structures on categories CC(C, p) first appeared in [11].
The author would like to thank the Department of Computer Science and Engineering of the University of Gothenburg and Chalmers University of Technology for its hospitality during the work on this paper.
2 J-structures on C-systems and on universe categories 1 The J-structure on a C-system To define the J-structure on a C-system we will actually define three structures J0-structure, J1-structure over a J0-structure and and J2-structure over a J1-structure with the J-structure being the same as a triple (IdT, ref l, J) where Idt is a J0-structure, ref l is a J1-structure over IdT and J is a J2-structure over ref l. For the notations used below see [15].

Definition 1.1 A J0-structure on a C-system CC is a family of functions
given for all Γ ∈ Ob that is natural in Γ i.e. such that for any f : given for all Γ ∈ Ob such that:

for any
To define the notion of a J2-structure over a given J1-structure we will need to describe two constructions first.

Construction 1.4
Recall that for T ∈ Ob 1 (Γ) we let δ(T ) denote the morphism T → p * T (T ) that can be described equivalently as s Id T or as the only morphism such that δ(T ) • p p * T (T ) = Id T and δ T • q(p T , T ) = Id T . Because of the first equation we have δ(T ) ∈ Ob(p * T (T )). We define: IdxT (T ) := IdT p * T (T ) ((p * Problem 1.5 Given a J0-structure IdT and a J1-structure ref l over it to construct for all Γ ∈ Ob and T ∈ Ob 1 (Γ) a morphism such that for any f : Construction 1. 6 We have: where the last equality follows from the fact that f * (δ(T )) = s f and for any s ∈ Ob, s s = s. This shows that we have a canonical square of the form and ref l(δ(T )) is a morphism T → IdT (δ(T ), δ(T )). We define: The proof that for any f : Γ ′ → Γ one has f * (rf T ) = rf f * (T ) is straightforward.
Definition 1.7 Let IdT and ref l be a J0-structure and a J1-structure over it. A J2structure over (IdT, ref l) is data of the form: for all Γ ∈ Ob, for all T ∈ Ob 1 (Γ), for all P ∈ Ob 1 (IdxT (T )), for all s0 ∈ Ob(rf * T (P )), an element J(Γ, T, P, s0) of Ob(P ) such that: 1. J is natural in Γ, i.e., for any f : Γ ′ → Γ and T, P, s0 as above one has where the right hand side of the equation is well-defined because of the naturality in f of IdxT and rf .
2. J satisfies the ι-rule. For Γ, T, P, s0 as above one has rf * T (J(Γ, T, P, s0)) = s0 One can easily see that any two extensional J0-structures are equal and that any extensional J0-structure has a unique extension to a full J-structure that is also called extensional.
We will not consider these extended versions of J in the present version of the paper.

Remark 1.9
When one studies J-structures on C-systems that have no (Π, λ)-structures it is important, as emphasized for example in [9], to consider a more complex structure than the one that we consider here. This more complex structure can be seen as a family of structures eJ n where eJ 0 = J2 and where eJ n over (IdT, ref l) is a collection of data of the form: for all Γ ∈ Ob, for all T ∈ Ob 1 (Γ), for all ∆ ∈ Ob n (IdxT (T )), for all P ∈ Ob 1 (∆), for all s0 ∈ Ob(rf * T (P )), an element eJ n (Γ, T, ∆, s0) in Ob(P ) such that eJ n satisfies the obvious analog of ι-rule and such that it is natural in Γ. See also Remark 2.11.
2 The J-structure on a universe in a category Let C be a (pre-)category and p : U → U a morphism in C. Recall that a universe structure on p is a choice of pull-back squares of the form for all X and all morphisms F : X → U. A universe in C is a morphism with a universe structure on it and a universe category is a category with a universe and a choice of a final object pt.
For f : W → X and g : W → U we will denote by f * g the unique morphism such that When we need to distinguish canonical squares of different universes we may write (X; F ) p and f * p g.
Remark 2.1 Note that we made no assumption about Q(Id U ) being equal to Id U . In fact, since we want the results of this paper to be constructive, we are not allowed to make such an assumption since the question of whether or not a given morphism is an identity morphism need not be decidable and therefore we can not "normalize" our constructions by doing a "case" on whether a morphism is an identity morphism or not. The importance of this observation (in the context of whether a simplex is degenerate or not) was emphasized by [1]. For As is shown in [15], the square is a pull-back square.
Following [15] we define for any universe p : U → U and any V ∈ C a functor whose action on morphisms is given by When C is a locally cartesian closed category any morphism p : U → U defines a functor that are natural in X and V . We let η denote the inverse bijections Using the functorial structure on the mapping V → (U × V, pr 1 ) together with the naturality of internal Hom-objects in the second argument we get a functoriality structure on I p Similarly, using the functoriality of Hom in the second argument (see e.g. the appendix in [15]) we obtain, for any p : U → U, p ′ : U ′ → U and h : U ′ → U over U and V a morphism Lemma 2.2 In the notations introduced above let f : V → V ′ be a morphism, then the square Proof: This is a particular case of the commutative square of [15,Lemma 8.5].
Lemma 2.3 Let p : U → U and p ′ : U ′ → U be two morphisms with universe structures and f : U ′ → U be a morphism over U. For V ∈ C let I f (V ) be the corresponding morphism . Then for any X the square where the left hand side arrow is of the form

commutes.
Proof: Since η is defined as an inverse to η ! it is sufficient to show that for any g ∈ Hom(X, I p (V )) one has η ′ ,! (g • I f (V )) = D f (X, V )(η ! (g)). Let be the canonical projections. Let be the morphisms introduced in [15]. By [15,Problem 3.8] we have and Therefore it is sufficient to show that The first equality asserts that I f (V ) is a morphism over U which follows from its construction.
By Lemma 1.1 we have by [15,Lemma 3.2]. It remains to check that This requires opening up the definitions of st and st ′ which gives us We will obtain this equality as a consequence of commutativity of three squares: and The first two squares are particular cases of [15,Lemma 8.1]. To obtain the first one one has to set Z = U, b = Id U ′ , and a = I f (V ). To obtain the second one one has to set Z = U, b = f and a = Id Ip(V ) . The last square is a particular case of [15,Lemma 8.6].
Definition 2.4 A J0-structure on a universe p in a category C is a morphism Eq : ( U; p) → U.
Let Eq be a J0-structure on p. Consider the object E U := ( U; p, Eq) as an object over U relative to the composition of projections that we will denote by pE U .
Problem 2.5 To construct a universe structure on pE U .

Construction 2.6
We have three diagrams with pull-back squares of the form: and we define the canonical square for F relative to pE U to be the square obtained by concatenating these three squares vertically.
Let us denote the components of the canonical squares for pE U as follows: p E X,F = p (X;F,Q(F )•p),Q(Q(F ),p)•Eq • p (X;F ),Q(F )•p • p X,F We will also write Q(f, F ) E for the canonical morphisms from (X; f • F ) E to (X; F ) E . Definition 2.7 Let p be a universe in C and Eq be a J0-structure on p. A J1-structure on p over Eq is a morphism Ω : U → U such that the square The square (6) defines a morphism U → E U that we will denote by ω.
To define a J2-structure on a universe we will need to assume that C is a locally cartesian closed category. Recall that locally cartesian closed category is a category with the choice of fiber squares based on all pairs of morphisms with a common codomain as well as the choice of relative internal Hom-objects and co-evaluation morphisms for all such pairs. For our notations related to the locally cartesian closed categories as well as for some other notations used below see [15].
When a universe is considered in a locally cartesian closed category we make no assumption about the compatibility of choices of the pull-back squares of the universe structure on p and pull-back squares of the locally cartesian closed structure.
Consider the functors I p and I pE U . We have the following commutative square: and therefore a morphism Definition 2.8 A J2-structure on p relative to a J0-structure Eq and J1-structure Ω, is a morphism Note that we have: where prI p (V ) is the canonical morphism I p (V ) → U.
A J-structure on p is a triple (Eq, Ω, Jp) where Eq is a J0-structure, Ω is a J1-structure relative to Eq and Jp a J2-structure relative to Eq and Ω.
For a J1-structure (Eq, Ω) on a universe in a category with a locally cartesian closed structure let F p Eq,Ω denote the fiber product and let pF p Eq,Ω = I ω (U) ⋄ I p (p) be the projection F p Eq,Ω → U. Let further pr 1 be the projection from F p to I pE U (U) and pr 2 the projection from F p to I p ( U ).
Our solution to the following problem is the key to the construction of J-structures over a given J1-structure in categories with weak factorization systems in particular in Quillen model categories.

Problem 2.9
Let C be a category with a locally cartesian closed structure and Eq, Ω be a J1-structure on (C, p). To construct a bijection between the set of J-structures on p over (Eq, Ω) and the set of morphisms (F p, pF p) × U (E U , pE U) → U that split the following square into two commutative triangles: Construction 2.10 Observe first that there is a bijection between the set of morphisms that split the square (10) into two commutative triangles and the set of morphisms that split into two commutative triangles the square: The rule f → adj(f ) gives us a bijection of the form All sections of coJ are automatically morphisms over U. Therefore it remains to show that this bijection defines a bijection of the subset of morphisms that are sections of coJ and morphisms that make the two triangles commutative.
One verifies first that a morphism f : F p → I pE U ( U ) is a section of coJ if and only if f • I pE U (p) = pr 1 and f • I ω ( U ) = pr 2 . This is straightforward.
Next we have Therefore by [15,Lemma 8.7] one has and we conclude that f is a section of coJ iff This completes the construction.

Remark 2.11
It is likely to be relatively easy to generalize the constructions of this paper to the extended J-structures eJ n (see Remark 1.9). The key to such generalization is [15,Remark 3.13]. The structures eJp n can be defined in the same way as Jp but with the square (7) replaced by the square

J-structures on universes in categories with two classes of morphisms
This is the only part of the paper where we depart from constructions that are conservatively algebraic over the theory of categories, i.e., from constructions that can be expressed in terms of adding new essentially algebraic operations to the theory of categories without adding new sorts to this theory.
Considering classes of morphisms in categories can be expressed in the essentially algebraic way but this requires adding new sorts to the theory.
This is also the only context where we use the concept "there exists" in this paper. In all the previous cases the objects that we considered were given (specified). To make the lemmas proved below into constructions and to avoid the use of "there exists" one would have to define the collection F B as a collection of pairs of a morphism p together with, for Recall that a collection of morphisms R is said to have the right lifting property for the collection of morphisms L if for any commutative square of the form such that i ∈ L and p ∈ R there exists a morphism g : W → E that makes the two triangles into which it splits the square to commute i.e. a morphism g such that i • g = f Z and We are going to consider two sets of conditions (Conditions 3.1 and 3.3) on a pair of classes of morphisms F B and T C in a category with fiber products and then show in Theorems 3.2 and 3.8 how pairs satisfying conditions of each of these two sets can be used to construct J-structures on elements of F B.
Our first set of conditions is as follows:

consider morphisms
Then the morphism is in T C.
Theorem 3.2 Let F B and T C be two classes of morphisms in a locally cartesian closed category C that satisfy Conditions 3.1. Let p be a universe in C and (Eq, Ω) a J1-structure on p such that: Then there exists an extension of (Eq, Ω) to a full J-structure on p.
Proof: Let us apply Construction 2.10 to (Eq, Ω). To construct the required morphism it is sufficient to establish that Id F p × ω is in T C. It follows from the first of our conditions that F B is closed under pull-backs and compositions. Therefore, pE U is in F B. It remains to apply the second of our conditions.
Our second set of conditions is more involved. Conditions of this set can be satisfied in the situations arising when one attempts to localize Quillen model structures and when the resulting sets of morphisms do not for a model structure. The difference is mainly concerned with the fact that the good behavior is required only for fibrations over fibrant objects. One particular example of such situation is considered in [12,Section 3.3].
and only if it has the right lifting property for T C, iis an arbitrary morphism then is in T C.
We will say that B is fibrant if the morphism B → pt is in F B.
Proof: Since B ′ is fibrant it is sufficient to verify that p ′ has the right lifting property for T C. This can be shown in the standard way to be a consequence of p having the right lifting property for T C. That p has this property we know because p is in F B and B is fibrant.
Lemma 3.5 Let B be fibrant and p 2 : Since pt is fibrant it is sufficient to show that π E 1 has the right lifting property for T C. It is shown in the standard way from the fact that both p 1 and π B : B → pt have the right lifting property for T C and π E 1 = p 1 • π B .
Since E 1 is fibrant we know that p 2 has the right lifting property for T C and since B is fibrant we know that p 1 has the right lifting property for F B. From this we conclude in the standard way that p 2 • p 1 have the right lifting property for T C and since B is fibrant this implies that Lemma 3.6 Assume that U, V are fibrant and that p : Proof: Since U is fibrant it is sufficient to check that pr = prI p (V ) has the right lifting property for T C. Consider a commutative square of the form We need to construct a morphism f : W → Hom U (( U , p), (U × V, pr 1 )) that would make the two triangles commutative. The commutativity of the lower triangle means that f is a morphism over U which is equivalent to the assumption that f = adj −1 (g) for some g : Consider the square By Lemma 3.4 we know that pr 1 belongs to F B. By our assumptions on T C and F B we know that i × Id U is in T C. Therefore there exists a morphism g : (W, f W ) × U ( U , p) → U × V that makes the two triangles commute. The commutativity of the lower triangle means that this is a morphism over U. Therefore adj −1 (g) is defined. Set f = adj −1 (g). It remains to check [15,Lemma 8.7(3)], this is equivalent to (i×Id U )•g = adj(f Z ) which is the commutativity of the upper triangle.
Lemma 3.7 Assume that U, V are fibrant and that p : U → U and r : Proof: By Lemmas 3.6 and 3.5 we know that I p (V ) is fibrant. Therefore it is sufficient to show that I p (r) has the right lifting property for T C. Consider a commutative square of the The lower right corner is an object over U through the morphism p△pr 1 . Let This square commutes. Indeed, where the first equality is by [15,Lemma 8.7(1)] and the third by [15,Lemma 8.7(3)]. By Lemmas 3.4 and 3.5 we know that Id U ×r is in F B. By our assumption (3) on F B and T C we know that i×Id U is in T C. Therefore, there exists a morphism g : (W, p W )× U ( U, p) → U ×V ′ that splits this square into two commutative triangles. Since the lower triangle commutes, g is a morphism over U and in particular g = adj(f ) for some f : Let us show that f splits the square (12) into two commutative triangles i.e. that we have The first equality is equivalent to which is the commutativity of the upper of the two triangles into which g splits (13).
The second equality is equivalent to which is the commutativity of the lower of the two triangles into which g splits (13).
Lemma is proved.
We can now prove the second main theorem of this section.
Theorem 3.8 Let (C, p, pt) be a universe category, let C be given a locally cartesian closed structure and let T C and F B be two collections of morphisms in C that satisfy Conditions 3.3. Let further Eq : ( U ; p) → U and Ω : U → U be a J1-structure and assume that the following conditions hold: Then there exists a J-structure Jp extending (Eq, Ω).
Proof: Let us use the notations of Problem 2.9. We need to show that under the assumptions of the current theorem there exists a morphism that splits the square of Problem 2.9 into two commutative triangles. Observe first that constructing such a splitting is equivalent to constructing the splitting of the square are permutations of the factors.
It is easy to show that U × U is fibrant. Therefore it is sufficient to show that Id U × p is in F B and ω × U Id F p is in T C. The first fact follows from the assumption that p is in F B and that U is fibrant. The obtain the second fact let us apply condition (3) on the classes F B and T C to B = U, f = pE U , i = ω and p = pF p. It remains to show that pF p is in F B.
We can represent pF p as the composition The morphism pE U is in F B as a composition of pull-backs of p with respect to morphisms with fibrant domains through repeated application of Lemmas 3.4 and 3.5. Therefore, the morphism prI pE U is in F B by Lemma 3.6 and as a corollary we know that I pE U (U) is fibrant. Similarly I p (U) is fibrant and i p (p) is in F B and applying again Lemma 3.4 we see that pr 1 is in F B. And again by Lemma 3.5 we see that pF p is in F B which finishes the proof of the theorem.
Corollary 3.9 Let C be a locally cartesian closed category with a Quillen model structure, p a universe in C and (Eq, Ω) a J1-structure on p. Assume further that p is a fibration and ω is a trivial cofibration and that in addition one of the following two conditions holds: 1. consider morphisms f : B ′ → B, p 1 : E 1 → B, p 2 : E 2 → B and i : E 1 → E 2 such that p 1 , p 2 are fibrations and i a trivial cofibration. Then the morphism is a trivial cofibration,

U is fibrant and the pull-back of a trivial cofibration along a fibration is a trivial cofibration.
Then (Eq, ω) can be extended to a full J-structure on p.
The following result can be used to produce many examples of universes with J-structures (but not the univalent universes). Let C be a locally cartesian closed category with coproducts of sequences ∐ n∈N X n . We let in n : X n → ∐ n X n and f n n : ∐ n X n → Y denote the canonical morphisms. We let ∐f n : ∐ n X n ∐ n Y n denote the morphism f n • in n n .
Assume that these coproducts satisfy the following two conditions: 1. for a sequence of morphisms f n : E n → B n the square is a pull-back square, 2. for a sequence of morphisms f n : E n → B n the square is a pull-back square. 1. the coproduct of a sequence of morphisms from T C is in T C and the coproduct of a sequence of morphisms from F B is in F B,

the composition of a morphism from T C with an isomorphism is in T C,
3. for any morphism f : X → Y there is given an object P (f ) and morphisms i f : To construct, for any universe p : U → U such that p ∈ F B a sequence of morphisms p n : U n → U n such that p 0 = p, p n ∈ F B and ∐ n p, with the universe structure defined by the fiber squares of C, has a J-structure with ω ∈ T C.
Construction 3.11 Define p n : U n → U n inductively as follows. For n = 0 we take p 0 = p. To define p n+1 consider the diagonal ∆ n : U n → ( U n , p n ) × Un ( U n , p n ) and let p n+1 = q ∆n : P (∆ n ) → ( U n , p n ) × Un ( U n , p n ) so that in particular U n+1 = ( U n , p n ) × Un ( U n , p n ).
Let U * = ∐ n U n , U * = ∐ n U n and p * = ∐ n p n . According to the first of the two properties that we required from the coproducts the canonical morphism is an isomorphism. Together with the second property applied to the right-most square this gives us a diagram with pull-back squares of the form: where r = ∐ n p n+1 . Define Eq as the composition of the lower horizontal arrows of this diagram (up to an isomorphism this is just in n+1 n ). Since the squares of the diagram are pull-back the natural morphism 4 Constructing a J-structure on CC(C, p) from a J-structure on p The construction of a C-system CC(C, p) from a category with a universe p and a final object pt was presented in [13] and summarized in [15]. Let us recall some facts and notations. The underlying category of CC(C, p) is equipped with a functor int to C. Note that while int is the identity on morphisms by construction of CC(C, p), the notations for the same element of Hom(Γ ′ , Γ) and Hom(int(Γ ′ ), int(Γ)) may differ. In particular for f : For each Γ ∈ Ob(CC(C, p)) we have natural bijections where u −1 1 (F ) = (Γ, F ) and where In particular, i.e., with respect to these bijections the function ∂ : Ob 1 (Γ) → Ob 1 (Γ) is given by composition with p : U → U.
We set: We let IdT Eq denote the J0-structure on CC(C, p) constructed from Eq in Construction 4.2.

Lemma 4.3 Let
Eq be a J0-structure on p. Let Γ ∈ Ob and F : int(Γ) → U. Then one has: Proof: Let T = (Γ, F ). We have:    Proof: We have On the other hand, by definition of ref l Ω , Proof: In view of Lemma 4.3, both rf T and F * (ω) are morphisms from (int(Γ); F ) to (int(Γ); F ) E . Let us denote int(Γ) by X and (int(Γ); F, Q(F ) • p) by Y . We have and we can see this object as a part of the diagram with two pull-back squares: The morphism rf T is defined in (4) as where the second equation is from (14). We have On the other hand Therefore by Lemma 4.6 we have We have rf T • v = δ(T ) because the square (3) commutes. Both rf T • v and F * (ω) • v are morphisms int(T ) → int(p * T (T )). Since p * T (T ) is a part of a pull-back square with the projections being p p * T (T ) and Q(Q(F ) • p) we need to check that which holds by a simple computation, and For this equality we need to verify two further equalities The second one is the second equality of the two that define F * (ω). For the first one we have This completes the proof of Lemma 4.7.
Problem 4.8 Let (Eq, Ω, Jp) be a J-structure on a universe p. To construct for all Γ ∈ Ob = Ob(CC(C, p)), for all T ∈ Ob 1 (Γ), for all P ∈ Ob 1 (IdxT (T )), for all s0 ∈ Ob(rf * T (P )), an element J(Γ, T, P, s0) of Ob(P ). Let us show first that where the first equality is from Lemma 2.3, the second from Lemma 4.7, the third from the commutativity of the canonical square and the fact that s0 is a section, the fourth from (17) and the fifth from naturality of η p,X,V in V .
Therefore the pair (η pE U (F, G), η p (F, H)) gives us a morphism  is given by the pair of morphisms (η pE U (u 1,Γ (T ), u 1,IdxT (T ) (P )), η p (u 1,Γ (T ), u 1,Γ (s0))). Proof: Let X := int(Γ) and X ′ := int(Γ ′ ). By definition, Q(f, F ) E is the unique morphism such that We will be building the proof using the following diagram By construction that is seen on this diagram we have: Therefore, the first equation that we need to verify is By [15,Lemma 3.2] we have, together with the defining rule Q(a, A) • Q(A) = Q(a • A), also the rule: Applying it twice and then the defining rule we get: which gives us the first equation. The second equation is immediate from the commutativity of the three squares that define q3. Proof: Let us write J for J Jp (Γ, T, P, s0) and J ′ for J Jp (Γ ′ , f * (T ), f * (P ), f * (s0)) and use the notations of Construction 4.9.
Recall that for f : Γ ′ → Γ the operation f * is defined only on Ob 1 (Γ). In all other uses it is an abbreviation for operations such as X → f * (X, i) and s → f * (s, i) for various i (see [16]). In particular, (19) is an abbreviation for We have: By naturality of η with respect to the first argument we have Therefore, by Lemma 4.11 we have Since both η pE U and u 1 are bijections and in particular injections it is sufficient to show that Since both φ expressions are morphism into a product this amounts to two equations that, taking into account the definition of φ in Construction 4.9 are: The first equality follows naturality of η and Lemma 4.11. The second equality follows from naturality of η. This finished the proof of Lemma 4.12.

Functoriality of the J-structures 1 A theorem about functors between categories with two universes
Before we can formulate the definition of what it means for a universe category functor to be compatible with J-structures we need some general results about functors between categories with two universes that we will later apply to the universes p : U → U and pE U : E U → U in a locally cartesian closed category C.
Given two universes (p, p X,F , Q(F )) and (p ′ , p ′ X,F , Q(F ) ′ ) where p : U → U and p ′ : U ′ → U and the canonical squares are of the form Note that F * (f ) depends on the universe structures on p and p ′ . Even when two universe structures give the same choices of the objects (X; F ) and (X; F ) ′ the difference in the choice of some of the morphisms, e.g., Q(F ) will affect morphisms F * (f ). We will need the following lemma about these morphisms. For We let Q ′ (−) and Q ′ (−, −) denote the morphisms Q(−) and Q(−, −) relative to the universe p ′ .
→ U be two morphisms. Then the square

commutes.
Proof: Since (X; F ) is a fiber product relative to the projections p X,F and Q(F ) it is sufficient to verify that which easily follows from the defining equations for Q(−, −) and (−) * .
Let (C, p, pt), (C ′ , p ′ , pt ′ ) be two universe categories such that C and C ′ are equipped with locally cartesian closed structures. In [15,Construction 5.6] we have defined, for any universe category functor Φ = (Φ, φ, φ) : (C, p, pt) → (C ′ , p ′ , pt ′ ) and any V ∈ C, a morphism We now need to consider the case when we have the following collection of data: 1. two universes p 1 , p 2 in C with the common codomain U and a morphism g : U 1 → U 2 over U, 2. two universes p ′ 1 , p ′ 2 in C ′ with the common codomain U ′ and a morphism g ′ : and this data is such that: 2. the triples Φ i := (Φ, φ, φ i ), i = 1, 2 are universe category functors i.e. Φ takes canonical squares of p 1 and p 2 to pull-back squares and the squares Let us denote the exchange morphisms by χ i (V ). The maps Φ 2 i in the following lemma are constructed in [15,Construction 5.2].

Lemma 1.2 Under the previous assumptions and notations the squares
On the other hand For which it is sufficient to check that The codomain of both morphisms is Φ((X; F 1 ) p 2 ) and since Φ takes canonical squares based on p 2 to pull-back squares it is sufficient to check that where the first equality is from the definition of ι in [15,Construction 5.2] and the second from (20). On the other hand This proofs the first equation. For the second equation we have: This finishes the proof of the lemma.

Lemma 1.3 Under the previous assumptions and notations the squares
Proof: Let X = I p 2 (V ). We have by definition of χ in [15,Construction 5.6]. Then by Lemma 2.3 and Lemma 1.2 we have: ))) Then, again by Lemma 2.3, we have It remains to show that η(Φ 2 1 (η −1 (I g (V )))) = Φ(I g (V )) • χ 1 (V ) Let a be any element of Hom(I p 2 (V ), I p 1 (V )). Let us show that ))) where the second equality holds because of naturality of η in the first argument. Then by [15,Lemma 5.4] and again by naturality of η in the first argument. This finishes the proof of Lemma 1.3.

Consider the morphisms
given by ζ i = χ i (U) • I p i (φ) and given by ζ i = χ i ( U 1 ) • I p i ( φ 1 ). Note that where ξ are the morphisms introduced in [15] and Theorem 1.4 Under the previous assumptions and notations the morphisms ζ 1 , ζ 2 , ζ 1 , ζ 2 form a morphism from the square to the square Proof: We need to prove commutativity of the outer squares of the following four diagrams: The left squares in the first and the second diagram are commutative by Lemma 1.3.
The left squares in the third and the fourth diagram are commutative by [15,Lemma 5.7].
The right hand side squares in the first and second diagram commute by Lemma 2.2.
The right hand side squares of the third and the fourth diagram commute because I p ′ i are functorial and therefore take commutative squares to commutative squares.
Theorem is proved.

Universe category functors compatible with J-structures
Let us define now conditions on functors of universe categories that reflect the idea of compatibility with the J0-J1-and J2-structures on the universes. Recall that for universe categories (C, p, pt), (C ′ , p ′ , pt ′ ) a functor of universe categories is a triple (Φ, φ, φ) where Φ : C → C ′ is a functor that takes the canonical squares to pull-back squares and pt to a final object and is a pull-back square. For any functor of universe categories and X ∈ C, F : is an isomorphism and we will denote it Φ X,F . Let Φ U p be the composition We also have another description of this morphism given by the following lemma.
Lemma 2.1 One has: where the second equality is by definition of Q ′ (−, −) and the third equality is by definition of Φ U ,p . Then where again the second equality is by definition of Q(−, −) and the fourth equality is by definition of Φ U ,p .
The particular case of ∆ follows from the fact that ∆ = Id U * Id U .
Proof: This square is equal to the composition of two squares The right hand side square is a pull-back square (5). The left hand side square is a pullback square as a commutative square whose sides are isomorphisms. We conclude that the composition of these two squares is a pull-back square.

Definition 2.4 Let
Eq be a J0-structure on p and Eq ′ a J0-structure on p ′ . A universe category functor (Φ, φ, φ) is said to be compatible with Eq and Eq ′ if the square commutes.
Let Eq, Eq ′ be as above. Let (Φ, φ, φ) be a universe functor compatible with Eq, and Eq ′ . Define a morphism Lemma 2.5 Let Eq, Eq ′ be as above. Let (Φ, φ, φ) be a universe functor compatible with Eq, and Eq ′ . Then the square is a pull-back square.
Proof: Consider the diagram The outer square of this diagram is equal to the outer square of the diagram where the equality of the lower horizontal arrows follows from the commutativity of the square (23). The left hand side square of this diagram is a pull-back square because Φ takes canonical squares to pull-back squares. The right hand side square is a pull-back square by definition of a functor of universe categories. Therefore the outer square is a pull-back square. The right hand side square of (24) is a canonical square and therefore a pull-back square. We conclude that the left hand square of (24) is a pull-back square.
Lemma 2.6 Let Eq, Eq ′ be as above. Let (Φ, φ, φ) be a functor of universe categories compatible with Eq, and Eq ′ . Then the square is a pull-back square.
Proof: It follows from the fact that the square (26) is equal to the vertical composition of the squares of Lemmas 2.5 and 2.3 with the square (22).

Definition 2.7 Let
Eq, Eq ′ be as above and let Ω, Ω ′ be J1-structures over Eq and Eq ′ respectively. A universe category functor (Φ, φ, φ) is said to be compatible with Ω and Ω ′ if the square Lemma 2.8 Let Eq, Ω and Eq ′ , Ω ′ be as above and let Φ be a universe category functor compatible with Eq, Eq ′ and Ω, Ω ′ . Then the square

commutes.
Proof: Since E U ′ = (( U ′ ; p ′ ); Eq ′ ) it is sufficient to verify that the compositions of the two paths in the square with p ( U ′ ;p ′ ),Eq ′ and Q(Eq ′ ) coincide. We have: where the first equation holds by definition of φ E . The proof follows now from the assumption that Φ is compatible with Ω and Ω ′ .
To formulate the condition of compatibility of a universe functor with full J-structures on C and C ′ we will use Theorem 1.4.
Let Φ = (Φ, φ, φ) be a functor of universe categories. In view of Lemma 2.6, if Φ is compatible with Eq and Eq ′ then the triple Φ E := (Φ, φ, φ E ) is a functor of universe categories as well.
If, in addition, Φ is compatible with Ω and Ω ′ then, by Lemma 2.8, morphisms ω and ω ′ satisfy the conditions on morphisms g and g ′ of Section 1. Let be given by the compositions Applying Theorem 1.4 in this context we get the following.
Theorem 2.9 Let Φ be a functor of universe categories compatible with the J1-structures (Eq, Ω) and (Eq ′ , Ω ′ ) on p and p ′ respectively. Then the morphisms ξ Φ , ξ Φ , ζ Φ , ζ Φ form a morphism from the square to the square where the second arrow is defined by ξ Φ , ξ Φ and ζ Φ in view of Theorem 2.9. and ψ (Γ,F ) is the unique morphisms int ′ (H(Γ, F )) → Φ(int(Γ, F )) such that and Observe that ψ Γ is automatically an isomorphism. The action of H on morphisms is given, 1 Let Φ be a universe category functor as above that is compatible with the J0structures Eq and Eq ′ on p and p ′ respectively. Then the homomorphism of C-systems H = H(Φ) is a homomorphism of C-systems with J0-structures relative to IdT Eq and IdT Eq ′ .
Proof: We will only consider the second assertion. The proof of the first one is similar and simpler.
To prove that the pair (u ′ 1,H(Γ) (H(T )), u ′ 1,IdxT ′ (H(T )) (H(o))) is a well defined element of D pE U ′ (Φ(int(Γ)), U ′ ) we need to show that f t(∂(H(o))) = IdxT ′ (H(T )) and that the source of u ′ 1,IdxT ′ (H(T )) (H(o))) equals to (int(H(Γ)); u ′ 1 (H(T ))) E , i.e., that The former is a corollary of our assumptions and Lemma 4.1 and the latter is a corollary of Let X = int(Γ), F = u 1,Γ (T ) and G = u 1,Idx(T ) (o). By definitions we have is the unique morphism such that On the other hand  1,2)]. Therefore, to prove the lemma it is sufficient to show that Both sides are morphisms with the codomain Φ(int(IdxT (T ))) = Φ((X; F ) E ) and since Φ E is a universe category functor it is sufficient to show that the compositions of the two sides with Φ(p E X,F ) and Φ(Q(F ) E ) • φ E are the same. Since and since Equation (27)  We have Therefore (28) is equivalent to two equations: and The first equality we will have to decompose further into two using the fact that by Lemma 2.1 we have Φ U p = (Φ(p U ,p ) • φ) * (Φ(Q(p)) • φ) Therefore (29) is equivalent to two equations and To prove (30) observe first two useful equalities where the first follows from the proof of Lemma 4.3 and the second is the combination of the first with the third equality of the same lemma. Now we have: ψ IdxT (T ) •Φ(Q(u 1 (IdxT (T ))))• φ = Q ′ (ψ IdxT (T ) •Φ(u 1 (IdxT (T )))•φ) = Q(u 1 (H(IdxT (T )))) and (H(T ))) E ′ • Q(Eq ′ ) = Q ′ (u 1 (H(IdxT (T )))) The equality (30) is proved.