From comprehension categories with a universe to categories with a universe Our goal is to define a pseudofunctor from the bicategory of (DFL, full, univalent) comprehension categories with a universe to the bicategory of univalent categories with finite limits and a universe. This is one of the necessary ingredients to extend the biequivalence between DFL full comprehension categories and categories with finite limits to universes. To construct the desired pseudofunctor, we construct a displayed pseudofunctor over the pseudofunctor from DFL comprehension categories to categories with finite limits maps. This pseudofunctor maps every DFL comprehension category to its category of contexts. As such. it suffices to show that whenever a comprehension category `χ : D ⟶ C^→` is equipped with a universe, then we can equip the category `C` of contexts with a universe type. Similarly, we must show that functors between DFL comprehension categories preserve universe types and that natural transformations satisfy a suitable coherence condition. To get insight in the construction, let's look at some details. A universe in the comprehension category `χ : D ⟶ C^→` gives us a type `u : ty ☐` in the empty context. By using the comprehension functor, we obtain a morphism `χ u : dom(χ u) --> ☐` to the empty context. The domain of this morphism is the universe object in `C`. The next important observation is that terms of type `u` in context `Γ` are the same as morphisms from `Γ` to `χ u` (note that, technically, we need to talk about a term of type `u [ ! ]` where `!` is the unique map from `Γ` to the empty context). To understand why, note that we have the following pullback square

    Γ & u [[ ! ]] -----> dom(χ u)
       |                   |
     π |                   | χ u
       |                   |
       V                   V
       Γ ---------------> []
           !

Terms of type `u [ ! ]` are sections of the projection `π` displayed in the diagram. As a result, terms of type `u [ ! ]` are the same as morphisms from `Γ` to `dom(χ u)`. This correspondence allows us to show that every morphism `Γ --> dom(χ u)` gives rise to a morphism to `Γ`. A morphism `Γ --> dom(χ u)` gives rise to a term `u [ ! ]` in context `Γ`, which gives rise to a type in context `Γ` and that type gives us a morphism to `Γ` via `χ`. The main technical work lies in establishing the necessary coherences. This file defines the actions on objects and 1-cells of the desired pseudofunctor. The construction has been split up so that the resulting files are smaller and so that they can be compiled concurrently. Contents 1. Action on objects 1.1. Construction of the universe object 1.2. Terms of the universe type versus morphisms 1.3. The type associated to a term of the universe 1.4. Calculational lemmas 1.5. Stability of the type associated to a term of the universe 1.6. Coherence of the stability isomorphisms 2. Action on 1-cells 2.1. Preservation of the universe object 2.2. Preservation of the associated type 2.3. Coherences

1. Action on objects

1.1. Construction of the universe object

1.2. Terms of the universe type versus morphisms

1.3. The type associated to a term of the universe

1.4. Calculational lemmas

Every morphism gives rise to a term. In the following lemma, we simplify how this acts on the composition of morphisms, and we relate it to substitution of terms.

1.5. Stability of the type associated to a term of the universe

1.6. Coherence of the stability isomorphisms

2. Action on 1-cells

2.1. Preservation of the universe object

2.2. Preservation of the associated type

2.3. Coherences