4 The Groupoid Model

In this chapter we construct a natural model in $\mathbf{Psh}(\mathbf{grpd})$ the presheaf category indexed by the category $\mathbf{grpd}$ of (small) groupoids. We will build the classifier for display maps in the style of Hofmann and Streicher [ HS98 ] and Awodey [ Awo23 ] . To interpret the type constructors, we will make use of the weak factorization system on $\mathbf{grpd}$ - which comes from restricting the “classical Quillen model structure” on $\mathbf{cat}$ [ Joy ] to $\mathbf{grpd}$.

4.1 Classifying display maps

Notation

We denote the category of small categories as $\mathbf{cat}$ and the large categories as $\mathbf{Cat}$. We denote the category of small groupoids as $\mathbf{grpd}$.

We are primarily working in the category of large presheaves indexed by the (large, locally small) category of small groupoids, which we will denote by

\[ \mathbf{Psh}(\mathbf{grpd})= [\mathbf{grpd}^{\mathrm{op}}, \mathbf{Set}] \]

In this section, $\mathsf{Tm}$ and $\mathsf{Ty}$ and so on will refer to the natural model semantics in this specific model.

Definition 4.1.1 Pointed

✓

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

\[ (F : \mathbb {C}_{1} \to \mathbb {C}_{0}, \phi : F c_{1} \to c_{0}) : (\mathbb {C}_{1}, c_{1}) \to (\mathbb {C}_{0}, c_{0}) \]

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

Definition 4.1.2 The display map classifier

✓

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

\[ \mathsf{tp}: \mathsf{Tm}\to \mathsf{Ty} \]

with representable fibers.

Consider the functor that forgets the point

\[ U : \mathbf{grpd}_\bullet \to \mathbf{grpd}\quad \quad \text{ in \quad $\mathbf{Cat}$. } \]

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

\[ U \circ : [ - , \mathbf{grpd}_\bullet ] \to [ - , \mathbf{grpd}] \quad \quad \text{ in \quad $\mathbf{Psh}(\mathbf{Cat})$. } \]

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.

$\begin{tikzcd} [row sep = tiny] \Cat & \PshCat & \Pshgrpd \\ \grpd & {[-,\grpd]} & \Type \arrow["\yo", from=1-1, to=1-2] \arrow["{\mathsf{res}}", from=1-2, to=1-3] \arrow[maps to, from=2-1, to=2-2] \arrow[maps to, from=2-2, to=2-3] \end{tikzcd}$

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

Remark 4.1.3

By Yoneda we can identify maps with representable domain into the type classifier

\[ A : \mathsf{y}\Gamma \to \mathsf{Ty}\quad \quad \text{ in } \quad \mathbf{Psh}(\mathbf{grpd}) \]

with functors

\[ A : \Gamma \to \mathbf{grpd}\quad \quad \text{ in } \quad \mathbf{Cat} \]

Definition 4.1.4 Grothendieck construction

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}$

$\begin{tikzcd} & {(c,x)} & {(Fc, x)} \\ {(c,x)} & {\int F} & \ptcat & {(C,c)} \\ c & \catC & \cat & C \\ & {} \arrow[maps to, from=1-2, to=1-3] \arrow[maps to, from=2-1, to=3-1] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow[from=2-3, to=3-3] \arrow[maps to, from=2-4, to=3-4] \arrow["F"', from=3-2, to=3-3] \end{tikzcd}$

Definition 4.1.5 Grothendieck construction for groupoids

✓

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

\[ \Gamma \cdot A := \int i \circ A \quad \quad \mathsf{disp}_{A} : \Gamma \cdot A \to \Gamma \]

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.

$\begin{tikzcd} {\Ga \cdot A} & \ptgrpd & \ptcat \\ \Ga & \grpd & \cat \\ {} \arrow[from=1-1, to=1-2] \arrow["\disp{A}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[from=1-2, to=1-3] \arrow[from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow[from=1-3, to=2-3] \arrow["A"', from=2-1, to=2-2] \arrow[from=2-2, to=2-3] \end{tikzcd}$

Corollary 4.1.6 The display map classifier is presentable

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}$.

$\begin{tikzcd} {\yo \Ga \cdot A} & \Term \\ {\yo \Ga} & \Type \\ {} \arrow[from=1-1, to=1-2] \arrow["{\yo \disp A}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\tp"', from=1-2, to=2-2] \arrow["A"', from=2-1, to=2-2] \end{tikzcd}$

Proof ▶

Consider the pullback in $\mathbf{Cat}$

$\begin{tikzcd} {\Ga \cdot A} & \ptgrpd \\ \Ga & \grpd \\ {} \arrow[from=1-1, to=1-2] \arrow[from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[from=1-2, to=2-2] \arrow["A"', from=2-1, to=2-2] \end{tikzcd}$

We send this square along $\mathsf{res} \circ \mathsf{y}$ in the following

$\begin{tikzcd} \Cat && \PshCat \\ \grpd && \Pshgrpd \\ & {} \arrow["\yo", from=1-1, to=1-3] \arrow[from=1-1, to=2-3] \arrow["{\mathsf{res}}", from=1-3, to=2-3] \arrow[from=2-1, to=1-1] \arrow["\yo", from=2-1, to=2-3] \end{tikzcd}$

The Yoneda embedding $\mathsf{y}: \mathbf{Cat}\to \mathbf{Psh}(\mathbf{Cat})$ preserves pullbacks, as does $\mathsf{res}$ since it is a right adjoint (with left Kan extension $\iota _{!} \dashv \mathsf{res}_{\iota }$).

4.2 Groupoid fibrations

Definition 4.2.1 Fibration

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$

$\begin{tikzcd} a & b \\ x & y \arrow[""{name=0, anchor=center, inner sep=0}, "{\lift{a}{f}}", dashed, from=1-1, to=1-2] \arrow[maps to, from=1-1, to=2-1] \arrow[dashed, maps to, from=1-2, to=2-2] \arrow[""{name=1, anchor=center, inner sep=0}, "f"', from=2-1, to=2-2] \arrow[shorten <=4pt, shorten >=4pt, Rightarrow, dashed, maps to, from=0, to=1] \end{tikzcd}$

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.

Note that $\mathsf{disp}_{A} : \Gamma \cdot A \to \Gamma $ is a fibration, since for any $(x \in \Gamma , a \in A \, x)$ and $f : x \to y$ in $\Gamma $ we have a morphism $(f, \mathsf{id}_{A \, f \, a}) : (x, a) \to (y, A \, f \, a)$ lifting $f$. Furthermore

Proposition 4.2.2

There is an adjoint equivalence

$\begin{tikzcd} {[\Ga, \grpd]} && {\Fib_\Ga} \arrow["{\disp{}}", shift left=2, from=1-1, to=1-3] \arrow["\simeq"{description}, draw=none, from=1-1, to=1-3] \arrow["{\fiber}", shift left=2, from=1-3, to=1-1] \end{tikzcd}$

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

\[ \mathsf{fiber}_{\delta } \, x = \textit{full subcategory} \, \{ a \in \Delta \, |\, \delta \, a = x\} \]

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

Pullback of fibrations along groupoid functors is not strictly coherent, in the sense that for $\tau : \Xi \to \Delta $ and $\sigma : \Delta \to \Gamma $ and a fibration $p \in \mathsf{Fib}_{\Gamma }$ we only have an isomorphism

\[ \tau ^{*} \sigma ^{*} p \cong (\sigma \circ \tau )^{*} p \]

rather than equality.

In order to interpret reindexing/substitution strictly, it is convenient to work with classifiers $[\Gamma ,\mathbf{grpd}]$ instead of fibrations.

Proposition 4.2.3 Strictly coherent pullback

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

$\begin{tikzcd} {\De.A\si} & {\Ga.A} & \ptgrpd \\ \De & \Ga & \grpd \arrow["{\si_A}"', dashed, from=1-1, to=1-2] \arrow[bend left, from=1-1, to=1-3] \arrow["{\disp{A\si}}"{description}, two heads, from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[from=1-2, to=1-3] \arrow["{\disp{A}}"{description}, two heads, from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow[from=1-3, to=2-3] \arrow["\si"', from=2-1, to=2-2] \arrow["A"', from=2-2, to=2-3] \end{tikzcd}$

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

Corollary 4.2.4 Fibrations are stable under pullback

$\begin{tikzcd} {[\Ga, \grpd]} && {\Fib_\Ga} \\ {[\De, \grpd]} && {\Fib_\De} \arrow["{\circ \si}"', from=1-1, to=2-1] \arrow["{\fiber}"', from=1-3, to=1-1] \arrow["{\si^*}", dashed, from=1-3, to=2-3] \arrow["{\disp{}}"', from=2-1, to=2-3] \end{tikzcd}$

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.

A strict interpretation of type theory would require $\Sigma $ and $\Pi $-formers to be stable under pullback (Beck-Chevalley). Thus we again define these as operations on classifiers $[\Gamma ,\mathbf{grpd}]$.

Definition 4.2.5 $\Sigma $-former operation

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

\[ \Sigma _{A}B (x) := A(x) \cdot B \circ x_{A} \]

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})$

$\begin{tikzcd} {A(x) \cdot B \circ x_A} & {\Ga.A.B} & \bullet \\ {A(x)} & {\Ga.A} & \grpd \\ \terminal & \Ga & \grpd \arrow[dashed, from=1-1, to=1-2] \arrow["{\disp{B \circ x_A}}"{description}, two heads, from=1-1, to=2-1] \arrow[from=1-2, to=1-3] \arrow["{\disp{B}}"{description}, from=1-2, to=2-2] \arrow["{x_A}"', from=2-1, to=2-2] \arrow["{!}"{description}, from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow["B", from=2-2, to=2-3] \arrow["{\disp{A}}"{description}, two heads, from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["x"', from=3-1, to=3-2] \arrow["A"', from=3-2, to=3-3] \end{tikzcd}$

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

\[ \Sigma _{A}B \, f \, (a,b) := (A \, f \, a, B \, (f,\mathsf{id}_{{A \, f \, a}}) \, b) \]

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$

\[ \Sigma _{A}B \, f \, (\alpha ,\beta ) := (A \, f \, \alpha , B \, (f,\mathsf{id}_{{A \, f \, a_{1}}}) \, \beta ) \]

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

\[ \mathsf{fst}_{x} : (a, b) \mapsto a \]

Proposition 4.2.6 Fibrations are closed under composition

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

$\begin{tikzcd} \Xi \\ \De & \Ga \arrow[two heads, from=1-1, to=2-1] \arrow[dashed, two heads, from=1-1, to=2-2] \arrow[two heads, from=2-1, to=2-2] \end{tikzcd}$

We can compare the two fibrations

\[ \mathsf{disp}_{B} \circ \mathsf{disp}_{A} \quad \quad \text{ and } \quad \quad \mathsf{disp}_{\Sigma _{A}(B)} \]

An object in the composition would look like $((x,a),b)$ for $x \in \Gamma $, $a \in A(x)$ and $b \in B(x,a)$, whereas an object in $\Gamma \cdot {\Sigma _{A}(B)}$ would instead be $(x,(a,b))$.

Proposition 4.2.7 Strict Beck-Chevalley for $\Sigma $

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

\[ (\Sigma _{A}B) \circ \sigma = \Sigma _{A \circ \sigma }(B \circ \sigma _{A}) \]

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

$\begin{tikzcd} & {\De \cdot A \si \cdot B \circ \si_A} & {\Ga.A.B} \\ & {\De \cdot A \si} & {\Ga.A} & \grpd \\ \grpd & \De & \Ga & \grpd \arrow["{\si_{A \cdot B}}"', from=1-2, to=1-3] \arrow["{\disp{B \circ \si_A}}"{description}, two heads, from=1-2, to=2-2] \arrow["{\disp{B}}"{description}, two heads, from=1-3, to=2-3] \arrow["{\si_A}"', from=2-2, to=2-3] \arrow["{\disp{A\si}}"{description}, from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["B", from=2-3, to=2-4] \arrow["{\disp{A}}"{description}, two heads, from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow["{(\Si_A B) \circ \si}"', shift right, from=3-2, to=3-1] \arrow["{\Si_{A \circ \si} (B \circ \si_A)}", shift left, from=3-2, to=3-1] \arrow["\si"', from=3-2, to=3-3] \arrow["A"', from=3-3, to=3-4] \end{tikzcd}$

Proof ▶

By checking pointwise at $x \in \Delta $, this boils down to showing

\[ (\sigma x)_{A} = \sigma _{A} \circ x_{A \circ \sigma } : A (\sigma x) \to \Gamma \cdot A \]

$\begin{tikzcd} {A (\si x)} & {\De \cdot A \si} & {\Ga.A} & \grpd \\ \terminal & \De & \Ga & \grpd \arrow["{x_{A \si}}"', from=1-1, to=1-2] \arrow["{(\si x)_A}", bend left, from=1-1, to=1-3] \arrow["{!}"{description}, from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{\si_A}"', from=1-2, to=1-3] \arrow["{\disp{A\si}}"{description}, from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["B", from=1-3, to=1-4] \arrow["{\disp{A}}"{description}, two heads, from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["x"', from=2-1, to=2-2] \arrow["\si"', from=2-2, to=2-3] \arrow["A"', from=2-3, to=2-4] \end{tikzcd}$

which holds because of the universal property of pullback.

Definition 4.2.8 $\Pi $-former operation

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

\[ [\Gamma \cdot A, \mathbf{grpd}](\mathsf{disp}_{A}\circ C, B) \cong [\Gamma , \mathbf{grpd}](C, \Pi _{A} B) \]

natural in both $B$ and $C$.

Proof ▶

$\Pi _{A}B$ acts on objects by taking fiberwise sections

\[ \Pi _{A}B (x) := \{ s \in [A (x), \Sigma _{A}B (x)] \, |\, \mathsf{fst}_x \circ s = \mathsf{id}_{A (x)}\} \]

Where we have taken the full subcategory of the functor category $[A (x), \Sigma _{A}B (x)]$. This is a groupoid since any natural transformation of functors into groupoids are natural isomorphisms.

$\Pi _{A}B$ acts on morphisms via conjugation

$\begin{tikzcd} x &&& {\Pi_A B (x)} &&& {A (x)} && {\Si_{A}B (x)} \\ & {} & {} \\ y &&& {\Pi_A B(y)} &&& {A (y)} && {\Si_{A}B (y)} \arrow["f", from=1-1, to=3-1] \arrow["{\Si_AB(f) \circ - \circ A (f^{-1})}", from=1-4, to=3-4] \arrow["s"{description}, from=1-7, to=1-9] \arrow["{\Si_A B(f)}"{description}, from=1-9, to=3-9] \arrow["{\Pi_A B}", maps to, from=2-2, to=2-3] \arrow["{A(f^{-1})}"{description}, from=3-7, to=1-7] \arrow["{\Pi_A B (f) (s)}"', dashed, from=3-7, to=3-9] \end{tikzcd}$

Note that conjugation is functorial and invertible.

Corollary 4.2.9 Fibrations are closed under pushforward

Stated in terms of fibrations, we have

$\begin{tikzcd} \Xi & {\Ga_! \si_* \tau} \\ \De & \Ga \arrow["\tau"', two heads, from=1-1, to=2-1] \arrow["{\si_* \tau}", two heads, from=1-2, to=2-2] \arrow["\si"', two heads, from=2-1, to=2-2] \end{tikzcd}$

with the universal property of pushforward

\[ \mathsf{Fib}_{\Delta }(\sigma ^{*}\rho , \tau ) \cong \mathsf{Fib}_{\Gamma }(\rho , \sigma _{*} \tau ) \]

natural in both $\tau $ and $\rho $.

Proposition 4.2.10 Strict Beck-Chevalley for $\Pi $

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

\[ (\Pi _{A}B) \circ \sigma = \Pi _{A \circ \sigma }(B \circ \sigma _{A}) \]

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

$\begin{tikzcd} & {\De \cdot A \si \cdot B \circ \si_A} & {\Ga.A.B} \\ & {\De \cdot A \si} & {\Ga.A} & \grpd \\ \grpd & \De & \Ga & \grpd \arrow["{\si_{A \cdot B}}"', from=1-2, to=1-3] \arrow["{\disp{B \circ \si_A}}"{description}, two heads, from=1-2, to=2-2] \arrow["{\disp{B}}"{description}, two heads, from=1-3, to=2-3] \arrow["{\si_A}"', from=2-2, to=2-3] \arrow["{\disp{A\si}}"{description}, from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["B", from=2-3, to=2-4] \arrow["{\disp{A}}"{description}, two heads, from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow["{\Pi_A B \circ \si}"', shift right, from=3-2, to=3-1] \arrow["{\Pi_{A \circ \si} (B \circ \si_A)}", shift left, from=3-2, to=3-1] \arrow["\si"', from=3-2, to=3-3] \arrow["A"', from=3-3, to=3-4] \end{tikzcd}$

Proof ▶

By checking pointwise, this boils down to Beck-Chevalley for $\Sigma $.

Proposition 4.2.11 All objects are fibrant

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

Definition 4.2.12 Interval

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}$.

$\begin{tikzcd} & \terminal \\ \terminal & \Two \\ && \Interval \arrow[from=1-2, to=2-2] \arrow["{\de_1}", bend left, from=1-2, to=3-3] \arrow[from=2-1, to=2-2] \arrow["{\de_0}"', bend right, from=2-1, to=3-3] \arrow["\partial"{description}, dashed, from=2-2, to=3-3] \end{tikzcd}$

Proposition 4.2.13 Path object 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^{-}$.

$\begin{tikzcd} {A^{\Interval}} \\ & {A \times A} & A \\ & A \arrow["{A^\partial}"{description}, dashed, two heads, from=1-1, to=2-2] \arrow["{A^{\de_1}}", bend left, two heads, from=1-1, to=2-3] \arrow["{A^{\de_0}}"', bend right, two heads, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \end{tikzcd}$

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

We can use this to justify the interpretation of the identity type later, where we will have the strictified versions (as in strictly stable under substitution) of the above

$\begin{tikzcd} A & {\terminal \cdot A} & \ptgrpd & \ptgrpd \\ {A^{\Interval}} & {\terminal \cdot A \cdot A \cdot \Id} & {I'} & \grpd \\ {A \times A} & {\terminal \cdot A \cdot A} & {U \times_\grpd U} & \ptgrpd \\ A & {\terminal \cdot A} & \ptgrpd & \grpd \\ {} & \terminal & \grpd \arrow["\iso"{description}, from=1-1, to=1-2] \arrow[from=1-1, to=2-1] \arrow["{\var_A}", from=1-2, to=1-3] \arrow["{A^* \rho'}"{description}, from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["{\rho'}"{description}, from=1-3, to=2-3] \arrow["U", from=1-4, to=2-4] \arrow["\iso"{description}, from=2-1, to=2-2] \arrow["{A^{\partial}}"{description}, two heads, from=2-1, to=3-1] \arrow[from=2-2, to=2-3] \arrow["{\disp{\Id' \circ U^* \var_A}}"{description}, from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow[from=2-3, to=1-4] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=30}, draw=none, from=2-3, to=2-4] \arrow[from=2-3, to=3-3] \arrow["\iso"{description}, from=3-1, to=3-2] \arrow["\fst"', from=3-1, to=4-1] \arrow[from=3-2, to=3-3] \arrow["{\disp{U \circ \var_A}}"{description}, from=3-2, to=4-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3] \arrow["{\Id'}"{description}, from=3-3, to=2-4] \arrow["\snd"', from=3-3, to=3-4] \arrow["\fst"{description}, from=3-3, to=4-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-3, to=4-4] \arrow["U"', from=3-4, to=4-4] \arrow["\iso"{description}, from=4-1, to=4-2] \arrow["{\var_A}"{description}, from=4-2, to=4-3] \arrow["{\disp{A}}"', from=4-2, to=5-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=4-2, to=5-3] \arrow["U"', from=4-3, to=4-4] \arrow["U", from=4-3, to=5-3] \arrow["A"', from=5-2, to=5-3] \end{tikzcd}$

In general, we will want to build a pathspace for a type in any context, which requires us to pull back the interval along the context, and rebuild the required fibration by exponentiation in the slice.

4.3 Classifying type dependency

Proposition 4.3.1 $P_{\mathsf{tp}}$ classifies type dependency

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

\[ A : \Gamma \to \mathsf{Ty}\quad \quad \text{ and } \quad \quad B : \Gamma \cdot A \to X \]

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

\[ A : \Gamma \to \mathbf{grpd}\quad \quad \text{ and } \quad \quad B : \Gamma \cdot A \to \mathbf{grpd} \]

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

$\begin{tikzcd} & \De \\ {} & \Ga & {\Poly{\tp} X} \arrow["\si"', from=1-2, to=2-2] \arrow["{(A\circ \si, B \circ \tp^* \si)}", from=1-2, to=2-3] \arrow["{(A, B)}"', from=2-2, to=2-3] \end{tikzcd}$

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

$\begin{tikzcd} {\De \cdot A\circ \si} & {\Ga\cdot A} & \ptgrpd \\ \De & \Ga & \grpd \arrow["{\tp^* \si}", dashed, from=1-1, to=1-2] \arrow[two heads, from=1-1, to=2-1] \arrow[from=1-2, to=1-3] \arrow[two heads, from=1-2, to=2-2] \arrow[from=1-3, to=2-3] \arrow["\si"', from=2-1, to=2-2] \arrow["A"', from=2-2, to=2-3] \end{tikzcd}$

4.4 Pi and Sigma structure

Lemma 4.4.1

$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

\begin{align*} \tilde{F}_{\Gamma } : \mathbf{Psh}(\mathbf{grpd})(\Gamma , P_{\mathsf{tp}} X) & \to \mathbf{Psh}(\mathbf{grpd})(\Gamma , X) \\ (A, B) & \mapsto F_{A} B \end{align*}

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

\[ (F_{A} B) \circ \sigma = F_{A \circ \sigma } (B \circ \mathsf{tp}^{*} \sigma ) \]

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

Proof ▶

Using 4.3.1

$\begin{tikzcd} [column sep = small] {(A, B)} &&& {F_AB} \\ & {\Pshgrpd(\Ga, \Poly{\tp} X) } & {\Pshgrpd(\Ga, X)} \\ & {\Pshgrpd(\De, \Poly{\tp} X) } & {\Pshgrpd(\De, X)} \\ {(A \circ \si, B \circ \tp^* \si)} && {F_{A \circ \si} B \circ \tp^* \si} & {(F_A B) \circ \si} \arrow[maps to, from=1-1, to=1-4] \arrow[maps to, from=1-1, to=4-1] \arrow[maps to, from=1-4, to=4-4] \arrow["{\tilde{F}_{\Ga}}", from=2-2, to=2-3] \arrow["{- \circ \si}"', from=2-2, to=3-2] \arrow["{- \circ \si}", from=2-3, to=3-3] \arrow["{\tilde{F}_{\De}}"', from=3-2, to=3-3] \arrow[maps to, from=4-1, to=4-3] \arrow[Rightarrow, dashed, no head, from=4-3, to=4-4] \end{tikzcd}$

Definition 4.4.2 Interpretation of $\Pi $ types

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 $

\[ \lambda _{A}\beta \, (x) := (\Pi _{A} B \, (x) , a \mapsto (a, b (x , a))) \]

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

\[ \lambda _{A}\beta \, (f) := (\Pi _{A} B \, (f) , \eta ) \]

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

\[ \eta _{a} := (\mathsf{id}_{a}, \mathsf{id}_{b (y , a)}) \]

These combine to give us a pullback square

$\begin{tikzcd} {\Poly{\tp}{\Term}} & \Term \\ {\Poly{\tp}{\Type}} & \Type \arrow["\la", from=1-1, to=1-2] \arrow["{\Poly{\tp}{\tp}}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\tp", from=1-2, to=2-2] \arrow["\Pi"', from=2-1, to=2-2] \end{tikzcd}$

Proof ▶

We should check that the $\lambda $ operation satisfied Beck-Chevalley. This follows from the $\Pi $ satisfying Beck-Chevalley and extensionality results for functors.

The square commutes and is a pullback if and only it pointwise commutes and pointwise gives pullbacks, i.e. for each groupoid $\Gamma $

$\begin{tikzcd} {(A,\be)} &&& {\la_A \be} \\ & {\Pshgrpd(\Ga,\Poly{\tp}{\Term})} & {[\Ga,\ptgrpd]} \\ & {\Pshgrpd(\Ga,\Poly{\tp}{\Type})} & {[\Ga,\grpd]} \\ {(A,U\circ \be)} && {\Pi_\Ga U \circ \be} & {U \circ \la_A \be} \arrow[maps to, from=1-1, to=1-4] \arrow[maps to, from=1-1, to=4-1] \arrow[maps to, from=1-4, to=4-4] \arrow["{\la_\Ga}", from=2-2, to=2-3] \arrow["{\Pshgrpd(\Ga, \Poly{\tp}{\tp})}"', from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{U \circ -}", from=2-3, to=3-3] \arrow["{\Pi_\Ga}"', from=3-2, to=3-3] \arrow[maps to, from=4-1, to=4-3] \arrow[Rightarrow, no head, from=4-3, to=4-4] \end{tikzcd}$

where we have used 4.3.1. That this commutes follows from the definitions of $\Pi $ and $\lambda $.

To show it is pullback it suffices to note that for any $f : \Gamma \to \mathbf{grpd}_\bullet $ and $(A,B) : \Gamma \to P_{\mathsf{tp}} \mathsf{Ty}$ such that $U \circ f = \Pi _{A} B$, there exists a unique $(A, \beta ) : \Gamma \to P_{\mathsf{tp}} \mathsf{Tm}$ such that $U \circ \beta = B$ and $\lambda _{A} \beta = f$. Indeed $\beta $ is fully determined by the above conditions to be

\begin{align*} \beta : \Gamma \cdot A & \to \mathbf{grpd}_\bullet \\ (x, a) & \mapsto (B(x,a), f \, x \, a) \end{align*}

Lemma 4.4.3

This is a specialization of 5.0.3. Use $R$ to denote the fiber product

$\begin{tikzcd} R & {\Poly{\tp}{\Type}} \\ \Term & \Type \arrow["{\rho_{\Poly{}}}", from=1-1, to=1-2] \arrow["{\tp^* \tp_* \Term^* \Type = \rho_\Term}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{\tp_* \Term^* \Type}", from=1-2, to=2-2] \arrow["\tp"', from=2-1, to=2-2] \end{tikzcd}$

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}$.

$\begin{tikzcd} \Ga \\ & R & {\Poly{\tp} {\Type}} \\ & \Term & \Type \arrow["{(\al,B)}"{description}, from=1-1, to=2-2] \arrow["{(U \circ \al,B)}"{description}, bend left, from=1-1, to=2-3] \arrow["\al"', bend right, from=1-1, to=3-2] \arrow["{\rho_{\Poly{}}}", from=2-2, to=2-3] \arrow["{\rho_\Term}"', from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{\tp_* \Term^* \Type}", from=2-3, to=3-3] \arrow["\tp"', from=3-2, to=3-3] \end{tikzcd}$

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

$\begin{tikzcd} & \De \\ {} & \Ga & R \arrow["\si"', from=1-2, to=2-2] \arrow["{(\al \circ \si, B \circ \tp^*\si)}", from=1-2, to=2-3] \arrow["{(\al, B)}"', from=2-2, to=2-3] \end{tikzcd}$

Definition 4.4.4 Evaluation

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.

$\begin{tikzcd} \Ga \\ & R & {\Poly{\tp}{\Type}} \\ {\Type \times \Term} & \Term & \Type \\ \Type & \terminal \arrow["{(\al,B)}"{description, pos=0.7}, from=1-1, to=2-2] \arrow["{(A,B)}"{description}, bend left, from=1-1, to=2-3] \arrow["{(\ev{\al}{B}, \al)}"{description}, dashed, from=1-1, to=3-1] \arrow["\al"{description, pos=0.2}, from=1-1, to=3-2] \arrow["{\ev{\al}{B}}"{description}, bend right = 50, dashed, from=1-1, to=4-1] \arrow[from=2-2, to=2-3] \arrow["\counit"{description, pos=0.7}, from=2-2, to=3-1] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{\tp_* \Term^* \Type}", from=2-3, to=3-3] \arrow[from=3-1, to=3-2] \arrow[from=3-1, to=4-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2] \arrow["\tp"', from=3-2, to=3-3] \arrow[from=3-2, to=4-2] \arrow[from=4-1, to=4-2] \end{tikzcd}$

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

\[ \mathsf{ev}_{} \, = \pi _{\mathsf{Ty}} \circ \, \mathsf{counit} \, \]

Lemma 4.4.5

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

\[ \mathsf{ev}_{\alpha } \, B = B \circ a \]

where

$\begin{tikzcd} \Ga \\ & {\Ga \cdot A} & \ptgrpd \\ & \Ga & \grpd \arrow["a"{description}, dashed, from=1-1, to=2-2] \arrow["\al", bend left, from=1-1, to=2-3] \arrow[Rightarrow, no head, bend right, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow["{\disp{A}}"', from=2-2, to=3-2] \arrow[from=2-3, to=3-3] \arrow["A"', from=3-2, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \end{tikzcd}$

Proof ▶

This is a specialization of 5.0.5 with liberal applications of Yoneda.

Definition 4.4.6 Classifier for dependent pairs

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

$\begin{tikzcd} Q & R & R & {\Poly{\tp} {\Type}} \\ {\Term \times \Term} & {\Type \times \Term} & \Term & \Type \\ \Term & \Type & \terminal \arrow[from=1-1, to=1-2] \arrow["{\tp \PolyComp \tp}"{description}, bend left, from=1-1, to=1-4] \arrow[from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow[Rightarrow, no head, from=1-2, to=1-3] \arrow["\counit"{description}, from=1-2, to=2-2] \arrow[from=1-3, to=1-4] \arrow[from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["{\tp_* \Term^* \Type}", from=1-4, to=2-4] \arrow[from=2-1, to=2-2] \arrow[from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["\tp"', from=2-3, to=2-4] \arrow[from=2-3, to=3-3] \arrow["\tp"', from=3-1, to=3-2] \arrow[from=3-2, to=3-3] \end{tikzcd}$

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 $.

$\begin{tikzcd} \Ga \\ & Q & R & R & {\Poly{\tp} {\Type}} \\ & {\Term \times \Term} & {\Type \times \Term} & \Term & \Type \\ & \Term & \Type & \terminal \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow[""{name=0, anchor=center, inner sep=0}, Rightarrow, no head, from=2-3, to=2-4] \arrow["\counit"{description}, from=2-3, to=3-3] \arrow[from=2-4, to=2-5] \arrow[from=2-4, to=3-4] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-4, to=3-5] \arrow["{\tp_* \Term^* \Type}", from=2-5, to=3-5] \arrow[from=3-2, to=3-3] \arrow[from=3-2, to=4-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3] \arrow[from=3-3, to=3-4] \arrow[from=3-3, to=4-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-3, to=4-4] \arrow["\tp"', from=3-4, to=3-5] \arrow[from=3-4, to=4-4] \arrow["\tp"', from=4-2, to=4-3] \arrow[from=4-3, to=4-4] \arrow["\ep"{description}, from=1-1, to=2-2] \arrow["{(A,B)}"{description}, bend left, from=1-1, to=2-5] \arrow["\al"{description, pos=0.2}, bend left = 10, from=1-1, to=3-4] \arrow["\be"', from=1-1, bend right, to=4-2] \arrow["{( \al , B ) }"{description}, bend left = 25, from=1-1, to=2-3] \end{tikzcd}$

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

\[ \varepsilon = (\beta , \alpha , B) \]

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

$\begin{tikzcd} \De \\ \Ga & Q \arrow["\si"', from=1-1, to=2-1] \arrow["{(\be \circ \si, \al \circ \si, B \circ \tp^* \si)}", from=1-1, to=2-2] \arrow["{(\be, \al, B)}"', from=2-1, to=2-2] \end{tikzcd}$

Definition 4.4.7 Interpretation of $\Sigma $

We define the natural transformation

\[ \Sigma : P_{\mathsf{tp}} \mathsf{Ty}\to \mathsf{Ty} \]

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})$)

\[ \alpha \, x = (A \, x, a_{x}) \quad \text{ and } \quad \beta \, x = (B (x , a_{x}), b_{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})$)

\[ \alpha \, f = (A \, f, \phi _{f} { \color {gray} : A \, f \, a_{x} \to a_{y}}) \quad \text{ and } \quad \beta \, f = (B(f, \phi _{f}), \psi _{f} {\color {gray}: B(f, \phi _{f}) \, b_{a_{x}}\to b_{a_{y}}}) \]

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

$\begin{tikzcd} Q & \Term \\ {\Poly{\tp}{\Type}} & \Type \arrow["\pair", from=1-1, to=1-2] \arrow["{\tp \PolyComp \tp}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\tp", from=1-2, to=2-2] \arrow["\Si"', from=2-1, to=2-2] \end{tikzcd}$

Proof ▶

To show naturality of $\mathsf{pair}$, suppose $\sigma : \Delta \to \Gamma $ is a functor between groupoids.

$\begin{tikzcd} {\Pshgrpd(\De,Q)} &&& {[\De,\ptgrpd]} \\ & {(\be \circ \si,\al \circ \si,B \circ \tp^{*}\si)} & {?} \\ & {(\be,\al,B)} & {\pair_\Ga(\be,\al,B)} \\ {\Pshgrpd(\Ga,Q)} &&& {[\Ga,\ptgrpd]} \arrow["{\pair_\De}", from=1-1, to=1-4] \arrow[maps to, from=2-2, to=2-3] \arrow[maps to, from=3-2, to=2-2] \arrow[maps to, from=3-2, to=3-3] \arrow[maps to, from=3-3, to=2-3] \arrow["{\circ \si}", from=4-1, to=1-1] \arrow["{\pair_\Ga}"', from=4-1, to=4-4] \arrow["{\circ \si}"', from=4-4, to=1-4] \end{tikzcd}$

So we check that for any $x \in \Gamma $,

\begin{align*} & \mathsf{pair}_\Delta (\beta \circ \sigma , \alpha \circ \sigma , B \circ \sigma _A) \, x \\ = \, & (\Sigma _{A \circ \sigma } B \circ \sigma _A \, x, (a_x, b_{a_x})) \\ = \, & ((\Sigma _{A} B) \circ \sigma \, x, (a_x, b_{a_x})) \\ = \, & \mathsf{pair}_\Gamma (\beta , \alpha , B) \circ \sigma \, x \end{align*}

where

\[ \alpha \circ \sigma \, x = (A \circ \sigma x, a_{x}) \quad \text{and} \quad \beta \circ \sigma \, x = (\mathsf{ev}_{\alpha } \, B \circ \sigma \, x, b_{a_{x}}) \]

and so on.

It follows from the definition of $\mathsf{pair}$ that the square commutes. To show that it is pullback, it suffices to show that for each $\Gamma $,

$\begin{tikzcd} {\Pshgrpd (\Ga, Q)} & {[\Ga,\ptgrpd]} \\ {\Pshgrpd(\Ga,\Poly{\tp}{\Type})} & {[\Ga,\grpd]} \arrow["{\pair_\Ga}", from=1-1, to=1-2] \arrow["{\tp \PolyComp \tp \circ -}"', from=1-1, to=2-1] \arrow["{U \circ -}", from=1-2, to=2-2] \arrow["{\Si_\Ga}"', from=2-1, to=2-2] \end{tikzcd}$

is a pullback. Since we are in $\mathbf{Set}$, it suffices to just show the universal property applied to a point: so for any $A : \Gamma \to \mathbf{grpd}$, any $B : \Gamma \cdot A \to \mathbf{grpd}$, and any $p : \Gamma \to \mathbf{grpd}_\bullet $, such that

\[ U \circ p = \Sigma _{\Gamma } (A, B) \]

there exists a unique $(\beta , \alpha , B) : \Gamma \to Q$ such that

\[ \mathsf{pair}_{\Gamma }(\beta ,\alpha ,B) = p \quad \text{and} \quad \mathsf{tp}\lhd \mathsf{tp}\circ (B,\alpha , B) = (A, B) \]

Indeed if we write

\[ p \, x = (\Sigma _{A} B \, x , (a_{x} {\color {gray} \in A x}, b_{x} {\color {gray} \in B(x, a_{x})})) \]

this uniquely determines $\alpha $ and $\beta $ as

\[ \alpha \, x = (A x, a_{x}) \quad \text{and} \quad \beta \, x = (\mathsf{ev}_{\alpha } \, B \, x, b_{x}) \]

4.5 Identity types

Definition 4.5.1 Identity formation and introduction

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

$\begin{tikzcd} \Term & \Term \\ {\tp \times_\Type \tp} & \Type \arrow["\refl", from=1-1, to=1-2] \arrow["\de"', from=1-1, to=2-1] \arrow["\tp", from=1-2, to=2-2] \arrow["\Id"', from=2-1, to=2-2] \end{tikzcd}$

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

$\begin{tikzcd} \Cat & \PshCat & \Pshgrpd \arrow["\yo", from=1-1, to=1-2] \arrow["{\mathsf{res}}", from=1-2, to=1-3] \end{tikzcd}$

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

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

$\begin{tikzcd} \ptgrpd & \ptgrpd \\ {U \times_\grpd U} & \grpd \arrow["{\refl'}", from=1-1, to=1-2] \arrow["\de"', from=1-1, to=2-1] \arrow["U", from=1-2, to=2-2] \arrow["{\Id'}"', from=2-1, to=2-2] \end{tikzcd}$

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

\[ (A, a_{0}, a_{1}) \mapsto A(a_{0}, a_{1}) \]

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

\[ (f : {\color {gray} A \to B}, \phi _{0} : {\color {gray} f a_{0} \to b_{0}}, \phi _{1} : {\color {gray} f a_{1} \to b_{1}}) \mapsto \phi _{1} \circ f(-) \circ \phi _{0}^{-1} \]

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

\[ (A, a) \mapsto (A(a,a), \mathsf{id}_{a}) \]

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

\[ (f : {\color {gray} A \to B}, \phi : {\color {gray} (A, a) \to (B, b)}) \mapsto (\phi \circ f(-) \circ \phi ^{-1}, \phi \circ f(\mathsf{id}_{a}) \circ \phi ^{-1} = \mathsf{id}_{b}) \]

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.

Proof ▶

Since $\delta (A,a) = (A, a, a)$, it follows that the square in 1 commutes.

Lemma 4.5.2

We can then construct the pullback $I'$

$\begin{tikzcd} \ptgrpd \\ & {I'} & \ptgrpd \\ & {U \times_\grpd U} & \grpd \arrow["{\rho'}"{description}, dashed, from=1-1, to=2-2] \arrow["{\refl'}", bend left, from=1-1, to=2-3] \arrow["\de"', bend right, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["U", from=2-3, to=3-3] \arrow["{\Id'}"', from=3-2, to=3-3] \end{tikzcd}$

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

\[ (f, \phi _{0}, \phi _{1}, A h = k) : (A, a_{0}, a_{1}, h : a_{0} \to a_{1}) \to (B, b_{0}, b_{1}, k : b_{0} \to b_{1}) \]

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

\[ \rho ' (A, a) = (A, a, a, \mathsf{id}_{a}) \]

Lemma 4.5.3

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

\[ A : \Gamma \to \mathsf{Ty}\quad \quad \text{ and } \quad \quad C : \Gamma \cdot A \cdot A \cdot \mathsf{Id}\to X \]

where $A = q \circ \varepsilon $ and

$\begin{tikzcd} X & {\Ga \cdot A \cdot A \cdot \Id} & {I'} & \ptgrpd \\ & {\Ga \cdot A \cdot A} & {U \times_\grpd U} & \grpd \\ & {\Ga \cdot A} & \ptgrpd \\ & \Ga & \grpd \arrow["C"', from=1-2, to=1-1] \arrow[from=1-2, to=1-3] \arrow[from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow[from=1-3, to=1-4] \arrow[from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["U", from=1-4, to=2-4] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{\Id'}"', from=2-3, to=2-4] \arrow["\fst"', from=2-3, to=3-3] \arrow[from=3-2, to=3-3] \arrow[from=3-2, to=4-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3] \arrow["U", from=3-3, to=4-3] \arrow["A"', from=4-2, to=4-3] \end{tikzcd}$

Lemma 4.5.4

$\begin{tikzcd} \Ga \\ & T & {\Poly{\tp} {\Term}} \\ & {\Poly{q} {\Type}} & {\Poly{\tp} {\Term}} \arrow[dashed, from=1-1, to=2-2] \arrow["{(A, \ga_\refl)}", bend left, dashed, from=1-1, to=2-3] \arrow["{(A, C)}"', bend right, dashed, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow[from=2-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] \arrow["{\Poly{\tp} {\tp}}", from=2-3, to=3-3] \arrow["{\Star{\rho}_{\Type}}"', from=3-2, to=3-3] \end{tikzcd}$

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

\begin{align*} A \, & : \Gamma \to \mathbf{grpd}\\ C \, & : \Gamma \cdot A \cdot A \cdot \mathsf{Id}\to \mathbf{grpd}\\ \gamma _{\mathsf{refl}} \, & : \Gamma \cdot A \to \mathbf{grpd}_\bullet \\ \text{ such that } \, & C \circ A^{*} \rho ’ = U \circ \gamma _{\mathsf{refl}} \\ \end{align*}

$\begin{tikzcd} \ptgrpd && {\Ga \cdot A} & \ptgrpd & \ptgrpd \\ \grpd && {\Ga \cdot A \cdot A \cdot \Id} & {I'} & \grpd \\ && {\Ga \cdot A \cdot A} & {U \times_\grpd U} & \ptgrpd \\ && {\Ga \cdot A} & \ptgrpd & \grpd \\ && \Ga & \grpd \arrow["U"', from=1-1, to=2-1] \arrow["{\ga_\refl}"{description}, from=1-3, to=1-1] \arrow["{\var_A}", from=1-3, to=1-4] \arrow["{A^* \rho'}"{description}, from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["{\rho'}"{description}, from=1-4, to=2-4] \arrow["U", from=1-5, to=2-5] \arrow["C"{description}, from=2-3, to=2-1] \arrow[from=2-3, to=2-4] \arrow["{\disp{\Id' \circ U^* \var_A}}"', from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow[from=2-4, to=1-5] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-4, to=2-5] \arrow[from=2-4, to=3-4] \arrow[from=3-3, to=3-4] \arrow["{\disp{U \circ \var_A}}"', from=3-3, to=4-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-3, to=4-4] \arrow["{\Id'}"{description}, from=3-4, to=2-5] \arrow["\snd"', from=3-4, to=3-5] \arrow["\fst"{description}, from=3-4, to=4-4] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-4, to=4-5] \arrow["U"', from=3-5, to=4-5] \arrow["{\var_A}"{description}, from=4-3, to=4-4] \arrow["{\disp{A}}"', from=4-3, to=5-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=4-3, to=5-4] \arrow["U"', from=4-4, to=4-5] \arrow["U", from=4-4, to=5-4] \arrow["A"', from=5-3, to=5-4] \end{tikzcd}$

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

$\begin{tikzcd} & \De \\ {} & \Ga & T \arrow["\si"', from=1-2, to=2-2] \arrow["{(A \circ \si, C \circ q^* \si, \ga_\refl \circ \tp^*\si )}", from=1-2, to=2-3] \arrow["{(A, C, \ga_\refl)}"', from=2-2, to=2-3] \end{tikzcd}$

Proof ▶

By the universal property of pullbacks, The data of a map from a representable $\Gamma \to T$ corresponds to the data of $(A, C) : \Gamma \to P_{q}{\mathsf{Ty}}$ and $(A',\gamma _\mathsf{refl}) : \Gamma \to P_{\mathsf{tp}}{\mathsf{Tm}}$ such that

\[ {\rho }^{\star }_{\mathsf{Ty}} \circ (A, C) = P_{\mathsf{tp}} {\mathsf{tp}} \circ (A', \gamma _\mathsf{refl}) \]

By 5.0.8 and 5.0.2 this says

\[ (A, C \circ A^{*} \rho ) = (A', \mathsf{tp}\circ \gamma _\mathsf{refl}) \]

so the above is equivalent to having $A = A', C, \gamma _\mathsf{refl}$ such that

\[ C \circ A^{*} \rho = \mathsf{tp}\circ \gamma _\mathsf{refl}\text{ in } \mathbf{Psh}(\mathbf{grpd}) \]

By Yoneda this is equivalent to requiring

\[ C \circ A^{*} \rho ' = U \circ \gamma _\mathsf{refl}\text{ in } \mathbf{Cat} \]

Proposition 4.5.5

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

\begin{align*} \varepsilon _{\Gamma } : \, & \mathbf{Psh}(\mathbf{grpd})(\Gamma , P_{q}{\mathsf{Tm}}) \to \mathbf{Psh}(\mathbf{grpd})(\Gamma , T) \\ & (A, \gamma ) \mapsto (A, U \circ \gamma , \gamma \circ A^{*} \rho ’) \end{align*}

Proof ▶

This follows from the computation for $T$ 4.5.4, the polynomial action on slice morphisms 5.0.8, and 5.0.2.

Definition 4.5.6 Identity elimination

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

\begin{align*} J_{\Gamma } : \mathbf{Psh}(\mathbf{grpd})(\Gamma , T) \to \, & \mathbf{Psh}(\mathbf{grpd})(\Gamma , P_{q}{\mathsf{Tm}})\\ (A, C, \gamma _{\mathsf{refl}}) \mapsto \, & (A, \gamma ) \end{align*}

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:

$\begin{tikzcd} \ptgrpd && {\Ga \cdot A} & \ptgrpd & \ptgrpd \\ \grpd && {\Ga \cdot A \cdot A \cdot \Id} & {I'} & \grpd \\ && {\Ga \cdot A \cdot A} & {U \times_\grpd U} & \ptgrpd \\ && {\Ga \cdot A} & \ptgrpd & \grpd \\ && \Ga & \grpd \arrow["U"', from=1-1, to=2-1] \arrow["{\ga_\refl}"{description}, from=1-3, to=1-1] \arrow["{\var_A}", from=1-3, to=1-4] \arrow["{A^* \rho'}"{description}, from=1-3, to=2-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] \arrow["{\rho'}"{description}, from=1-4, to=2-4] \arrow["U", from=1-5, to=2-5] \arrow["\ga"{description}, dashed, from=2-3, to=1-1] \arrow["C"{description}, from=2-3, to=2-1] \arrow[from=2-3, to=2-4] \arrow["{\disp{\Id' \circ U^* \var_A}}"', from=2-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] \arrow[from=2-4, to=1-5] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-4, to=2-5] \arrow[from=2-4, to=3-4] \arrow[from=3-3, to=3-4] \arrow["{\disp{U \circ \var_A}}"', from=3-3, to=4-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-3, to=4-4] \arrow["{\Id'}"{description}, from=3-4, to=2-5] \arrow["\snd"', from=3-4, to=3-5] \arrow["\fst"{description}, from=3-4, to=4-4] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-4, to=4-5] \arrow["U"', from=3-5, to=4-5] \arrow["{\var_A}"{description}, from=4-3, to=4-4] \arrow["{\disp{A}}"', from=4-3, to=5-3] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=4-3, to=5-4] \arrow["U"', from=4-4, to=4-5] \arrow["U", from=4-4, to=5-4] \arrow["A"', from=5-3, to=5-4] \end{tikzcd}$

Let us name the fibers over the diagonal

\[ C_{\mathsf{refl}} := U \circ \gamma _{\mathsf{refl}} = C \circ A^{*} \rho ' : \Gamma \cdot A \to \mathbf{grpd} \]

and its given points

\[ \gamma _{\mathsf{refl}} = (C_{\mathsf{refl}}, c_{\mathsf{refl}}) \]

(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

\[ (\mathsf{id}_{x},\mathsf{id}_{a_{0}},h, \_ ) : (x, a_{0}, a_{0}, \mathsf{id}_{a}) \to (x, a_{0}, a_{1}, h) \in \Gamma \cdot A \cdot A \cdot \mathsf{Id} \]

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$,

\[ a_{1} \in U \circ \mathsf{var}_{A} (x, a_{0}) = U (A x, a_{0}) = A x \]

and

\[ h \in Id' \circ U^{*}\mathsf{var}_{A} (x, a_{0}, a_{1}) = \mathsf{Id}' (A x, a_{0}, a_{1}) = A x (a_{0}, a_{1}) \]

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

\[ (\mathsf{Id}' \circ U^{*}\mathsf{var}_{A} (\mathsf{id}_{x}, \mathsf{id}_{a_{0}}, h)) \mathsf{id}_{a_{0}} = (\mathsf{Id}' (A \mathsf{id}_{x}, \mathsf{id}_{a_{0}}, h)) \mathsf{id}_{a_{0}} = h \circ A \mathsf{id}_{x} \mathsf{id}_{a_{0}} \circ \mathsf{id}_{a_{0}}^{-1} = h \]

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

\[ (x, a_{0}, a_{1}, h) \mapsto (C (x, a_{0}, a_{1}, h), C(\mathsf{id}_{x}, \mathsf{id}_{a_{0}}, h, \_ ) \, c_{\mathsf{refl}}(x, a_{0})) \]

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

\[ c_{\mathsf{refl}} (x, a_{0}) \in C \circ A^{*} \rho ' (x, a_{0}) = C(x, a_{0}, a_{1}, h) \]

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

\[ (f, \phi _{0}, \phi _{1}, \_ ) \mapsto ( C (f, \phi _{0}, \phi _{1}, \_ ), C(\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k, \_ ) \, c_{\mathsf{refl}}(f, \phi _{0}) ) \]

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

\begin{align*} C(\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k, \_ ) c_{\mathsf{refl}}(f, \phi _{0}) \quad : \quad & C (f, \phi _{0}, \phi _{1}, \_ ) \circ C(\mathsf{id}_{x}, \mathsf{id}_{a_{0}}, h, \_ ) \, c_{\mathsf{refl}}(x, a_{0}) \\ = \, & C (f, \phi _{0}, \phi _{1} \circ A f h, \_ ) \, c_{\mathsf{refl}}(x, a_{0}) \\ = \, & C (f, \phi _{0}, k \circ \phi _{0}, \_ ) \, c_{\mathsf{refl}}(x, a_{0}) \\ = \, & C (\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k , \_ ) \circ C (f, \phi _{0}, \phi _{0}, \_ ) \, c_{\mathsf{refl}}(x, a_{0}) \\ = \, & C (\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k , \_ ) \circ C_{\mathsf{refl}} (f, \phi _{0}) \, c_{\mathsf{refl}}(x, a_{0}) \\ \to \, & C (\mathsf{id}_{y}, \mathsf{id}_{b_{0}}, k , \_ ) \, c_{\mathsf{refl}} (y, b_{0})\\ \end{align*}

Proof ▶

Functoriality of $\gamma $ is routine. We show naturality of $J$. Suppose $\sigma : \Delta \to \Gamma $ is representable

$\begin{tikzcd} & {(A \circ \si, C \circ q^* \si, \ga_\refl \circ \tp^*\si )} & {\quad \quad(A \circ \si, \ga_\De) } \\ {} && {(A \circ \si, \ga_\Ga \circ q^*\si)} \\ & {\Pshgrpd(\De, T)} & {\Pshgrpd(\De, \Poly{q}{\Term})} \\ & {\Pshgrpd(\Ga, T)} & {\Pshgrpd(\Ga, \Poly{q}{\Term})} \\ & {(A, C, \ga_\refl)} & {(A, \ga_\Ga)} \arrow[maps to, from=1-2, to=1-3] \arrow[Rightarrow, dashed, no head, from=1-3, to=2-3] \arrow["{J_\De}", from=3-2, to=3-3] \arrow["{- \circ \si}", from=4-2, to=3-2] \arrow["{J_\Ga}"', from=4-2, to=4-3] \arrow["{- \circ \si}"', from=4-3, to=3-3] \arrow[maps to, from=5-2, to=5-3] \end{tikzcd}$

So we want to show that on objects $(x, a_{0}, a_{1}, h) \in \Delta \cdot A \circ \sigma \cdot A \circ \sigma \cdot \mathsf{Id}$

\[ \gamma _{\Delta } \, (x, a_{0}, a_{1}, h) = \gamma _{\Gamma } \circ q^{*} \sigma \, (x, a_{0}, a_{1}, h) \]

Let us denote $q^{*} \sigma (x, a_{0}, a_{1}, h) = (\sigma x, a_{0}', a_{1}', h')$. Then

\begin{align*} & \gamma _{\Delta } \, (x, a_{0}, a_{1}, h) \\ = \, & (C \circ q^{*} \sigma \, (x, a_{0}, a_{1}, h), (C \circ q^{*} \sigma \, (\mathsf{id}_{x}, \mathsf{id}_{a_{0}}, h, \_ )) (c_{\mathsf{refl}} (\mathsf{tp}^{*}\sigma (x, a_{0}))) )\\ = \, & (C \, (\sigma x, a_{0}’, a_{1}’, h’) , (C \, (\mathsf{id}_{\sigma x}, \mathsf{id}_{a_{0}'}, h’, \_ )) (c_{\mathsf{refl}} \, (\sigma x, a_{0}’)) )\\ = \, & \gamma _{\Gamma }(\sigma x, a_{0}’, a_{1}’, h’) \\ = \, & \gamma _{\Gamma } \circ q^{*} \sigma \, (x, a_{0}, a_{1}, h) \\ \end{align*}

and similarly for morphisms.

Proposition 4.5.7

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

Proof ▶

Let $(A, C, \gamma _{\mathsf{refl}}) : \Gamma \to T$ be a map from a representable. Then using the definition of $J$ and the computation of $\varepsilon $ 4.5.5

\[ \varepsilon _{\Gamma } \circ J_{\Gamma } \, (A, C, \gamma _{\mathsf{refl}}) = \varepsilon _{\Gamma } (A, \gamma ) = (A, U \circ \gamma , \gamma \circ A^{*} \rho ') \]

By definition of $\gamma $ from $J$ we can see that $U \circ \gamma = C$, so it suffices to show that $\gamma \circ A^{*} \rho ' = \gamma _{\mathsf{refl}}$. On an object $(x, a_{0})$

\begin{align*} \gamma \circ A^{*} \rho ’ (x, a_{0}) \\ = \, & \gamma (x, a_{0}, a_{0}, \mathsf{id}_{a_{0}})\\ = \, & (C(x,a_{0},a_{0},\mathsf{id}_{a_{0}}), C(\mathsf{id}_{x}, \mathsf{id}_{a_{0}}, \mathsf{id}_{a_{0}}) \, c_{\mathsf{refl}})\\ = \, & (C_{\mathsf{refl}} (x, a_{0}), c_{\mathsf{refl}}(x, a_{0}))\\ \end{align*}

4.6 Universe of Discrete Groupoids

In this section we assume three different universe sizes, which we will distinguish by all lowercase (small), capitalized first letter (large), and all-caps (extra large), respectively. For example, the three categories of sets will be nested as follows

\[ \mathbf{set}\hookrightarrow \mathbf{Set}\hookrightarrow \mathbf{SET} \]

We shift all of our previous work up by one universe level, so that we are working in the category $\mathbf{PSH}(\mathbf{Grpd})$ of extra large presheaves, indexed by the (extra large, locally large) category of large groupoids. We would then have $\mathsf{Ty}= [-, \mathbf{Grpd}]$ and $\mathsf{Tm}= [-, \mathbf{Grpd}_\bullet ]$.

Definition 4.6.1 Universe of discrete groupoids

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.

$\begin{tikzcd} \U & \grpd \\ & \Grpd \arrow[hook, from=1-1, to=1-2] \arrow["\El"', hook, from=1-1, to=2-2] \arrow[hook, from=1-2, to=2-2] \end{tikzcd}$

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

$\begin{tikzcd} \E & \Term \\ \U & \Type \arrow[from=1-1, to=1-2] \arrow["\pi"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\tp", from=1-2, to=2-2] \arrow["\El"', from=2-1, to=2-2] \end{tikzcd}$

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

\[ E((X,x), (Y,y)) = \{ f : X \to Y \, |\, f \, x = y \} \]

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

Showing that this universe is closed under $\Pi , \Sigma , \mathsf{Id}$ formation depends on how we formalize $\mathbf{set}\hookrightarrow \mathbf{Set}$. In both cases we need to check that discreteness is preserved by the type formers, which is straightforward. If we are working with sets and cardinality, i.e. taking $\mathbf{set}= \mathbf{Set}_{{\lt}\lambda } \subset \mathbf{Set}_{{\lt} \kappa } = \mathbf{Set}$ for some inaccessible cardinals $\lambda {\lt} \kappa $, then it is straightforward to check that the type formers do not make “larger” types. If we are working with type theoretic universes with a lift operation $\mathsf{ULift} : \mathbf{set}\to \mathbf{Set}$ then it may not be true that $\mathsf{ULift}$ commutes with our type formers.