Dependencies

From \(\mathbb {C}\) a small category and \(F : \mathbb {C}\to \mathbf{cat}\) a functor, we construct a small category \(\int F\). For any \(c\) in \(\mathbb {C}\) we refer to \(F c\) as the fiber over \(c\). The objects of \(\int F\) consist of pairs \((c \in \mathbb {C}, x \in F c)\), and morphisms between \((c, x)\) and \((d, y)\) are pairs \((f : c \to d, \phi : F \, f \, x \to y)\). This makes the following pullback in \(\mathbf{Cat}\)

Define the operation of evaluation \(\mathsf{ev}_{\alpha } \, B\) to take \(\alpha : \Gamma \to \mathbf{grpd}_\bullet \) and \(B : \Gamma \cdot U \circ \alpha \to \mathbf{grpd}\) and return \(\mathsf{ev}_{\alpha } \, B : \Gamma \to \mathbf{grpd}\), described below.

where we write \(A := U \circ \alpha \) and treat a map \(\Gamma \to \mathbf{grpd}\) as the same as a map \(\Gamma \to \mathsf{Ty}\).

More concisely, evaluation is a natural transformation \(\mathsf{ev}_{} \, : R \to \mathsf{Ty}\), given by

Let \(p : \mathbb {C}_{1} \to \mathbb {C}_{0}\) be a functor. We say \(p\) is a split Grothendieck fibration if we have a dependent function \(\mathsf{lift} \, a \, f\) satisfying the following: for any object \(a\) in \(\mathbb {C}_{1}\) and morphism \(f : p \, a \to y\) in the base \(\mathbb {C}_{0}\) we have \(\mathsf{lift} \, a \, f : a \to b\) in \(\mathbb {C}_{1}\) such that \(p (\mathsf{lift} \, a \, f) = f\) and moreover \(\mathsf{lift} \, a \, g \circ f = \mathsf{lift} \, b \, g \circ \mathsf{lift} \, a \, f\)

In particular, we are interested in split Grothendieck fibrations of groupoids, which are the same as isofibrations (replace all the morphisms with isomorphisms in the definition).

Unless specified otherwise, by a fibration we will mean a split Grothendieck fibration of groupoids. Let us denote the category of fibrations over a groupoid \(\Gamma \) as \(\mathsf{Fib}_{\Gamma }\), which is a full subcategory of the slice \(\mathbf{grpd}/ \Gamma \). We will decorate an arrow with \(\twoheadrightarrow \) to indicate it is a fibration.

Let \(\Gamma \) be a groupoid and \(A : \Gamma \to \mathbf{grpd}\) a functor, we can compose \(F\) with the inclusion \(i : \mathbf{grpd}\hookrightarrow \mathbf{Cat}\) and form the Grothendieck construction which we denote as

This is also a small groupoid since the underlying morphisms are pairs of morphisms from groupoids \(\Gamma \) and \(A x\) for \(x \in \Gamma \). Furthermore the pullback factors through (pointed) groupoids.

Let the interval groupoid \(\mathbb {I}\) be the small groupoid with two objects and a single non-identity isomorphism. There are two distinct morphisms \(\delta _{0}, \delta _{1} : \bullet \to \mathbb {I}\) and a natural isomorphism \(i : \delta _{0} \Rightarrow \delta _{1}\). Note that \(\delta _{0}\) and \(\delta _{1}\) both form adjoint equivalences with the unique map \(! : \mathbb {I}\to \bullet \).

Denote by \(\bullet +\bullet \) the small groupoid with two objects and only identity morphisms. Then let \(\partial : \bullet +\bullet \to \mathbb {I}\) be the unique map factoring \(\delta _{0}\) and \(\delta _{1}\).

We would like to define a natural transformation in \(\mathbf{Psh}(\mathbf{grpd})\)

with representable fibers.

Consider the functor that forgets the point

If we apply the Yoneda embedding \(\mathsf{y}: \mathbf{Cat}\to \mathbf{Psh}(\mathbf{Cat})\) to \(U\) we obtain

Since any small groupoid is also a large category \(i : \mathbf{grpd}\hookrightarrow \mathbf{Cat}\), we can restrict \(\mathbf{Cat}\) indexed presheaves to be \(\mathbf{grpd}\) indexed presheaves (this the nerve in \(i_{!} \dashv \mathsf{res}\)). We define \(\mathsf{tp}: \mathsf{Tm}\to \mathsf{Ty}\) as the image of \(U \circ \) under this restriction.

Note that \(\mathsf{Tm}\) and \(\mathsf{Ty}\) are not representable in \(\mathbf{Psh}(\mathbf{grpd})\).

Let \(\mathsf{U}\) be the (large) groupoid of small sets, i.e. let \(\mathsf{U}\) have \(\mathbf{set}\) as its objects and morphisms between two small sets as all the bijections between them. This gives us \(\ulcorner \mathsf{U}\urcorner : \bullet \to \mathsf{Ty}\).

Then we define \(\mathsf{El}: \mathsf{y}\mathsf{U}\to \mathsf{Ty}\) by defining \(\mathsf{El}: \mathsf{U}\to \mathbf{Grpd}\) as the inclusion - any small set can be regarded as a large discrete groupoid.

Then we take \(\pi := \mathsf{disp}_{\mathsf{El}}\), giving us

We can compute the groupoid \(E\) as that with objects that are pairs \((X,x)\) where \(x \in X \in \mathbf{set}\), and morphisms

Then \(\pi : E \to U\) is the forgetful functor \((X,x) \mapsto X\).

To define the commutative square in \(\mathbf{Psh}(\mathbf{grpd})\)

We first note that both \(\delta \) and \(\mathsf{tp}\) in the are in the essential image of the composition from 4.1.2

since the composition preserves pullbacks. So we first define in \(\mathbf{Cat}\)

\begin{equation} \label{eq:IdDiagram1} \end{equation}

1

Then obtain \(\mathsf{Id}\) and \(\mathsf{refl}\) in \(\mathbf{Psh}(\mathbf{grpd})\) by applying \(\mathsf{res} \circ \mathsf{y}\) to this diagram.

To this end, let \(\mathsf{Id}' : U \times _{\mathbf{grpd}} U \to \mathbf{grpd}\) act on objects by taking the set - the discrete groupoid - of isomorphisms

and on morphisms \((f, \phi _{0}, \phi _{1}) : (A, a_{0}, a_{1}) \to (B, b_{0}, b_{1})\) by

Let \(\mathsf{refl}' : \mathbf{grpd}_\bullet \to \mathbf{grpd}_\bullet \) act on objects by

and on morphisms \((f, \phi ) : (A, a) \to (B, b)\) by

where the second component has to be the identity on the object \(\mathsf{id}_{d}\), since \(B(b,b)\) is a discrete groupoid. So we need a merely propositional proof that the two maps are equal, which in this case is clear.

We want to define \(J : T \to P_{q}{\mathsf{Tm}}\)

for some \(\gamma : \Gamma \cdot A \cdot A \cdot \mathsf{Id}\to \mathbf{grpd}_\bullet \) which we will define below. We first use \(T\) 4.5.4 to describe the given data:

Let us name the fibers over the diagonal

and its given points

(Note that \(c_{\mathsf{refl}}\) is not a functor, but will give us an object per object \((x, a)\), and morphism \(c_{\mathsf{refl}}(f, \phi ) : C_{\mathsf{refl}}(f,\phi ) c_{\mathsf{refl}}(x, a) \to c_{\mathsf{refl}} (y, b)\) per morphism \((f, \phi )\).) Then \(\gamma \) will be defined by using \(C\) to lift the path

that starts on the diagonal, to give us a point in any fiber, using \(c_{\mathsf{refl}}\). Note that we unfolded \(\Gamma \cdot A \cdot A \cdot \mathsf{Id}\) as the domain of the nested display maps so that \(x \in \Gamma \), \(a_{0} \in A x\),

and

We also check \((\mathsf{id}_{x},\mathsf{id}_{a_{0}},h, \_ )\) is a path in \(\Gamma \cdot A \cdot A \cdot \mathsf{Id}\) by proving “\(\_ \)”, the omitted equality

So we define \(\gamma : \Gamma \cdot A \cdot A \cdot \mathsf{Id}\to \mathbf{grpd}_\bullet \) on objects by

noting that from the computation of \(\rho '\) given in 4.5.2 it follows that

Define \(\gamma \) on morphism \((f, \phi _{0}, \phi _{1}, \phi _{1} \circ A f h \circ \phi _{0}^{-1} = k) : (x, a_{0}, a_{1}, h) \to (y, b_{0}, b_{1}, k)\) by

We type check \(C(\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k, \_ ) \, c_{\mathsf{refl}}(f, \phi _{0})\)

We define the natural transformation \(\Pi : P_{\mathsf{tp}} \mathsf{Ty}\to \mathsf{Ty}\) as that which is induced (4.4.1) by the \(\Pi \)-former operation (4.2.8).

Then we define the natural transformation \(\lambda : P_{\mathsf{tp}} \mathsf{Ty}\to \mathsf{Ty}\) as the natural transformation induced by the following operation: given \(A : \Gamma \to \mathbf{grpd}\) and \(\beta : \Gamma \cdot A \to \mathbf{grpd}_\bullet \), \(\lambda _{A}\beta : \Gamma \to \mathbf{grpd}_\bullet \) will be the functor such that on objects \(x \in \Gamma \)

where \(B := U \circ \beta : \Gamma \cdot A \to \mathbf{grpd}\) and \(b (x , a)\) is the point in \(\beta (x , a)\). On morphisms \(f : x \to y\) in \(\Gamma \) we have

where \(\eta : \Pi _{A} B \, f \, s_{x} \to s_{y}\) is a natural isomorphism between functors \(A_{y} \to \Sigma _{A} B y\) given on objects \(a \in A_{y}\) by

These combine to give us a pullback square

We define the natural transformation

as that which is induced (4.4.1) by the \(\Sigma \)-former operation (4.2.8).

To define \(\mathsf{pair}: Q \to \mathsf{Tm}\), let \(\Gamma \) be a groupoid and \((\beta ,\alpha ,B) : \Gamma \to Q\) (such that \(U \circ \beta = \mathsf{ev}_{\alpha } \, \beta \)). We define a functor \(\mathsf{pair}_{\Gamma }(\beta ,\alpha ,B) : \Gamma \to \mathbf{grpd}_\bullet \) such that on objects \(x \in \Gamma \), the functor returns \((\Sigma _{A} B \, x, (a_{x}, b_{a_{x}}))\), where (using 4.4.5 \(U \circ \beta x = \mathsf{ev}_{\alpha } \, B x = B(x, a_{x})\))

and on morphisms \(f : x \to y\), the functor returns \((\Sigma _{A} B \, f, (\phi _{f}, \psi _{f}))\), where (using 4.4.5 \(U \circ \beta f = \mathsf{ev}_{\alpha } \, B f = B(f, \phi _{f})\))

\(\Sigma \) and \(\mathsf{pair}\) combine to give us a pullback square

Given \(A : \Gamma \to \mathbf{grpd}\) and \(B : \Gamma \cdot A \to \mathbf{grpd}\) we will define \(\Pi _{A} B : \Gamma \to \mathbf{grpd}\) such that for any \(C : \Gamma \to \mathbf{grpd}\) we have an isomorphism

natural in both \(B\) and \(C\).

Recall the following definition of composition of polynomial endofunctors, specialized to our situation

By the universal property of pullbacks, the data of a map with representable domain \(\varepsilon : \Gamma \to Q\) corresponds to the data of a triple of maps \(\alpha , \beta : \Gamma \to \mathsf{Tm}\) and \((A,B) : \Gamma \to P_{\mathsf{tp}} \mathsf{Ty}\) such that \(\mathsf{tp}\circ \beta = \pi _{\mathsf{Ty}} \circ \, \mathsf{counit} \, \circ (\alpha , B)\) and \(A = \mathsf{tp}\circ \alpha \).

This in turn corresponds to three functors \(\alpha , \beta : \Gamma \to \mathbf{grpd}_\bullet \) and \(B : \Gamma \cdot U \circ \alpha \to \mathbf{grpd}\), such that \(U \circ \beta = \mathsf{ev}_{\alpha } \, B\). So we will write

gray Type theoretically \(\alpha = (A , a : A)\) and \(\mathsf{ev}_{\alpha } \, B = B a\) and \(\beta = (B a, b : B a)\). Then composing \(\varepsilon \) with \(\mathsf{tp}\lhd \mathsf{tp}\) returns \(\gamma \), which consists of \((A, B)\). It is in this sense that \(Q\) classifies pairs of dependent terms, and \(\mathsf{tp}\lhd \mathsf{tp}\) extracts the underlying types.

Precomposition with a substitution \(\sigma : \Delta \to \Gamma \) acts on this triple by

Then given \(A : \Gamma \to \mathbf{grpd}\) and \(B : \Gamma \cdot A \to \mathbf{grpd}\) we define \(\Sigma _{A}B : \Gamma \to \mathbf{grpd}\) such that \(\Sigma _{A}B\) acts on objects by forming fiberwise Grothendieck constructions

where \(x_{A} : A(x) \to \Gamma \cdot A\) takes \(f : a_{0} \to a_{1}\) to \((\mathsf{id}_{x},f) : (x,a_{0}) \to (x,a_{1})\)

\(\Sigma _{A}B\) acts on morphism \(f : x \to y\) in \(\Gamma \) and \((a \in A(x), b \in B(x,a))\) by

and for morphism \((\alpha : a_{0} \to a_{1} \in A(x),\beta : B \, (\mathsf{id}_{x},\alpha ) \, b_{0} \to b_{1} \in B(x,a_{1}))\) in \(\Sigma _{A}B \, x\)

Let us also define the natural transformation \(\mathsf{fst}: \Sigma _{A}B \to A\) by

The identity function \(\mathsf{id}_{A} : \Gamma \to \mathsf{Tm}\) of type \(\mathsf{Exp}\circ (A,A) : \Gamma \to \mathsf{Ty}\) can be defined by the following

Viewed as a map between the display maps, this is simply the identity \(\Gamma \cdot A \to \Gamma \cdot A\).

Composition is also simplest when viewed as an operation on maps between fibers. Given \(f : \mathsf{disp}_{A} \to \mathsf{disp}_{B}\) and \(g : \mathsf{disp}_{B} \to \mathsf{disp}_{C}\), the composition is \(g \circ f : \mathsf{disp}_{A} \to \mathsf{disp}_{C}\).

Following Awodey [ Awo17 ] , we say that a map \(\mathsf{tp}: \mathsf{Tm}\to \mathsf{Ty}\) in \(\mathbf{Psh}(\mathbb {C})\) is fiberwise representable or a natural model when any fiber of a representable is representable. In other words, given any \(\Gamma \in \mathbb {C}\) and a map \(A : \mathsf{y}(\Gamma ) \to \mathsf{Ty}\), there is some representable \(\Gamma \cdot A \in \mathbb {C}\) and maps \(\mathsf{disp}_{A} : \Gamma \cdot A \to \Gamma \) and \(\mathsf{var}_{A} : \mathsf{y}(\Gamma \cdot A) \to \mathsf{Tm}\) forming a pullback

The first option is fully extensional identity types, i.e. those satisfying equality reflection and uniqueness of identity proofs (UIP). Equality reflection says that if one can construct a term satisfying \(\mathsf{Id}(a,b)\) then we have that definitionally \(a \equiv b\), i.e. they are equal morphisms in the natural model. This amounts to just requiring that 3 is a pullback, i.e. \(\rho \) is an isomorphism

Note that this means \({\rho }^{\star }\) is an isomorphism, from which it follows that 4 is also a pullback, i.e. \(\varepsilon \) is an isomorphism.

Suppose \(\mathsf{tp}: \mathsf{Tm}\to \mathsf{Ty}\) is a natural model and we have a commutative square (this need not be a pullback)

\begin{equation} \label{eq:Id} \end{equation}

3

where \(\delta \) is the diagonal:

Then let \(I\) be the pullback. We get a comparison map \(\rho \)

Then view \(\rho : \mathsf{tp}\to q\) as a map in the slice over \(\mathsf{Ty}\).

Now (by 5.0.8) applying \(P_{-} : (\mathbf{Psh}(\mathbb {C})/ \mathsf{Ty}) ^{\mathrm{op}} \to [\mathbf{Psh}(\mathbb {C}), \mathbf{Psh}(\mathbb {C})]\) to \(\rho : \mathsf{tp}\to q\) gives us a naturality square (this also need not be a pullback).

\begin{equation} \label{eq:JDefinition1} \end{equation}

4

Taking the pullback \(T\) and the comparison map \(\varepsilon \) we have

\begin{equation} \label{eq:JDefinition2} \end{equation}

5

Then a natural model \(\mathsf{tp}\) with identity types consists of a commutative square 3, with a section \(\mathsf{J}: T \to P_{q}{\mathsf{Tm}}\) of \(\varepsilon \).

Say an identity type in a natural model satisfies UIP if \(I \to \mathsf{tp}\times _{\mathsf{Ty}} \mathsf{tp}\) is a strict proposition, meaning for any \((a,b) : \Gamma \to \mathsf{tp}\times _{\mathsf{Ty}} \mathsf{tp}\) there it at most one lift

We will use \(P_{\mathsf{tp}_i}\) to denote the polynomial endofunctor 5.0.1 associated with a natural model \(\mathsf{tp}_i\). Then additional structure of \(\Pi \) types on our \(N\) universes consists of, for each \(i, j \le N\), a pullback square

\begin{equation} \label{eq:PiPullback} \end{equation}

1

A collection of \(N+1\) natural models with \(N\) Russell style universes and lifts consists of

• For each \(i \leq N\) a natural model \(\mathsf{tp}_i : \mathsf{Tm}_i \to \mathsf{Ty}_i\)

• For each \(i {\lt} N\) a lift \(\mathsf{L}_{i}^{i+1} : \mathsf{Ty}_i \to \mathsf{Ty}_{i+1}\)

• For each \(i {\lt} N\) a point \(\mathsf{U}_i : 1 \to \mathsf{Ty}_{i+1}\) such that

  

We will use the polynomial composition of two maps 5.0.6, \(\mathsf{tp}_i \lhd \mathsf{tp}_j : Q \to P_{\mathsf{tp}_i}(\mathsf{Ty}_j)\). Then additional structure of \(\Sigma \) types on our \(N\) universes consists of, for each \(i, j \le N\), a pullback square

\begin{equation} \label{eq:SiPullback} \end{equation}

2

Univalence for universe \(\mathsf{U}\) states that IdToEquiv itself is an equivalence

Note that this statement is large, i.e. not a type in the universe \(\mathsf{U}\).

We will take the category of pointed small categories \(\mathbf{cat}_\bullet \) to have objects as pairs \((\mathbb {C}\in \mathbf{cat}, c \in \mathbb {C})\) and morphisms as pairs

Then the category of pointed small groupoids \(\mathbf{grpd}_\bullet \) will be the full subcategory of objects \((\Gamma , c)\) with \(\Gamma \) a groupoid.

Let \(f : B \to A\) and \(g : D \to C\). Define the polynomial composition \(f \lhd g : Q \to P_{f}{C}\) as the composition of the two vertical maps in the following

Then the two functors

are naturally isomorphic.

In the natural model we can construct these by considering first the map

defined using the characterising property of polynomials 5.0.2, which we can visualize in

Then, respectively, the pullback of the diagrams 1 and 2 for interpreting \(\Pi \) and \(\Sigma \) rules along this map give us pullback diagrams for interpreting function types and product types. (We simplify the situation to where \(i = j\).)

Let \(\mathbb {C}\) be a locally Cartesian closed category (in our case, presheaves on the category of contexts). This means for each morphism \(t : B \to A\) we have an adjoint triple

where \(t^{*}\) is pullback, and \(t_{!}\) is composition with \(t\).

Let \(t : B \to A\) be a morphism in \(\mathbb {C}\). Then define \(P_{t} : \mathbb {C}\to \mathbb {C}\) be the composition

We can also view taking polynomial endofunctors as a covariant functor on the category of arrows with cartesian squares as morphisms

where the action on a cartesian square is

given by the whiskered natural transformations

Furthermore, the natural transformation \(P_{\kappa }\) is cartesian. meaning each naturality square is a pullback square.

The natural transformation \(P_{\kappa }\) computes in the following way

using the fact that \(\Gamma \cdot _{s} \alpha \) and \(\Gamma \cdot _{t} \theta \circ \alpha \) are limits of the same diagram.

Let \(\, \mathsf{counit} \, : \rho _B \to B \to B^* Y\) denote the counit of the adjunction \(f^* \dashv f_*\) at the object \(B^* Y\), recalling that \(\rho _B = t^* t_* B^* Y\). Then viewing the object \(B^* Y\) in the slice as the object \(Y \times B\) in the ambient category, we define \(\mathsf{ev}_{} \, : R \to Y\) as the composition

Let \(P_{-} : (\mathbb {C}/ A)^{\mathrm{op}} \to [\mathbb {C}, \mathbb {C}]\) be defined by taking \(s \mapsto P_{s}\) on objects and act on a morphism by

where

where \(\mu = \mu ^{*}\) is the mate from 5.0.7, and \(\eta \) is the natural isomorphism given by pullback pasting.

Pointwise, this natural transformation acts on a pair \((\alpha , \beta ) : \Gamma \to P_{t}{X}\) by

where \(\alpha ^{*} \rho \) is defined as

We prove this now.

\(X \in \mathbf{Psh}(\mathbf{grpd})\) be a presheaf. Let \(F\) be an operation that takes a groupoid \(\Gamma \), a functor \(A : \Gamma \to \mathbf{grpd}\) and \(B : \Gamma \cdot A \to X\) and returns a natural transformation \(F_{A} B : \Gamma \to X\).

Then using Yoneda to define \(\tilde{F} : P_{\mathsf{tp}} X \to X\) pointwise as

gives us a natural transformation if and only if \(F\) satisfies the strict Beck-Chevalley condition

for every \(\sigma : \Delta \to \Gamma \) in \(\mathbf{grpd}\).

We can then construct the pullback \(I'\)

as the groupoid with objects \((A, a_{0}, a_{1}, h)\) where \(A\) is a groupoid with \(a_{0}, a_{1} \in A\) and \(h : a_{0} \to a_{1}\), and morphisms

where \(f : A \to B\), \(\phi _{i} : f a_{i} \to b_{i}\) and \(A h = k\) represents a merely propositional proof of equality. Then we can also compute

Specialized to \(q : I \to \mathsf{Ty}\) in \(\mathbf{Psh}(\mathbf{grpd})\), the characterizing property of polynomial endofunctors 5.0.2 says that a map from a representable \(\varepsilon : \Gamma \to P_{q}X\) corresponds to the data of

where \(A = q \circ \varepsilon \) and

This is a specialization of 5.0.3. Use \(R\) to denote the fiber product

By the universal property of pullbacks, The data of a map from a representable \(\varepsilon : \Gamma \to R\) corresponds to the data of \(\alpha : \Gamma \to \mathsf{Tm}\) and \((U \circ \alpha ,B) : \Gamma \to P_{\mathsf{tp}}{\mathsf{Ty}}\). Then by 4.3.1 this corresponds to the data of \(\alpha : \Gamma \to \mathsf{Tm}\) and \(B : \Gamma \cdot U \circ \alpha \to \mathsf{Ty}\).

Precomposition by a substitution \(\sigma : \Delta \to \Gamma \) then acts on such a pair by

The data of a map \((A, C, \gamma _{\mathsf{refl}}) : \Gamma \to T\) corresponds to the data of

Then precomposition with \(\sigma : \Delta \to \Gamma \) acts on such a triple via

Use \(R\) to denote the fiber product

By the universal property of pullbacks and 5.0.2, The data of a map \(\Gamma \to R\) corresponds to the data of \(\beta : \Gamma \to B\) and \((t \circ \beta ,y) : \Gamma \to P_{t}{Y}\), or just \(\beta : \Gamma \to B\) and \(y : \Gamma \cdot t \circ \beta \to Y\)

By uniqueness in the universal property of pullbacks and 5.0.2, Precomposition by a map \(\sigma : \Delta \to \Gamma \) acts on such a pair by

Suppose \((\beta ,y) : \Gamma \to R\), as in 5.0.3

Then the evaluation of \(y\) at \(\beta \) can be computed as

where

and

Suppose

Then we have a mate \(\mu _{!} : \rho _{!} \circ s^{*} \Rightarrow t^{*}\). This is given by the universal property of pullbacks: given \(f : x \to y\) in the slice \(\mathbb {C}/ A\) we have

By the calculus of mates we also have a reversed mate between the right adjoints \(\mu ^{*} : t_{*} \to s_{*} \circ \rho ^{*}\). Explicitly \(\mu ^{*}\) is the composition

For any small groupoid \(\Gamma \) and \(A : \mathsf{y}\Gamma \to \mathsf{Ty}\), the pullback of \(\mathsf{tp}\) along \(A\) can be given by the representable map \(\mathsf{y}\mathsf{disp}_{A}\).

The functor \(\mathsf{ev}_{\alpha } \, B : \Gamma \to \mathbf{grpd}\) can be computed as

where

There is an adjoint equivalence

where for each fibration \(\delta : \Delta \to \Gamma \) and each object \(x \in \Gamma \)

It follows that all fibrations are pullbacks of the classifier \(U : \mathbf{grpd}_\bullet \to \mathbf{grpd}\), when viewed as morphisms in \(\mathbf{Cat}\).

The corresponding fact about fibrations is that the composition of two fibrations is a fibration.

We can deduce a corresponding fact about fibrations: since fibrations are closed under isomorphism, and since any pullback in \(\mathbf{grpd}\) of a fibration \(p\) is isomorphic to the display map \(\mathsf{disp}_{\mathsf{fiber}{p} \circ \sigma }\), any pullback of a fibration is a fibration.

Stated in terms of fibrations, we have

with the universal property of pushforward

natural in both \(\tau \) and \(\rho \).

We can compute \(\varepsilon : P_{q}{\mathsf{Tm}} \to T\) via

Let \(\sigma : \Delta \to \Gamma \) be a functor between groupoids. Since display maps are pullbacks of the classifier \(U : \mathbf{grpd}_\bullet \to \mathbf{grpd}\) we have the pasting diagram

This gives us a functor \(\circ \sigma : [\Gamma ,\mathbf{grpd}] \to [\Delta ,\mathbf{grpd}]\) which is our strict version of pullback.

\(J : T \to P_{q}{\mathsf{Tm}}\), as defined above is a section of \(\varepsilon \).

Let \(\bullet \) denote the terminal groupoid, namely that with a single object and morphism. Then the unique map \(\Gamma \to \bullet \) is a fibration.

Let \(A\) be a small groupoid. Recall that \(\mathbf{grpd}\) is Cartesian closed, so we can take the image of the above diagram under the functor \(A^{-}\).

Then the indicated morphisms are fibrations, and \(A^{\delta _{0}}, A^{\delta _{1}}\) form adjoint equivalences with \(A^{!} : A \to A^{\mathbb {I}}\).

Let \(\sigma : \Delta \to \Gamma \), \(A : \Gamma \to \mathbf{grpd}\) and \(B : \Gamma \cdot A \to \mathbf{grpd}\). Then

where \(\sigma _{A}\) is uniquely determined by the pullback in

Specialized to \(\mathsf{tp}: \mathsf{Tm}\to \mathsf{Ty}\) in \(\mathbf{Psh}(\mathbf{grpd})\), the characterizing property of polynomial endofunctors 5.0.2 says that a map from a representable \(\Gamma \to P_{\mathsf{tp}}X\) corresponds to the data of

The special case of when \(X\) is also \(\mathsf{Ty}\) gives us a classifier for dependent types; by Yoneda the above corresponds to the data in \(\mathbf{Cat}\) of

Furthermore, precomposition by a substitution \(\sigma : \Delta \to \Gamma \) acts on such a pair by

where \(\mathsf{tp}^{*} \sigma \) is given by

Let \(\sigma : \Delta \to \Gamma \), \(A : \Gamma \to \mathbf{grpd}\) and \(B : \Gamma \cdot A \to \mathbf{grpd}\). Then

where \(\sigma _{A}\) is uniquely determined by the pullback in

The data of a map into the polynomial applied to an object in \(\mathbb {C}\)

corresponds to

Applying the adjunction \(A_{!} \dashv A^{*}\), this corresponds to

Applying the adjunction \(t^{*} \dashv t_{*}\), this corresponds to

Henceforth we will write

for this map, since it is uniquely determined by this data. Furthermore, precomposition by \(\sigma : \Delta \to \Gamma \), acts on such a pair by

and given a morphism \(f : X \to Y\), the morphism \(P_{t}{f}\) acts on such a pair by

If we have

then the two possible ways of obtaining composing the covariant and contravariant actions of \(P_{-}\) form a (strictly commuting) pullback square in \([\mathbb {C}, \mathbb {C}]\).