I don't have Bart Jacobs' book so I don't know for sure what the context is for this extract from it, but I suspect that it is the categorical semantics of a **type of types** or **universe** such as in Martin-Löf Type Theory. This is not treated by Mac Lane or Lambek and Scott but my own book *Practical Foundations of Mathematics* considers related material, though not Martin-Löf Type Theory.

A **fibration** is a way of presenting the manner in which a mathematical structure varies according to a certain parameter. The parameter is represented by the **base category** $\mathbb B$ and for each value $X\in\mathbb B$ the corresponding structure is the category ${\mathbb E}_X$, which is called the **fibre** over $X$. As $X$ "varies" along a morphism $f:Y\to X$, this structure is related by a functor $f^*:{\mathbb E}_X\to{\mathbb E}_Y$. In a fibration, all of these categories and functors are collected together into a single category $\mathbb E$ together with a functor $p:{\mathbb E}\to{\mathbb B}$ with certain properties. In this, the fibre ${\mathbb E}_X\subset{\mathbb E}$ consists of the objects and morphisms that $p$ takes to $X$ and ${\mathsf{id}}_X$. We say informally that these objects and morphisms **live** over $X$.

The clearest paradigm of the use of fibrations in categorical type theory is that of **types and predicates**. Then the **base category** consists of types and terms (more precisely, its objects are **contexts**, *ie* lists of typed variables, and its morphisms are lists of terms whose types correspond to the target context and whose free variables correspond to the source). The **fibre** over a particular context consists of the predicates in its variables. The **horizontal** or **prone** or **cartesian** lifting of a base morphism at a predicate has as source the **substituted** form of the predicate using the terms that make up the morphism.

What is a **generic predicate**? Since *any* predicate on *any* type can be a substituted form of it, the free variable of the generic predicate cannot be any *ordinary* type but must somehow say *what it is to be a predicate*. If you follow through the definition, you will see that, for a *strong* generic predicate, this type has to be the *subobject classifier* $\Omega$ of a topos, whilst a *weak* generic predicate is the type or kind $\mathbf{Prop}$ of propositions.

We can handle universes or types of types in a similar way. Now the variables in the base category denote *type-unknowns* and the fibre over a particular context (list of type variables) consists of the type-expressions and terms that are definable using that list of type variables. The **generic type** is a single type variable *qua* type-expression in the fibre over the context that consists of that single type vaiable. Analogously to the previous case, its type is $\mathbf{Type}$, the type of all types. However, this can only give a **weak** generic type.

In fact, $\mathbf{Type}$ cannot itself be a type if you want the terms to do ordinary mathematics, with equality and functions, although it can be if you're doing domain theory with fixed points. In the former setting, such as in Martin-Löf Type Theory or Homotopy Type Theory, a hierarchy of universes is introduced; this has a corresponding hierarchy of generic types.

Personally, I feel that fibrations obfuscate categorical type theory.

The naive way of doing this would be to use **indexed categories**, which are functors ${\mathbb B}\to{\mathbf{Cat}}^{\mathsf{op}}$. In the applications in pure mathematics, we get **pseudofunctors** instead, where we have to take account of isomorphisms and coherence thereof; this was the reason for using fibrations instead, as explained in a paper of Bénabou that is notorious for its personal language. In the applications to type theory, on the other hand, these isomorphisms are unnecessary because the syntax ensures functoriality.

A deeper objection to indexed categories is that the functors mix up internal and external notions and making sense of them in the usual foundational setting (sets or toposes) requires the **axiom-scheme of replacement**. Using fibrations avoids this and potentially allows us to understand replacement in the context of a topos (see the final pages of my book).

The categorical technology that I prefer to fibrations is that of a **category with a class of display maps**, which is set out in Chapter VIII of my book.

In the applications of fibrations to type theory, each fibre usually has a terminal object, with which we can identify the objects of the base category, and we just work in the **total category** of the fibration (its source *qua* functor). The **display maps** are the terminal projections in each fibre, from which we recover the fibration as the codomain.

In the paradigm of types and propositions above, an object of the total category is a list of types together with a predicate on them. We may think of this as a subset of a product of sets, or just a mono. A morphism is a commutative square, which is a **pullback** iff the morphism is prone (horizonatal, cartesian). A base object (context) consists of a list of types together with the true predicate, or a set considered as the entire subset of itself. The display map corresponding to a particular object (mono) is the square consisting of this mono on the vertical sides and identities on the horizontal sides, though more briefly we take it to be the mono.

We can think of the display map in terms of its fibres. In the case of a predicate on a single type (or subset of a set), the fibre over an element is the truth-value of the predicate at that element, where we think of a truth value as a subset of the singleton. The mono **displays** these truth values over the set in that the source of the display map is the disjoint union of these sub-singletons.

I leave it as an exercise to see why the map $\top:{\mathbf 1}\to\Omega$ in a topos is the display of all possible truth values over their names.

We can now understand a generic type in the same way. The target of the display map is the type $\mathbf{Type}$ of all types. The fibre over each element of $\mathbf{Type}$ (the *name* of a type) is the *extent* of that type, so the source of the display map is the disjoint union of all types.

I leave it as another exercise to see that, for a model $M$ of set theory, this display map is the global mebership relation, $\{(x,y):M^2|x\in y\}\to M$ by $(x,y)\mapsto y$.

I proposed the word **prone** in this subject because the notion has nothing to do with Descartes and the word **cartesian**, like **regular** and **normal**, is grossly over-used in mathematics. Morphisms of the total category that the fibration takes to identities have been called **vertical**. However, there are two ways in which morphisms can be orthogonal to vertical morphisms, whilst the English language conveniently provides two words for horizontal, namely *prone* (face up) and *supine* (face down).

particularsuch adjunction, but without giving it a name. $\endgroup$ – Mike Shulman Nov 18 '15 at 23:45