Universes in categories In this file, we define the notion of universe within a category. These are Tarski-style universes, meaning that we have a map assigned to each term of the universe an actual type (instead of Russel style universes whose inhabitants are actual types). To define such universes, we first give their core ingredients. These are an object `U` and an map that assigns to each morphism into `U` a type. Concretely, this entails to

• an object `U`
• for all morphisms `t : Γ --> U`, a morphism `⌜ t ⌝ : El t --> Γ`

This data is given in cat_el_map. Next we express stability under substitution of the map `El`. To state that, we use that substitution is interpreted using pullback. More specifically, we express that certain squares are pullbacks. Suppose that we have morphisms `s : Δ --> Γ` and `t : Γ --> U`. Then we have the following

 El (s · t)         El t
     |                |
     |                |
     V                V
     Δ      ------>   Γ   -----> U
               s            t

To say that `El (s · t)` is the substitution of `El t` along `s`, we say that we have a morphism `sub_U s t : El (s · t) --> El t`, which makes the resulting square a pullback square. This is expressed in cat_el_map_stable. The final requirement is coherence of substitution. Specifically, we say how the morphism `sub_U s t` acts on the identity and composition of substitutions. The precise definition is given in is_coherent_cat_stable_el_map. All in all, we get a notion of universe in a category with finite limits, which is given in cat_stable_el_map_coherent. To construct a bicategory of categories with universes, we also define when functors and natural transformations preserve them. Suppose that we have a functor `F : C ⟶ D` and that `C` has a universe `U_1` and that `D` has as universe `U_2`. Then we say that `F` preserves the universe if we have

• an isomorphism `i : F U_1 ≅ U_2`
• for each `t : Γ --> U` in `C` we have an isomorphism `j : F (El_1 t) ≅ El_2 (F t · i)` such that the morphisms `F (El_1 t)` and `j · El_2 (F t · i)` are equal.

We also require that the functor `F` preserves the morphisms `sub_U s t : El (s · t) --> El t`. These requirements are expressed in the file `CatWithOb` (i.e., the morphism `i : F U_1 ≅ U_2`), and in the definitions functor_el_map and functor_stable_el_map. Finally, we define when a natural transformation preserves universes (see nat_trans_preserves_el). In this definition, we require that a certain diagram commutes. Content 1. The map assigning types to terms of the universe 2. Stability 3. Coherence 4. Preservation by functors 5. Identity and compositions preserve universes 6. Functors that preserve stable universes 7. The identity and composition 8. Preservation by natural transformations

1. The map assigning types to terms of the universe

2. Stability

3. Coherence

This lemma calculates the necessary transport for an equality principle

4. Preservation by functors

5. Identity and compositions preserve universes

6. Functors that preserve stable universes

7. The identity and composition

8. Preservation by natural transformations