2 Natural Models

In this chapter we describe the categorical semantics of our syntax via natural models. It follows previous work on natural models [ Awo17 ] , with the following additional features

A more compact description of identity types exploiting the technology of polynomial endofunctors.
A collection of N Russell-style nested universes.
universe-variable $\Pi $-types and $\Sigma $-types, i.e. with possibly different universe level inputs, and landing in the largest universe (imitating the type theory of Lean4).

2.1 Interpretation of syntax

A very brief overview of the interpretation of syntax follows. We will work in a presheaf category $\mathbf{Psh}(\mathbb {C})$. A context $\Gamma $ will be interpreted as an object $[\! [\Gamma ]\! ] \in \mathbb {C}$. We will often take the image of the context under the Yoneda embedding $\mathsf{y}[\! [\Gamma ]\! ] \in \mathbf{Psh}(\mathbb {C})$. If $i \le N$ is a universe level, then a typing judgment $\Gamma \vdash _i a : A$ will be interpreted as a commuting triangle of the following form

$\begin{tikzcd} & {\Term_i} \\ {\yo \IntpCtx{\Ga}} & {\Type_i} \arrow["{\tp_i}", from=1-2, to=2-2] \arrow["{\IntpTerm{a}}", from=2-1, to=1-2] \arrow["{\IntpType{A}}"', from=2-1, to=2-2] \end{tikzcd}$

2.2 Natural model

Fix a small category $\mathbb {C}$.

Definition 2.2.1 Natural model

✓

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

$\begin{tikzcd} {\yo (\Ga \cdot A)} & \Term \\ {\yo (\Ga)} & \Type \arrow["{\var_A}", 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}$

Definition 2.2.2 Russell universes

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

$\begin{tikzcd} {\Type_{i}} & {1 \cdot \U_i} && {\Term_{i+1}} \\ \\ & 1 && {\Type_{i+1}} \arrow["\iso"{description}, draw=none, from=1-1, to=1-2] \arrow[from=1-2, to=1-4] \arrow[from=1-2, to=3-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=3-4] \arrow["{\tp_{i+1}}", from=1-4, to=3-4] \arrow["{\U_i}"', from=3-2, to=3-4] \end{tikzcd}$

2.3 Pi types

Definition 2.3.1

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{tikzcd} {\Poly{\tp_i}{\Term_j}} & {\Term_{\max(i,j)}} \\ {\Poly{\tp_i}{\Type_j}} & {\Type_{\max(i,j)}} \arrow["\la", from=1-1, to=1-2] \arrow["{\Poly{\tp_i}{\tp_j}}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{\tp_{\max(i,j)}}", from=1-2, to=2-2] \arrow["\Pi"', from=2-1, to=2-2] \end{tikzcd}$

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

2.4 Sigma types

Definition 2.4.1

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{tikzcd} Q & {\Term_{\max(i,j)}} \\ {\Poly{\tp_i}{\Type_j}} & {\Type_{\max(i,j)}} \arrow["\pair", from=1-1, to=1-2] \arrow["{\tp_i \PolyComp \tp_j}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["{\tp_{\max(i,j)}}", from=1-2, to=2-2] \arrow["\Si"', from=2-1, to=2-2] \end{tikzcd}$

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

2.5 Identity types

Definition 2.5.1

✓

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

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

where $\delta $ is the diagonal:

$\begin{tikzcd} \Term \\ & {\tp \times_\Type \tp} & \Term \\ & \Term & \Type \arrow["\de"', from=1-1, to=2-2] \arrow[Rightarrow, no head, 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[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=3-3] \arrow["\tp"', from=3-2, to=3-3] \end{tikzcd}$

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

$\begin{tikzcd} \Term \\ & I & \Term \\ & {\tp \times_\Type \tp} & \Type \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["\tp", from=2-3, to=3-3] \arrow["\Id"', from=3-2, to=3-3] \end{tikzcd}$

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

$\begin{tikzcd} \Term \\ & I \\ & {\tp \times_\Type \tp} \\ & \Term \\ & \Type \arrow["\rho"{description}, dashed, from=1-1, to=2-2] \arrow["\de"{description}, bend right = 10, from=1-1, to=3-2] \arrow[bend right = 25, Rightarrow, no head, from=1-1, to=4-2] \arrow["\tp"', bend right = 40, from=1-1, to=5-2] \arrow[from=2-2, to=3-2] \arrow["q", bend left = 50, from=2-2, to=5-2] \arrow["\fst"', from=3-2, to=4-2] \arrow[from=4-2, to=5-2] \end{tikzcd}$

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{tikzcd} {\Poly{q} {\Term}} & {\Poly{\tp} {\Term}} \\ {\Poly{q} {\Type}} & {\Poly{\tp} {\Type}} \arrow["{\Star{\rho}_{\Term}}", from=1-1, to=1-2] \arrow["{\Poly{q} {\tp}}"', from=1-1, to=2-1] \arrow["{\Poly{\tp} {\tp}}", from=1-2, to=2-2] \arrow["{\Star{\rho}_{\Type}}"', from=2-1, to=2-2] \end{tikzcd}$

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

Taking the pullback $T$ and the comparison map $\varepsilon $ we have

$\begin{tikzcd} {\Poly{q} {\Term}} \\ & T & {\Poly{\tp} {\Term}} \\ & {\Poly{q} {\Type}} & {\Poly{\tp} {\Type}} \arrow["\ep"{description}, dashed, from=1-1, to=2-2] \arrow["{\Star{\rho}_{\Term}}", bend left, from=1-1, to=2-3] \arrow["{\Poly{q} {\tp}}"', 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["{\Poly{\tp} {\tp}}", from=2-3, to=3-3] \arrow["{\Star{\rho}_{\Type}}"', from=3-2, to=3-3] \end{tikzcd}$

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

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

2.6 Binary products and Exponentials

It is convenient to specialize $\Sigma $ and $\Pi $ types to their non-dependent counterparts $\times $ and $\mathsf{Exp}$.

Definition 2.6.1 Products and exponentials

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

\[ (\mathsf{fst}, \mathsf{snd}) : \mathsf{Ty}_i \times \mathsf{Ty}_j \to P_{\mathsf{tp}_i}{\mathsf{Ty}_j} \]

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

$\begin{tikzcd} {\Type_j} & {\Term_i \times \Type_j} & {\Term_i} \\ & {\Type_i \times \Type_j} & {\Type_i} \arrow["\snd"', from=1-2, to=1-1] \arrow[from=1-2, to=1-3] \arrow["{\fst^* \tp_i}"', from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["{\tp_i}", from=1-3, to=2-3] \arrow["\fst"', from=2-2, to=2-3] \end{tikzcd}$

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

$\begin{tikzcd} [column sep = large] F & {\Poly{\tp}{\Term}} & \Term \\ {\Type \times \Type} & {\Poly{\tp}{\Type}} & \Type \arrow["{(\dom,\fun)}", from=1-1, to=1-2] \arrow["\la", bend left, from=1-1, to=1-3] \arrow["{(\dom,:d)}"', from=1-1, to=2-1] \arrow["\la", from=1-2, to=1-3] \arrow["{\Poly{\tp}{\tp}}"', from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["\tp", from=1-3, to=2-3] \arrow["{(\fst,\snd)}"', from=2-1, to=2-2] \arrow["\Exp"', bend right, from=2-1, to=2-3] \arrow["\Pi"', from=2-2, to=2-3] \end{tikzcd}$

$\begin{tikzcd} [column sep = large] {\Term \times \Term} & Q & \Term \\ {\Type \times \Type} & {\Poly{\tp}{\Type}} & \Type \arrow["{(\snd, \fst, \tp \circ \snd)}", from=1-1, to=1-2] \arrow["\pair", bend left, from=1-1, to=1-3] \arrow["{\tp \times \tp}"', from=1-1, to=2-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\pair", from=1-2, to=1-3] \arrow["{\tp \PolyComp \tp}"', from=1-2, to=2-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] \arrow["\tp", from=1-3, to=2-3] \arrow["{(\fst,\snd)}"', from=2-1, to=2-2] \arrow["\times"', bend right, from=2-1, to=2-3] \arrow["\Si"', from=2-2, to=2-3] \end{tikzcd}$

By the universal property of pullbacks and 5.0.2 we can write a map $\Gamma \to F$ as a triple $(A,B,f)$ such that $A, B: \Gamma \to \mathsf{Ty}$ and

$\begin{tikzcd} {\Ga \cdot A} & \Term \\ \Ga & \Type \arrow["f", from=1-1, to=1-2] \arrow["{\disp{A}}"', from=1-1, to=2-1] \arrow["\tp", from=1-2, to=2-2] \arrow["B"', from=2-1, to=2-2] \end{tikzcd}$

This gives us four equivalent ways we can view a function. Namely, as $f : \Gamma \cdot A \to \mathsf{Tm}$ in the above diagram, $\lambda \circ f : \Gamma \to \mathsf{Tm}$, as $(A,B,f) : \Gamma \to F$, or as a map between the displays $\mathsf{disp}_{A} \to \mathsf{disp}_{B}$

$\begin{tikzcd} {\Ga \cdot A} \\ & {\Ga \cdot B} & \Term \\ & \Ga & \Type \arrow["{(\disp{A},f)}"{description}, dashed, from=1-1, to=2-2] \arrow["f", bend left, from=1-1, to=2-3] \arrow["{\disp{A}}"', bend right, from=1-1, to=3-2] \arrow[from=2-2, to=2-3] \arrow["{\disp{B}}"{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=3-3] \arrow["B"', from=3-2, to=3-3] \end{tikzcd}$

For the formalization, we need not prove that the pullback of $\mathsf{tp}\lhd \mathsf{tp}$ is $\mathsf{tp}\times \mathsf{tp}$. Rather, we can also use the universal property of pullbacks and 5.0.2 to classify a map into the pullback (whatever it may be) as a pair $(\alpha , \beta )$, where $\alpha , \beta : \Gamma \to \mathsf{Tm}$. This could then be adapted to a proof that the pullback is what the diagram claims it to be.

Definition 2.6.2

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

$\begin{tikzcd} &&& \Ga \\ {\Ga \cdot A} & \Term &&& F & \Term \\ \Ga & \Type &&& {\Type \times \Type} & \Type \arrow["{(A,A,\var_{A})}"{description}, from=1-4, to=2-5] \arrow["{\id_A}", bend left, dashed, from=1-4, to=2-6] \arrow["{(A,A)}"', bend right, from=1-4, to=3-5] \arrow["{\var_{A}}"', from=2-1, to=2-2] \arrow["{\disp{A}}"{description}, from=2-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] \arrow["\tp", from=2-2, to=3-2] \arrow["\la", from=2-5, to=2-6] \arrow["{(\dom, :d)}"{description}, from=2-5, to=3-5] \arrow["\tp", from=2-6, to=3-6] \arrow["A"', from=3-1, to=3-2] \arrow["\Exp"', from=3-5, to=3-6] \end{tikzcd}$

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

$\begin{tikzcd} {\Ga \cdot A} \\ & {\Ga \cdot A} & \Term \\ & \Ga & \Type \arrow[Rightarrow, dashed, no head, from=1-1, to=2-2] \arrow["{\var_A}", bend left, from=1-1, to=2-3] \arrow["{\disp{A}}"', bend right, from=1-1, to=3-2] \arrow["{\var_{A}}"', from=2-2, to=2-3] \arrow["{\disp{A}}"{description}, 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=3-3] \arrow["A"', from=3-2, to=3-3] \end{tikzcd}$

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

2.7 Univalence

For two types $A, B : \Gamma \to \mathsf{Ty}$ and two functions $f, g : A \to B$ we can define internally a homotopy from $f$ to $g$ as

\[ f \sim g := \Pi _{a : A} \, \mathsf{Id}(f \, a, g \, a) \]

We define the types of left and right inverses of $f : A \to B$ as

\[ \mathsf{BigLinv} f := \Sigma _{g : B \to A} \, g \circ f \sim \mathsf{id}_{A} \]

\[ \mathsf{BigRinv} f := \Sigma _{g : B \to A} \, f \circ g \sim \mathsf{id}_{B} \]

and the property of being an equivalence

\[ \mathsf{IsBigEquiv} f := \mathsf{BigLinv} f \times \mathsf{BigRinv} f \]

We could do the same for two small types $A, B : \Gamma \to \mathsf{U}$

\[ \mathsf{IsEquiv} f := \mathsf{Linv} f \times \mathsf{Rinv} f \]

\[ \mathsf{Equiv} A \, B := \Sigma _{f : A \to B} \mathsf{IsEquiv} f \]

Again, internally we can define a function

\[ \mathsf{IdToEquiv} A \, B : \mathsf{Id}(A, B) \to \mathsf{Equiv} A \, B \]

which uses $J$ to transport along the proof of equality to produce an equivalence.

Definition 2.7.1

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

\[ \mathsf{ua} : \mathsf{IsBigEquiv} (\mathsf{IdToEquiv} A \, B) \]

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

$\begin{tikzcd} {\U \cdot \U \cdot \Id} && {\U \cdot \U \cdot \mathsf{Equiv}} \\ & {\U \cdot \U} \arrow["{\mathsf{IdToEquiv}}", from=1-1, to=1-3] \arrow[from=1-1, to=2-2] \arrow[from=1-3, to=2-2] \end{tikzcd}$

2.8 Extensional identity types and UIP

In this section we outline variations on the identity type in the natural model. We will describe these as additional structure on $\mathsf{Id}$, as opposed to introducing different identity types.

Definition 2.8.1 Extensional types

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

$\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["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \arrow["\tp", from=1-2, to=2-2] \arrow["\Id"', from=2-1, to=2-2] \end{tikzcd}$

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.

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

We could only require UIP:

Definition 2.8.2 Identity types satisfying UIP

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

$\begin{tikzcd} & I \\ \Ga & {\tp \times_\Type \tp} \arrow[from=1-2, to=2-2] \arrow["{!}", dashed, from=2-1, to=1-2] \arrow["{(a,b)}"', from=2-1, to=2-2] \end{tikzcd}$

One might wonder what other variations we could come up with by tweaking the pullback conditions. In fact, only requiring that $\rho $ has a section is equivalent to requiring that $\rho $ is an isomorphism. So this just the extensional case again.

If we require instead that $\varepsilon $ is an isomorphism then this is giving an $\eta $-rule for $J$, from which we can prove equality reflection and UIP [ Hof95 ] . So this just the extensional case again.