2.1 Products and pullbacks

For a binary product $A \times B$ , we denote the projection maps $\pi _1^{A,B}$ and $\pi _2^{A,B}$ , omitting superscripts when they can be inferred from the context. The pairing of $f : X \rightarrow A$ and $g : X \rightarrow B$ is denoted $\langle f, g \rangle$ , and given $\alpha : X \rightarrow A$ and $\beta : Y \rightarrow B$ , we write $\alpha \times \beta$ for $\langle \alpha \circ \pi _1, \beta \circ \pi _2\rangle : X \times Y \rightarrow A \times B$ . This notation extends to the $n$ -fold product $A_1 \times \ldots \times A_n$ , which has projections $\pi _1, \ldots , \pi _n$ and pairing $\langle f_i \rangle _{i=1}^n$ . In particular, for the terminal object $\unicode {x1D7D9}$ , the unique arrow $X \rightarrow \unicode {x1D7D9}$ is denoted $\langle \rangle _X$ .

For pullbacks, the notation is similar. The pullback of $f : A \rightarrow C$ and $g : B \rightarrow C$ is denoted $A \times _C B$ , and the projections are denoted $\pi _1^{A,B}$ and $\pi _2^{A,B}$ . We will also use the notation $\langle p, q \rangle : X \rightarrow A \times _C B$ and $\alpha \times _C \beta : X \times _C Y \rightarrow A \times _C B$ whenever these constructions are well-defined.

2.2 Slice categories and exponentiable arrows

Given an arrow $f : A \rightarrow B$ in a category $\mathcal{C}$ , we write $\Sigma _f$ for the composition functor $\mathcal{C}/A \rightarrow \mathcal{C}/B$ . Its right adjoint is the pullback functor $\Delta _f : \mathcal{C}/B \rightarrow \mathcal{C}/A$ (sometimes denoted $f^*$ ), assuming it exists. In the special case $B = \unicode {x1D7D9}$ , these functors become $\Sigma _A : \mathcal{C}/A \rightarrow \mathcal{C}$ (the forgetful functor) and $\Delta _A : \mathcal{C} \rightarrow \mathcal{C}/A$ .

If $\Delta _f$ has a further right adjoint, we call it the dependent product functor along $f$ and denote it $\Pi _f : \mathcal{C}/A \rightarrow \mathcal{C}/B$ . We say $f$ is exponentiable if the right adjoint $\Pi _f$ exists; this is equivalent to saying that $f$ is exponentiable as an object of $\mathcal{C}/B$ (per Corollary 1.2 of Niefield (Reference Niefield1982)).

2.3 Polynomials

Polynomials and polynomial functors are often discussed in the context of a locally cartesian closed category, as is done in Gambino and Kock (Reference Gambino and Kock2013). However, it is possible to work in a much more general setting, as is done in Uemura (Reference Uemura2022) and Weber (Reference Weber2015), at the cost of not all polynomial functors existing. This is what we do as well.

Let $\mathcal{C}$ be a category with finite limits. A polynomial over a category $\mathcal{C}$ is a diagram $P$ of the following form.

If $f$ is exponentiable, then the functor $F_P : \mathcal{C}/I \rightarrow \mathcal{C}/J$ given by

is called the polynomial functor associated to $P$ . A functor $F : \mathcal{C}/I \rightarrow \mathcal{C}/J$ is called a polynomial functor if there exists a polynomial $P$ such that $F_P$ exists and $F \cong F_P$ . In this case, we say $P$ represents $F$ . If $F : \mathcal{C} \rightarrow \mathcal{C}$ , then we say it is a polynomial functor if this is the case when using the usual identification between $\mathcal{C}$ and $\mathcal{C}/\unicode {x1D7D9}$ .

2.4 Extensivity

A category is extensive if it has finite coproducts, which are well-behaved; we refer to Carboni et al. (Reference Carboni, Lack and Walters1993) for the precise definition. Since we often assume our categories have finite limits, we use the following characterization, drawn from Proposition 2.2 of Carboni et al. (Reference Carboni, Lack and Walters1993).

Fact 2.1. Let $\mathcal{C}$ be a category with finite limits and finite coproducts. Then, $\mathcal{C}$ is extensive if and only if for every coproduct $X_1 \longrightarrow X_1 + X_2 \longleftarrow X_2$ and any commutative diagram as below,

the squares are pullbacks if and only if the top row is a coproduct.

In particular, in an extensive category, every binary coproduct is universal, which means that its pullback along any arrow is still a coproduct.

3.1 The language for categories with finite products

In this section, we describe the internal language we’ll use for categories with finite products. First, the internal language has a collection of types, which are the objects of $\mathcal{C}$ . It has function symbols of the form $f : A_1 \times \ldots \times A_n \rightarrow B$ , which come from the arrows of $\mathcal{C}$ . Arrows with domain $\unicode {x1D7D9}$ are treated as constant symbols. We inductively build typed terms using variables and these function symbols in the usual way.

Next, a context is a list of variables and their types, such as $C=(x:X, y:Y, z:Z)$ , and we write $[C]$ for $X \times Y \times Z$ . (We omit the types of the variables if they are clear from context.) A context is valid for a term $t$ if all the variables in $t$ occur in $C$ , and the interpretation of a term $t:B$ in a valid context $C$ is an arrow $[t]_C : [C] \rightarrow B$ . This interpretation is defined inductively: for a variable $x_i$ in a context $C=(x_1:X_1, \ldots , x_n:X_n)$ , $[x_i]_C$ is the projection map $\pi _i : [C] \rightarrow X_i$ , and for a term $f(t_1, \ldots , t_n)$ , its interpretation is $f \circ \langle [t_1], \ldots , [t_n] \rangle$ .

Finally, if $t_1, t_2$ are terms in a context $C$ , we write $t_1 =_C t_2$ to mean that $[t_1]_C = [t_2]_C$ (as arrows in $\mathcal{C}$ ). Since this is enough to make sense of the example above with $h(x,y,z)$ , this completes the formal setup of the language. Notably, we don’t use relations, since the usual treatment requires the existence of pullbacks.

Below, we state some basic facts about this language (the only non-trivial rule is the second one, which requires Lemma D1.2.4 in Johnstone (Reference Johnstone2002)).

• • The equality $=_C$ is an equivalence relation.

• • The equality $=_C$ is preserved by substitution: if $a =_C b$ , then $a[\vec {t}/\vec {y}] =_C b[\vec {t}/\vec {y}]$ , and if $t_i =_C s_i$ for each $i$ , then $a[\vec {t}/\vec {y}] = a[\vec {s}/\vec {y}]$ .

• • Given arrows $f,g : X_1 \times \ldots \times X_n \rightarrow Y$ and the context $\vec {x} = (x_1 : X_1, \ldots , x_n : X_n)$ , we have $f=g$ if and only if $f(x_1, \ldots , x_n) =_{\vec {x}} g(x_1, \ldots , x_n)$ .

• • For any appropriate arrows $f, (g_i)_{i=1}^m, (h_j)_{j=1}^n$ , terms $(t_i)_{i=1}^m$ , and context $C$ , we have

  \begin{equation*} f(g_1(t_1, \ldots , t_n), \ldots , g_m(t_1, \ldots , t_n)) =_C (f \circ \langle g_1, \ldots , g_m \rangle )(t_1, \ldots , t_n) \end{equation*}
  and
  \begin{equation*} f(h_1(t_1), \ldots , h_n(t_n)) =_C (f \circ (h_1 \times \ldots \times h_n))(t_1, \ldots , t_n). \end{equation*}
  In particular, $f(g(t)) =_C (f \circ g)(t)$ .

Finally, given two terms $a:A$ , $b:B$ in a context $C$ , we can let $(a,b)$ be shorthand for the term ${\operatorname {Id}}_{A \times B}(a,b)$ (and similarly for products of any length). Since $(a,b) : A \times B$ , this notation lets us mimic products of types without having to build them into the language. Remark that $[(a,b)]_C = \langle [a]_C, [b]_C \rangle$ , as we’d expect. In particular, if we have an arrow $g : A \times B \rightarrow X$ , then $g((a,b)) =_C g(a,b)$ , and so we will not bother to distinguish between these terms.

3.2 Additional notation for categories with finite limits

In this section, we augment our internal language with some notation that makes it easier to work in categories with finite limits.

3.2.1. Contexts for equalizers

Suppose we have a context $D = (y_1 : Y_1, \ldots , y_n : Y_n)$ and terms $s,t : Z$ in the context $D$ . Then, we can form the following equalizer diagram.

We will write $\{y_1 : Y_1, \ldots , y_n : Y_n \mid s=t\}$ as notation for the object $E$ , and we will write $(y_1 : Y_1, \ldots , y_n : Y_n \mid s=t)$ or $(D \mid s=t)$ as notation for the context $D' = (e:E)$ . This makes it easier to refer to equalizers without using new variable names; for example, the context for a pullback of $f : U \rightarrow W$ , $g : V \rightarrow W$ is $(u:U, \, v:V \mid f(u) = g(v))$ .

A key point here is that $y_1, \ldots , y_n$ , as well as $s$ and $t$ , can be considered terms in the context $D' = (y_1, \ldots , y_n \mid s = t)$ . Indeed, any terms in the context $D$ can be also considered to be terms in $D'$ , simply by “pulling back” along the inclusion map $i : [D'] \rightarrow [D]$ . Explicitly, if $i = \langle i_1, \ldots , i_n \rangle$ , then the variable $y_k$ is considered shorthand for $i_k(e)$ . Note that, if we view $s,t$ as terms in $D'$ , then we have $s =_{D'} t$ .

3.2.2. Obtaining terms in the equalizer

Since the equalizer $E$ is thought of as a subset of $[D]$ , we want to be talk about “terms of type $E$ ” and “terms of type $[D]$ which equalize $s$ and $t$ ” interchangeably. This will require us to abuse notation in the following ways. First, if we have a term $e : E$ , then we can also think of it as the term $i(e) : [D]$ . So, we may write $e : [D]$ to refer to this term.

Second, if we have terms $u_1 : Y_1, \ldots , u_n : Y_n$ in a context $C = (\vec {x} : \vec {X})$ , then the term $(u_1, \ldots , u_n)$ is formally of type $[D]$ . However, if $s[\vec {u}/\vec {y}] =_C t[\vec {u}/\vec {y}]$ , then the universal property of the equalizer tells us there is a unique term $u : E$ such that $i(u) = (u_1, \ldots , u_n)$ . Thus, we write $(u_1, \ldots , u_n) : E$ as shorthand for $u : E$ .

It is important to note that these two ways of abusing notation are compatible with each other. On one hand, if $(u_1, \ldots , u_n) : [D]$ equalizes $s$ and $t$ , then $i(u_1, \ldots , u_n) =_C (u_1, \ldots , u_n)$ as terms of type $[D]$ ; on the other hand, if $e : E$ , then $i(e) =_C e$ as terms of type $E$ (these are easy to check).

Finally, we remark that the latter notation behaves well with respect to substitution. That is, with the above setup, if we let $w_1 : X_1, \ldots , w_m : X_m$ be terms in another context $B$ , then

\begin{align*} (u_1, \ldots , u_n)[\vec {w}/\vec {x}] =_B (u_1[\vec {w}/\vec {x}], \ldots , u_n[\vec {w}/\vec {x}]) \quad (\text{as terms of type } E). \end{align*}

The proof is straightforward, though it does require Lemma D1.2.4 from Johnstone (Reference Johnstone2002).

3.2.3. Substitution for equalizers

As noted previously, if we have terms $s,t$ in a context $D = (y_1, \ldots , y_n)$ , then we can form the context $D' = (y_1, \ldots , y_n \mid s = t)$ , and we can still view $y_1, \ldots , y_n$ as terms in this context. However, these $y_k$ are no longer variables in the context $D'$ , since formally, $D' = (e : E)$ , where $E$ is the equalizer.

Now, consider a term like $g(y_1, \ldots , y_n)$ in the context $D$ . If we consider this term in the context $D'$ , can we still substitute terms for the variables $y_k$ ? The $y_k$ are no longer variables in the context $D'$ , so this requires special consideration.

Formally, let $r : R$ be a term in the context $D' = (e : E) = (y_1, \ldots , y_n \mid s = t)$ , and let $u_1 : Y_1, \ldots , u_n : Y_n$ be terms in a context $C$ . If we assume that $s[\vec {u}/\vec {y}] =_C t[\vec {u}/\vec {y}]$ , then we can say that

\begin{align*} r[\vec {u}/\vec {y}] \text{ is shorthand for } r[\vec {u}/e], \end{align*}

where on the right side, $\vec {u} = (u_1, \ldots , u_n)$ is considered to be of type $E$ by our previous abuse of notation. This definition ensures that our substitution notation enjoys many of the same properties of regular substitution, and it behaves the way: we have $y_k[\vec {u}/\vec {y}] =_C u_k$ (the proof is straightforward).

4.1 Natural numbers objects and arithmetic

We start this section by recalling the standard definition of natural numbers objects, which can be found in Román (Reference Román1989), for one.

This definition uses our internal language (see Section 3); the definition is given diagrammatically in Román (Reference Román1989). Following the convention of Román (Reference Román1989), the term “natural numbers object” will always refer to parametrized natural numbers objects; we will not discuss unparametrized NNOs (where we omit the parameter $A$ in the definition).

It’s helpful to have the following formulation of the universal property that uses the internal language even more (we omit the easy proof). It avoids the need to think of the terms $f, f_1, f_2, g, h$ as coming from arrows and is more true to how calculations are performed in Román (Reference Román1989).

The NNO property lets us define the operations of addition $+ : N \times N \rightarrow N$ , multiplication $\bullet : N \times N \rightarrow N$ , predecessor $P : N \rightarrow N$ , and (truncated) subtraction $\mathrel {\substack {\cdot \\[-1ex]-}} : N \times N \rightarrow N$ in the usual inductive way (see A2.5.4 of Johnstone (Reference Johnstone2002) for the full definitions). The operations $+$ and $\bullet$ , along with $0$ and $1 = s0$ , make $N$ into an (internal) commutative semiring. More properties of these operations can be found in Román (Reference Román1989) (themselves inspired by Goodstein (Reference Goodstein1957)), and we prove some additional facts in Appendix A. We also record the following fact (see, e.g., Johnstone (Reference Johnstone2002), Lemma A2.5.5]).

4.2 Order in NNOs

Relations, such as inequality for natural numbers, are usually represented as subobjects and integrated into the internal language of a category. For natural numbers objects, the inequality relation ( $\leq$ ) is given by the subobject $N \times N \hookrightarrow N \times N : (m,n) \mapsto (m,m+n)$ , and strict inequality ( $\lt$ ) is given by the subobject $N \times N \hookrightarrow N \times N : (m,n) \mapsto (m,sm+n)$ (see Román (Reference Román1989), Section 3]).

However, relations in the internal language require pullbacks to be interpreted (Johnstone Reference Johnstone2002, Definition D1.2.6), which we are avoiding for this section. Instead, for this paper, we will use the following notation to express inequalities. Given two terms $x,y : N$ in a context $C$ , we write $x \leq _C y$ to mean that $x \mathrel {\substack {\cdot \\[-1ex]-}} y =_C 0$ , and we write $x \lt _C y$ to mean $s(x) \mathrel {\substack {\cdot \\[-1ex]-}} y =_C 0$ . This lets us write things like $a \lt _a a+1$ .

The justification for this approach is that the subobject that defines inequality (given by $(m,n) \mapsto (m,m+n)$ ) is precisely the equalizer of the maps $(x,y) \mapsto x \mathrel {\substack {\cdot \\[-1ex]-}} y$ and $(x,y) \mapsto 0$ . In particular, $x \leq _C y$ implies both that $x \mathrel {\substack {\cdot \\[-1ex]-}} y =_C 0$ and that there is a term $k$ such that $x+k = y$ . (The analogous fact is true for strict inequality.) However, while this fact seems implicit in the proof of Proposition 3.2 in Román (Reference Román1989), we could not find it stated explicitly. In Appendix A, we show this result (Corollary A.3) and other useful facts about our version of inequality.

We also use inequalities when defining equalizers in our internal language; for instance, we will write $\{m:N, n:N \mid m \lt n\}$ instead of $\{m:N, n:N \mid (sm \mathrel {\substack {\cdot \\[-1ex]-}} n) = 0\}$ . Finally, we record the following proposition; it follows directly from Appendix A, but we single it out since we will use it several times.

4.3 Definition by cases in NNOs

In this section, we’ll establish some notation for defining functions by cases. For instance, if we have a term $n : N$ in a context $C$ , we may like to define an arrow $[C] \rightarrow X$ that splits into cases $n=0$ and $n\gt 0$ . In an extensive category with finite limits, this can be done by writing $[C]$ as a coproduct (as is done in Section 6.1), but this is not possible in a general category with finite products. Fortunately, we can use an alternative, which we describe below.

Given an object $X$ , define the function $ITE_X : X \times X \times N \rightarrow X$ (short for “if-then-else”) by induction as follows:

\begin{align*} ITE_X(x,y,0) =_{x,y} x, \quad ITE_X(x,y,sn) =_{x,y,n} y. \end{align*}

We will use the following special notation for this function.

\begin{align*} ITE_X(x,y,n) =_{x,y,n} \left \{\begin{matrix} x\;\;\;\;\; & \text{if } n=0 \\ y\;\;\;\;\; & \text{else} \end{matrix}\right . \end{align*}

If we substitute the variables $x,y,n$ by general terms in a context $C$ , we obtain a function $[C] \rightarrow X$ , as desired.

We make this notation a bit more flexible in two ways. First, when considering more than one case at a time, we’ll write

\begin{align*} \left \{\begin{matrix} x\;\;\;\;\; & \text{if } m=0 \\ y\;\;\;\;\; & \text{else if } n=0 \\ z\;\;\;\;\; & \text{else} \end{matrix}\right \} =_{x,y,z,m,n} \left \{\begin{matrix} x\;\;\;\;\; & \text{if } m=0 \\ \left \{\begin{matrix} y\;\;\;\;\; & \text{if } n=0 \\ z\;\;\;\;\; & \text{else} \end{matrix}\right \} & \text{else} \end{matrix}\right \}\!. \end{align*}

Second, if we want our condition to look like $m \leq n$ instead of $n = 0$ , we use the following shorthand (and similarly for $m\lt n$ ).

\begin{align*} \left \{\begin{matrix} x\;\;\;\;\; & \text{if } m \leq n \\ y\;\;\;\;\; & \text{else} \end{matrix}\right \} =_{x,y,m,n} \left \{\begin{matrix} x\;\;\;\;\; & \text{if } (m \mathrel {\substack {\cdot \\[-1ex]-}} n)=0 \\ y\;\;\;\;\; & \text{else} \end{matrix}\right \} \end{align*}

4.4 The generic finite cardinal

A key part of Theorem 1.1 is the arrow $\pi _2^E : E \rightarrow N$ . In the category of sets, we said that $E = \{(m,n) \in \mathbb{N} \times \mathbb{N} : m \lt n\}$ , and this carries over nicely to a category with finite limits and a natural numbers object $N$ , where we set

\begin{align*} E = \{m : N, \, n : N \mid m\lt n \}. \end{align*}

(Here, we use notation from Sections 3.2 and 4.2; explicitly, $E$ is the equalizer of the arrows $N \times N \rightarrow N$ given by $(m,n) \mapsto s(m) \mathrel {\substack {\cdot \\[-1ex]-}} n$ and $(m,n) \mapsto 0$ .) Now, if we write $D$ for the context $(m : N, \, n : N \mid m\lt n)$ (remark that $[D] = E$ ), then we can define the map $\pi _2^E : E \rightarrow N$ by $\pi _2^E(m,n) =_D n$ . This arrow is sometimes called the generic finite cardinal (e.g., section A2.5 of [John 02]). Going forward, we’ll write $E$ , $\pi _2^E$ to refer to this object without mentioning it explicitly.

4.5 List objects

In this section, we introduce list objects and give some basic properties. List objects in the context of category theory originated with Cockett in 1990 and have since received considerable attention. They have notably been used to develop the theory of shapely functors (Jay Reference Jay1993a, Reference Jay1995; Jay et al. Reference Jay and Cockett1994; Moggi et al. Reference Moggi, Bellè and Jay1999) and are usually studied when the ambient category is a locos: an extensive category with finite limits and list objects. List objects have been used to study finiteness in a locos (Jay Reference Jay1997) and are used in Maietti (Reference Maietti2010) to define arithmetic universes. Owing to their roots in computer science, list objects are also studied from the perspective of datatypes in, for example, Abbott et al. (Reference Abbott, Altenkirch, Ghani and Gordon2003) and Abbott et al. (Reference Abbott, Altenkirch and Ghani2005), where they are examples of initial algebras and strictly positive types. List objects have even been generalized to monoidal categories (see Jay (Reference Jay1993b) and Fiore and Saville (Reference Fiore, Saville and Miller2017)); the free monoid functor, closely related to lists, can be constructed in certain cases when the category has countable coproducts (Lack Reference Lack2010).

List objects are defined as follows. As with natural numbers objects, “list object” will always mean the parametrized version.

Definition 4.4. Let $\mathcal{C}$ be a category with finite products, and let $X \in \mathcal{C}$ be an object. A $\text{(parametrized) list object}$ on $X$ is a triple $(L(X), r_0^X, r_1^X)$ consisting of an object $L(X)$ and arrows $r_0^X : \unicode {x1D7D9} \rightarrow L(X)$ , $r_1^X : X \times L(X) \rightarrow L(X)$ , which satisfy the following property.

For any objects $A,B$ and arrows $g : A \rightarrow B$ , $h : X \times B \rightarrow B$ , there exists a unique arrow $f : A \times L(X) \rightarrow B$ , which makes the following diagrams commute. (Here, $\sigma$ is the obvious isomorphism $A \times (X \times L(X)) \rightarrow X \times (A \times L(X))$ .)

It is much easier to write these diagrams equationally. By writing $\varnothing$ for $r_0^X$ and $x :: \ell$ for $r_1^X(x,\ell )$ , the diagrams become the equations $f(a,\varnothing ) =_a g(a)$ and $f(a, x :: \ell ) =_{a,x,\ell } h(x,f(a,\ell ))$ ; we’ll also use the notation $[x]$ to denote the list $x :: \varnothing$ . A version of the universal property with terms can also be formulated, like for natural numbers objects (see Section 4.1 ).

The list object property can actually be generalized slightly to the following proposition. We have not found this result stated in the literature, but it seems to be used implicitly in Jay (Reference Jay1997), for instance. We use it to define the truncation arrow in Section 4.6.

From this proposition, it becomes clear that $L(\unicode {x1D7D9})$ is a (parametrized) natural numbers object, so it is redundant to assume that a category has list objects and a natural numbers object. Moreover, similarly to natural numbers objects, list objects can be expressed as a coproduct. (This is noted in section 2 of Jay et al. (Reference Jay and Cockett1994); it follows directly from the universal property.)

Finally, if a category $\mathcal{C}$ with finite products has all list objects, then we can form a functor $L : \mathcal{C} \rightarrow \mathcal{C}$ , which maps $X$ to the list object $L(X)$ . Its action on arrows is defined as follows: given $f : X \rightarrow Y$ , we define $L(f) : L(X) \rightarrow L(Y)$ inductively by

\begin{align*} L(f)(\varnothing ) = \varnothing \quad \text{and} \quad L(f)(x :: \ell ) =_{x,\ell } f(x) :: L(f)(\ell ). \end{align*}

The arrow $L(f)$ is also denoted $\texttt {map}(f)$ in Jay (1994).

4.6 Important list arrows

In this section, we define some important arrows related to list objects and prove some properties about them. Throughout, we assume we are working in a category $\mathcal{C}$ with finite products and parametrized list objects (and therefore a parametrized NNO).

Most of these definitions and results are not original: many of them appear in the existing literature on list objects (briefly surveyed in Section 4.5). Some of the notation comes from functional programming (in Jay et al. (Reference Jay and Cockett1994), the authors note that some of their notation is from Bird and Wadler (Reference Bird and Wadler1988)), while some of the results are inspired by the Rocq standard library for lists (Rocq 2025). However, in many cases, the definitions and results are either used implicitly or proved under different assumptions. Therefore, we restate the parts we’ll need and compare to the literature when possible.

We start with the definitions. These operators are all indexed by an object $X$ , but we remove this index if it is clear from context.

• • The length arrow, ${\operatorname {len}}_X : L(X) \rightarrow N$ , is defined inductively by the equations ${\operatorname {len}}_X(\varnothing ) = 0$ and ${\operatorname {len}}_X(x :: \ell ) =_{x,\ell } s({\operatorname {len}}_X(\ell ))$ .

• • The list concatenation arrow, $\mathbin {+\mkern -2mu+}_X : L(X) \times L(X) \rightarrow L(X)$ , is defined inductively by $\varnothing \mathbin {+\mkern -2mu+}_X \ell _2 =_{\ell _2} \ell _2$ and $(x :: \ell _1) \mathbin {+\mkern -2mu+}_X \ell _2 =_{x,\ell _1,\ell _2} x :: (\ell _1 \mathbin {+\mkern -2mu+}_X \ell _2)$ .

• • The truncate arrow, ${\operatorname {tr}}_X : L(X) \rightarrow L(X)$ , is the arrow that removes the leading element from a list. It is defined inductively by ${\operatorname {tr}}_X(\varnothing ) = \varnothing$ and ${\operatorname {tr}}_X(x :: \ell ) =_{x,\ell } \ell$ .

• • The tail arrow, ${\operatorname {tail}}_X : N \times L(X) \rightarrow L(X)$ , is an arrow, which iterates truncation: ${\operatorname {tail}}_X(n,\ell )$ returns the list $\ell$ with the $n$ leading elements removed. It is defined inductively by ${\operatorname {tail}}_X(0,\ell ) =_\ell \ell$ and ${\operatorname {tail}}_X(s(n), \ell ) =_{n,\ell } {\operatorname {tr}}_X({\operatorname {tail}}_X(n,\ell ))$ .

• • The zeroth-or-default arrow, ${\operatorname {zerothDef}}_X : X \times L(X) \rightarrow X$ , is an arrow that takes a pair $(x,\ell )$ as input. If $\ell$ is a nonempty list, it returns its leading element; however, if $\ell$ is empty, it returns $x$ , the “default” element. This arrow is defined inductively by ${\operatorname {zerothDef}}_X(x,\varnothing ) =_x x$ and ${\operatorname {zerothDef}}_X(x, y :: \ell ) =_{x,y,\ell } y$ .

• • The nth-or-default arrow, ${\operatorname {nthDef}}_X : X \times N \times L(X) \rightarrow X$ , is an arrow that takes a triple $(x,n,\ell )$ as input. It returns the $n^{th}$ element of $\ell$ if $n \lt {\operatorname {len}}(\ell )$ , and otherwise it returns a default. It is defined by ${\operatorname {nthDef}}_X(x,n,\ell ) =_{x,n,\ell } {\operatorname {zerothDef}}_X( x, \; {\operatorname {tail}}_X(n, \ell ))$ .

The length and concatenation arrows appear (for instance) in Jay et al. (Reference Jay and Cockett1994), where they are denoted $\#$ and $@$ ; the truncate and tail arrows appear in Jay (Reference Jay1997), with the names tail and take; the $\operatorname {zerothDef}$ and $\operatorname {nthDef}$ maps appears in Rocq (2025) as hd and nth. Note that we say “the zeroth element” for the leading element for consistency with “the $n^{th}$ element”.

Next, we establish some propositions about these maps. First, we have a naturality result; versions of these results are found in Rocq (2025).

Next, we have some results about how the concatenation and tail relate to the length arrow. We have not found them stated explicitly in the literature, but they are not new either: the first equality is used implicitly in a diagram in section 4 of Jay et al. (Reference Jay and Cockett1994), and a version of the second equality appears in Proposition5.2 of Cockett (Reference Cockett1990). They also appear in Rocq (2025).

The next proposition shows how to decompose list objects based on their length. We draw particular attention to the second case: we would like to decompose a list $t : L(X)$ of positive length into $t = x :: t'$ , but we cannot extract a term of type $X$ from the context $(\ell : L(X) \mid {\operatorname {len}}(\ell ) \gt 0)$ without additional assumptions (see Propositions 6.1 and 7.1). So, in order to perform the decomposition, we need to be given an arbitrary term ${\operatorname {def}} : X$ . Hence, these results are standard for locoi, but we have not seen a proof in the literature for categories with only finite products and list objects.

Proof. For the first point, consider the map $Z : N \times L(X) \rightarrow L(X)$ defined inductively by $Z(0,\ell ) =_{\ell } \varnothing$ , $Z(sn,\ell ) =_{n,\ell } \ell$ . By induction on $\ell$ , it is easy to show that $Z({\operatorname {len}}(\ell ), \ell ) =_\ell \ell$ . We conclude by using the hypothesis ${\operatorname {len}}(t) =_C 0$ to compute

\begin{align*} t =_C Z({\operatorname {len}}(t), t) =_C Z(0,t) =_C \varnothing , \end{align*}

as desired.

For the second point, we similarly consider an arrow $Z : X \times N \times L(X) \rightarrow L(X)$ defined by $Z(x,0,\ell ) =_{x,\ell } \varnothing$ and $Z(x,sn,\ell ) =_{x,n,\ell } {\operatorname {zerothDef}}(x,\ell ) :: {\operatorname {tr}}(\ell )$ . As before, we can easily show by induction that $Z(x, {\operatorname {len}}(\ell ), \ell ) =_{x,\ell } \ell$ . Now, if ${\operatorname {len}}(t) \gt _C 0$ , then ${\operatorname {len}}(t) =_C s(n)$ for some $n : N$ (by Proposition 4.3). If, moreover, we have some ${\operatorname {def}} : X$ , then

\begin{align*} t =_C Z({\operatorname {def}}, {\operatorname {len}}(t), t) =_C Z({\operatorname {def}}, s(n), t) =_C {\operatorname {zerothDef}}({\operatorname {def}},t) :: {\operatorname {tr}}(t), \end{align*}

as desired.

For the third point, consider the term ${\operatorname {zerothDef}}(x,t)$ . If we substitute the equality $t =_C {\operatorname {zerothDef}}(x',t) :: {\operatorname {tr}}(t)$ (which holds by the second point) and simplify, we get the desired result.

Finally, we have some results about the behavior of $\operatorname {nthDef}$ . They tell us that if $n \geq {\operatorname {len}}(\ell )$ , then $\operatorname {nthDef}$ returns the default, and if $n \lt {\operatorname {len}}(\ell )$ , then the default is irrelevant. Again, these do not seem to appear explicitly in the literature (except Rocq (2025)), and there is perhaps some novelty in establishing these results when only working in a category with finite products and list objects.

Proof. For the first point, we have ${\operatorname {len}}({\operatorname {tail}}(n,\ell )) =_C {\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} n =_C 0$ by Proposition 4.8 and the assumption $n \geq _C {\operatorname {len}}(\ell )$ ; thus, ${\operatorname {tail}}(n,\ell ) =_C \varnothing$ by Proposition 4.9. So, by definition of $\operatorname {nthDef}$ , we have

\begin{align*} {\operatorname {nthDef}}(x,n,\ell ) =_C {\operatorname {zerothDef}}(x, \; {\operatorname {tail}}(n,\ell )) =_C {\operatorname {zerothDef}}(x, \varnothing ) =_C x. \end{align*}

This is what we wanted.

For the second point, by Proposition A.5 from the appendix, $n\lt _C {\operatorname {len}}(\ell )$ implies that ${\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} n \gt _C 0$ , so

\begin{align*} {\operatorname {len}}({\operatorname {tail}}(n,\ell )) =_C {\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} n \gt _C 0 \end{align*}

by Proposition 4.8. Then, by Proposition 4.9, we have

\begin{align*} {\operatorname {nthDef}}(x,n,\ell ) &=_C {\operatorname {zerothDef}}(x, {\operatorname {tail}}(n,\ell )) \\ &=_C {\operatorname {zerothDef}}(x', {\operatorname {tail}}(n,\ell )) =_C {\operatorname {nthDef}}(x',n,\ell ), \end{align*}

as desired.

6.1 Rephrasing the hypotheses

Hypotheses (H1) and (H2) are not easy to apply directly when doing proofs with the internal language. In this section, we obtain consequences of these hypotheses that can be applied to the internal language. We start with (H1), which is fairly easy to adapt.

Proof. Since ${\operatorname {len}}(\ell ) \gt _C 0$ , we have ${\operatorname {len}}(\ell ) =_C s(P({\operatorname {len}}(\ell )))$ by Proposition 4.3, which means the following diagram commutes.

Since (H1) asserts that this square is a pullback, there exists an arrow $\gamma : [C] \rightarrow X \times L(X)$ , which makes the whole diagram commute. So, if we write $C = (y_1 : Y_1, \ldots , y_n : Y_n)$ and we let $x =_C \pi _1(\gamma (y_1, \ldots , y_n))$ and $\ell ' =_C \pi _2(\gamma (y_1, \ldots , y_n))$ , then the equality $[\ell ]_C = r_1^X \circ \gamma$ implies $\ell =_C x :: \ell '$ , as desired.

Next, we move on to (H2). This hypothesis is used when we need to perform a construction or calculation “by cases,” depending on whether a certain parameter is zero or nonzero (e.g., the proof of Theorem 8.6); the following proposition makes this easier to do.

Proof. Write $i_0, i_{\gt 0}$ for the inclusion maps of $[C_0], [C_{\gt 0}]$ into $[C]$ , respectively, and consider the following diagram.

We claim that this diagram commutes and that the squares are pullbacks. If this is true, then hypothesis (H2) tells us that the top row is a coproduct, as desired.

First, we check that the squares commute. The left square states that, in the context $C_0$ , $t =_{C_0} 0$ , which is true by definition. The right square states that, in the context $C_{\gt 0}$ , $t =_{C_{\gt 0}} s(P(t))$ . We know $t \gt 0$ in this context, so the equality follows by Proposition 4.3.

Second, we claim that the left square is a pullback because of how $[C_0]$ is defined as an equalizer, and the right square is a pullback because of how $[C_{\gt 0}]$ is defined as an equalizer. This is mostly a routine check, so we omit the details. We just note that for the latter case, if $f : B \rightarrow [C]$ and $g : B \rightarrow N$ are such that $[t]_C \circ f = s \circ g$ , then $[t]_C \circ f \gt 0$ (by Proposition 4.3) and $g = P \circ [t]_C \circ f$ .

The conclusion of this proposition can be reformulated using the internal language so that it is easier to use.

We will generalize the above result slightly. Instead of splitting into the case $t=0$ and $t\gt 0$ , we will split into the case $u\lt w$ and $u \geq w$ . Note that the conclusion of this generalization can also be phrased using terms as in the above remark; we won’t rewrite it in full.

Proof. Remark that $C_2 = (C \mid w \mathrel {\substack {\cdot \\[-1ex]-}} u = 0)$ . So, if we let $C_{\gt 0} = (C \mid w \mathrel {\substack {\cdot \\[-1ex]-}} u \gt 0)$ , then by Proposition 6.2, the following diagram is a coproduct.

So, to show the result we want, we need to show that there is an isomorphism $[C_1] \cong [C_{\gt 0}]$ that respects the inclusion into $[C]$ .

The only choice for an isomorphism between the objects $[C_1] = \{C \mid u \lt w\}$ and $[C_{\gt 0}] = \{C \mid w \mathrel {\substack {\cdot \\[-1ex]-}} u \gt 0\}$ which respects the inclusion into $[C]$ is the “identity map” $(x_1, \ldots , x_n) \mapsto (x_1, \ldots , x_n)$ . Therefore, we just need to show that this map is well-defined in both directions. This just involves showing that $w \mathrel {\substack {\cdot \\[-1ex]-}} u \gt _{C_1} 0$ (knowing that $u \lt _{C_1} w$ ) and that $u \lt _{C_{\gt 0}} w$ (knowing that $w \mathrel {\substack {\cdot \\[-1ex]-}} u \gt _{C_{\gt 0}} 0$ ). This is true by Proposition A.5 of the appendix.

6.2 Pullbacks along E

As we saw in Proposition 5.1, a central part of our proof strategy is the functor $\Sigma _E \circ \Delta _{\pi _2^E} : \mathcal{C}/N \rightarrow \mathcal{C}$ , which maps an arrow $l_A : A \rightarrow N$ to the object $E \times _N A$ defined by the following pullback.

Using the internal language, we have $E \times _N A = \{e : E, \, a : A \mid \pi _2^E(e) = l_A(a) \}$ . Since $E$ is the object $\{m : N, n : N \mid m \lt n\}$ , we could also write this as $\{(m,n) : E, \, a : A \mid n = l_A(a)\}$ . However, this shows us that the “ $n$ ” parameter is redundant, and that we can just think of this object as $\{m : N, \, a : A \mid m \lt l_A(a)\}$ . Specifically, we’d like to use the context $(m:N, a:A \mid m \lt l_A(a))$ when referencing the object $E \times _N A$ . The following proposition assures us that this is valid.

Proposition 6.4. Let $\mathcal{C}$ be a category with finite limits and a parametrized NNO, and let $l_A : A \rightarrow N$ . Then, the following maps are well-defined and provide an isomorphism $E \times _N A \cong \{m : N, \, a : A \mid m \lt l_A(a)\}$ .

Note that we do need to be careful when writing $\{m : N, a : A \mid m \lt l_A(a)\}$ for $E \times _N A$ , because applying the projection maps does not behave the way we expect. For instance, we have the map $\pi _1^{E,A} : E \times _N A \rightarrow E$ , and if we consider $(m,a) : E \times _N A$ with $m : N, a : A$ , then $\pi _1^{E,A}(m,a)$ is not equal to $m$ , as we might think if we’re not being careful.

Fortunately, this issue does not come up very often. We’ll only need the following fact to assure us that we aren’t making mistakes (the proof is a straightforward check, so we omit it).

Fact 6.5. Let $\mathcal{C}$ be a category with finite limits and a parametrized NNO, and suppose we have arrows $l_A : A \rightarrow N$ , $l_B : B \rightarrow N$ and $f : A \rightarrow B$ . Assume $l_B \circ f = l_A$ , so that we can consider the following arrow.

Then, in the context $C = (m : N, a : A \mid m \lt l_A(a))$ , we have

\begin{align*} ({\operatorname {Id}}_E \times _N f)(m,a) =_C (m,f(a)). \end{align*}

6.3 Converting a finite sequence to an infinite sequence

In the proof outline of Section 5, we saw that we need to use an arrow $g : E \times _N A \rightarrow X$ to produce an arrow $A \rightarrow L(X)$ . As we’ll see in Section 8.3, a key technical step in this process will be obtaining an intermediate arrow $g' : N \times [A_{\gt 0}] \rightarrow X$ , where $A_{\gt 0} = (a : A \mid l_A(a)\gt 0)$ . The important property of $g'$ is that it should produce the same output as $g$ , as long as it is acting on inputs $m:N$ , $a:A$ such that $m \lt l_A(a)$ .

In order to obtain the arrow $g'$ we want, we need to introduce an arrow ${\operatorname {IdUntil}} : N \times N \rightarrow N$ , defined by

\begin{align*} {\operatorname {IdUntil}}(m,n) =_{m,n} \min (m, Pn). \end{align*}

Here, $P$ is the predecessor function, and $\min$ is defined as in Román (Reference Román1989, Prop. 1.3). What’s important about $\operatorname {IdUntil}$ is that it has the following properties.

Proof. For the first part, we first note that $n \gt _C 0$ implies $n =_C s(P(n))$ (see Proposition 4.3). Using this and Román (Reference Román1989, Prop. 1.3), we compute

\begin{align*} s ( {\operatorname {IdUntil}}(m,n) ) \mathrel {\substack {\cdot \\[-1ex]-}} n =_C s (\!\min (m,Pn)) \mathrel {\substack {\cdot \\[-1ex]-}} s(P(n)) =_C \min (m,Pn) \mathrel {\substack {\cdot \\[-1ex]-}} Pn. \end{align*}

It is easy to check that $\min (x,y) \mathrel {\substack {\cdot \\[-1ex]-}} y =_{x,y} 0$ (using Román Reference Román1989, Prop. 1.3), so this gives us ${\operatorname {IdUntil}}(m,n) \lt _C n$ , as desired.

For the second part, we note that $n \gt _C 0$ , and so once again $n = s(P(n))$ . The inequality $m \lt _C n$ therefore implies that $m \leq P(n)$ (since $sx \mathrel {\substack {\cdot \\[-1ex]-}} sy =_{x,y} x \mathrel {\substack {\cdot \\[-1ex]-}} y$ ). This fact and Román (Reference Román1989, Prop. 1.3)] let us compute

\begin{align*} {\operatorname {IdUntil}}(m, n) =_C \min\!(m, Pn) =_C m \mathrel {\substack {\cdot \\[-1ex]-}} [m \mathrel {\substack {\cdot \\[-1ex]-}} Pn] =_C m \mathrel {\substack {\cdot \\[-1ex]-}} 0 =_C m. \end{align*}

This is all we needed to show.

We can now use the arrow $\operatorname {IdUntil}$ to obtain $g'$ from $g$ . Essentially, $g'(m,a)$ is equal to $g(m,a)$ for $m \lt l_A(a)$ , and for $m \geq l_A(a)$ , it is just equal to $g(l_A(a) \mathrel {\substack {\cdot \\[-1ex]-}} 1, \, a)$ (which is a valid term because $l_A(a)\gt 0$ , by assumption).

Corollary 6.7. Let $\mathcal{C}$ be a category with finite limits and a parametrized NNO. Let $l_A : A \rightarrow N$ be an arrow, let $C = (m:N, \, a:A \mid m \lt l_A(a))$ , and let $A_{\gt 0} = (a : A \mid l_A(a) \gt 0)$ . Then, for any $g : [C] \rightarrow X$ , the arrow $g' : N \times [A_{\gt 0}] \rightarrow X$ given by

\begin{align*} g'(m,a) =_{m,a} g ( {\operatorname {IdUntil}}(m, l_A(a)), \; a ) \end{align*}

is well-defined. Moreover, in the context $C$ , the term $g'(m,a)$ is well-defined, and

\begin{align*} g'(m,a) =_C g(m,a). \end{align*}

Proof. We start with the first part of the statement. Let $n = {\operatorname {IdUntil}}(m, l_A(a))$ ; we must check that $g(n, a)$ is well-defined (remark that $a : [A_{\gt 0}]$ , but we also write $a$ for its image via the inclusion $[A_{\gt 0}] \hookrightarrow A$ ). Specifically, we need to check that $(n, a)$ is a valid term of type $[C]$ by checking that $n \lt _{m,a} l_A(a)$ . By definition of $A_{\gt 0}$ , we have $l_A(a) \gt _{m,a} 0$ , so we can apply Proposition 6.6 to find that

\begin{align*} n =_{m,a} {\operatorname {IdUntil}}(m, l_A(a)) \lt _{m,a} l_A(a), \end{align*}

as desired.

For the second part, we must check that $g'(m,a)$ is well-defined. In particular, we need to check that the term $a : A$ in the context $C$ can be considered as a term of type $[A_{\gt 0}]$ . This is simple: we have $l_A(a) \gt m \geq 0$ , which is all we need.

Finally, we must check that $g'(m,a) =_C g(m,a)$ . Since $m \lt l_A(a)$ in $C$ , we can apply Proposition 6.6 to get ${\operatorname {IdUntil}}(m, l_A(a)) =_C m$ , and so $g'(m,a) =_C g(m,a)$ , as desired.

8.1 Constructing maps into a list object

The key idea for constructing maps into $L(X)$ is that we should use the inductive property of NNOs. Indeed, suppose we have a map $f : N \times A \rightarrow X$ , which we think of as a collection of infinite sequences $(x_{n,a})_n$ indexed by $a \in A$ . We can use this map to construct the map ${\operatorname {Seq}}[f] : N \times N \times A \rightarrow L(X)$ , where ${\operatorname {Seq}}[f](m,n,a)$ represents $[x_{m,a}, \ldots , x_{m+n-1,a}]$ . This is done by induction on $n$ , the length of this list, as follows.

\begin{align*} {\operatorname {Seq}}[f](m,0,a) =_{m,a} \varnothing && {\operatorname {Seq}}[f](m,s(n),a) =_{m,n,a} {\operatorname {Seq}}[f](m,n,a) \mathbin {+\mkern -2mu+} [f(m+n,a)] \end{align*}

If we are also given a map $p : A \rightarrow N$ that represents the length of a list associated to $a$ , then we can define ${\operatorname {List}}[f,p] : A \rightarrow L(X)$ by setting

\begin{align*} {\operatorname {List}}[f,p](a) =_a {\operatorname {Seq}}[f](0, p(a), a). \end{align*}

Intuitively, we have ${\operatorname {List}}[f,p](a) = [x_{0,a}, \ldots , x_{p(a)-1,a}]$ . The drawback of this technique is that it requires an infinite sequence $(x_{n,a})_n$ to specify this finite list; we address this issue in Section 8.3.

We end this section with some very basic facts about this construction.

8.2 The nth elements of constructed lists

In this section, we prove an important result about the interaction between $\operatorname {nth}$ and ${\operatorname {List}}[f,p]$ : specifically, we show with Theorem 8.5 that the $m^{th}$ element of ${\operatorname {List}}[f,p](a)$ is $f(m,a)$ , as long as $m\lt p(a)$ .

We start with some intermediate results. The first thing we need to do is investigate the interaction between truncation and ${\operatorname {Seq}}[f]$ because $\operatorname {nthDef}$ is built using $\operatorname {tr}$ , and $\operatorname {List}$ is built using $\operatorname {Seq}$ . Recall that $P$ represents the predecessor function.

Proof. By induction on $n$ , it suffices to show that the arrows agree on $0$ and $s$ . For the base case, it’s clear that both terms reduce to $\varnothing$ ; for the inductive case, we use Proposition 8.2:

\begin{align*} {\operatorname {tr}}({\operatorname {Seq}}[f](m,sn,a)) =_{m,n,a} {\operatorname {tr}}(f(m,a) :: {\operatorname {Seq}}[f](sm,n,a)) =_{m,n,a} {\operatorname {Seq}}[f](sm,n,a), \\ {\operatorname {Seq}}[f](sm,Psn,a) =_{m,n,a} {\operatorname {Seq}}[f](sm,n,a). \end{align*}

This is all we need to show.

From this fact, we expect that iterating the truncation map just turns into iterating the successor $s$ and predecessor $P$ . However, iterating the successor just becomes addition, and iterating the predecessor just becomes subtraction. This observation gives us the following important lemma.

Lemma 8.4. Let $f : N \times A \rightarrow X$ . Then,

\begin{align*} {\operatorname {tail}} (k, \; {\operatorname {Seq}}[f](m,n,a) ) =_{k,m,n,a} {\operatorname {Seq}}[f] (m+k, \; n \mathrel {\substack {\cdot \\[-1ex]-}} k, \; a ). \end{align*}

In particular, given $p : A \rightarrow N$ , we have

\begin{align*} {\operatorname {tail}} (k, \; {\operatorname {List}}[f,p](a) ) =_{k,a} {\operatorname {Seq}}[f] (k, \; p(a) \mathrel {\substack {\cdot \\[-1ex]-}} k, \; a ). \end{align*}

Proof. We start with the first equality, which we prove by induction on $k$ . To this end, we show that both arrows satisfy the equalities $h(0,m,n,a) =_{m,n,a} {\operatorname {Seq}}[f](m,n,a)$ and $h(sk,m,n,a) =_{k,m,n,a} {\operatorname {tr}}(h(k,m,n,a))$ . The first equality is trivial, since ${\operatorname {tail}}(0,\ell ) =_\ell \ell$ , $m+0 =_m m$ , and $n \mathrel {\substack {\cdot \\[-1ex]-}} 0 =_n n$ . The second equality is immediate for the left-hand side function (it’s the definition of $\operatorname {tail}$ ); for the right-hand side function, we use Proposition 8.3.

\begin{align*} {\operatorname {Seq}}[f] (m+sk, \; n \mathrel {\substack {\cdot \\[-1ex]-}} sk, \; a ) &=_{k,m,n,a} {\operatorname {Seq}}[f] (s(m+k), \; P(n \mathrel {\substack {\cdot \\[-1ex]-}} k), \; a ) ) \\ &=_{k,m,n,a} {\operatorname {tr}} ( {\operatorname {Seq}}[f] ( m+k, \; n \mathrel {\substack {\cdot \\[-1ex]-}} k, \; a ) ) \end{align*}

This is all we needed to show for the first part. For the second part, we simply replace $m$ by $0$ and $n$ by $p(a)$ , then use the definition of ${\operatorname {List}}[f,p]$ .

Finally, we arrive at the desired result. Note that we need to assume hypothesis (H1) and the existence of finite limits in order to talk about the $\operatorname {nth}$ arrow.

Theorem 8.5. Let $\mathcal{C}$ be a category with finite limits and parametrized list objects and assume (H1). Let $f : N \times A \rightarrow X$ and $p : A \rightarrow N$ and let $m:N$ , $a:A$ be terms in a context $C$ . If $m \lt _C p(a)$ , then

\begin{align*} {\operatorname {nth}}(m, {\operatorname {List}}[f,p](a)) =_C f(m,a). \end{align*}

Proof. First, we note that the term on the left is well-defined because ${\operatorname {len}}({\operatorname {List}}[f,p](a)) =_C p(a)$ (by Proposition 8.1) and $m \lt _C p(a)$ be assumption. Then, by the definition of $\operatorname {nth}$ and Lemma 8.4,

\begin{align*} {\operatorname {nth}}(m, {\operatorname {List}}[f,p](a)) &=_C {\operatorname {nthDef}}({\operatorname {def}}_X', m, {\operatorname {List}}[f,p](a)) \\ &=_C {\operatorname {zerothDef}} ({\operatorname {def}}_X', \; {\operatorname {tail}} (m, \; {\operatorname {List}}[f,p](a) ) ) \\ &=_C {\operatorname {zerothDef}} ({\operatorname {def}}_X', \; {\operatorname {Seq}}[f] (m, p(a) \mathrel {\substack {\cdot \\[-1ex]-}} m, a ) ). \end{align*}

(Here, ${\operatorname {def}}_X'$ is ${\operatorname {def}}_X$ with the appropriate substitution.) Since $m \lt _C p(a)$ by assumption, we have $p(a) \mathrel {\substack {\cdot \\[-1ex]-}} m \gt _C 0$ by Proposition A.5 of the appendix. Therefore, by Proposition 4.3, $p(a) \mathrel {\substack {\cdot \\[-1ex]-}} m =_C s(k)$ for some term $k$ . We substitute this into the above equality, apply Proposition 8.2, and use the definition of $\operatorname {zerothDef}$ . We get:

\begin{align*} {\operatorname {nth}}(m, {\operatorname {List}}[f,p](a)) &=_C {\operatorname {zerothDef}} ({\operatorname {def}}_X', \; {\operatorname {Seq}}[f](m, sk, a) ) \\ &=_C {\operatorname {zerothDef}} ({\operatorname {def}}_X', \; f(m,a) :: {\operatorname {Seq}}[f](sm,k,a) ) =_C f(m,a). \end{align*}

This is what we wanted to show.

8.3 The universal property arrow

The construction ${\operatorname {List}}[f,p]$ allows us to construct an arrow $A \rightarrow L(X)$ based on two arrows $f : N \times A \rightarrow X$ and $p : A \rightarrow N$ . However, the goal stated at the beginning of this chapter is to construct $h : A \rightarrow L(X)$ from $g : E \times _N A \rightarrow X$ and $l_A : A \rightarrow N$ , so we need to adjust this technique. (In this section, we assume our category has finite limits.)

Recall from Proposition 6.4 that $E \times _N A = \{m : N, \, a : A \mid m \lt l_A(a)\}$ . This means that the arrow $g : E \times _N A \rightarrow X$ only gives us finite sequences $(x_{0,a}, \ldots , x_{l_A(a)-1,a})$ instead of the infinite sequences used in ${\operatorname {List}}[f,p]$ . We account for this discrepancy by using two tricks.

• • First, if $l_A(a)\gt 0$ , then we can extend the finite sequence to an infinite one simply by repeating the last element; we will use Corollary 6.7 to do this formally.

• • Second, we note that the first trick doesn’t work if $l_A(a)=0$ , because then $g$ doesn’t give us any elements of $X$ . However, $l_A(a)=0$ just means that we should set $h(a)=\varnothing$ . So, we have to use hypothesis (H2) to split into two cases: $l_A(a)=0$ and $l_A(a)\gt 0$ .

We employ these techniques in the following proof. Note that hypothesis (H1) is required to talk about ${\operatorname {nth}}_X$ .

Proof. Hypothesis (H2) tells us (via Proposition 6.2) that we have the coproduct $A = [A_0] + [A_{\gt 0}]$ , where $A_0 = (a : A \mid l_A(a)=0)$ and $A_{\gt 0} = (a : A \mid l_A(a) \gt 0)$ . This lets us define $h : A \rightarrow L(X)$ by cases on each part of this coproduct.

In the case $l_A(a)=0$ , we simply set $h(a) =_{A_0} \varnothing$ . For the case $l_A(a) \gt 0$ , note that the domain of $g$ is $[C]$ , where $C = (m : N, \, a : A \mid m \lt l_A(a))$ . Then, Corollary 6.7 tells us that there is an arrow $g' : N \times [A_{\gt 0}] \rightarrow X$ such that $g'(m,a) =_C g(m,a)$ , and we can define $h$ in the $A_{\gt 0}$ case to be

\begin{align*} h(a) =_{A_{\gt 0}} {\operatorname {List}}[g', l_A'](a), \end{align*}

where $l_A' : [A_{\gt 0}] \rightarrow N$ is just given by $l_A'(a) =_{A_{\gt 0}} l_A(a)$ . This completes the definition of $h$ ; we must now check that it satisfies the required equalities.

First, we check that ${\operatorname {len}}(h(a)) =_a l_A(a)$ . This can be done by checking equality on both parts of the coproduct. In the $A_0$ case, we have ${\operatorname {len}}(h(a)) =_{A_0} {\operatorname {len}}(\varnothing ) =_{A_0} 0 =_{A_0} l_A(a)$ , and in the $A_{\gt 0}$ case, we have

\begin{align*} {\operatorname {len}}(h(a)) =_{A_{\gt 0}} {\operatorname {len}}({\operatorname {List}}[g', l_A'](a)) =_{A_{\gt 0}} l_A'(a) =_{A_{\gt 0}} l_A(a) \end{align*}

by using Proposition 8.1.

Second, we check that ${\operatorname {nth}}_X(m, h(a)) =_C g(m,a)$ . We could check on both parts of the coproduct, but this would be redundant: the condition $m\lt l_A(a)$ in $C$ implies that we are already in the $A_{\gt 0}$ case. Formally, performing the substitution $a \mapsto a$ in the equation $h(a) =_{A_{\gt 0}} {\operatorname {List}}[g',l_A'](a)$ gives us the equality $h(a) =_C {\operatorname {List}}[g', l_A'](a)$ , and this substitution is valid because $l_A(a) \gt 0$ in $C$ . Using this equality and Theorem 8.5, we compute

\begin{align*} {\operatorname {nth}}_X(m,h(a)) =_C {\operatorname {nth}}_X(m, {\operatorname {List}}[g', l_A'](a)) =_C g'(m, a) =_C g(m,a), \end{align*}

which is what we wanted.

9.1 Equality without extra hypotheses

Our goal for this section is to prove Theorem 9.4 below. Essentially, we want to prove that two lists $h_1, h_2 : A \rightarrow L(X)$ are equal if they have the same length and the same elements. The idea of the proof is to go by induction on their length and show that they are “built up in the same way”.

More specifically, the strategy is as follows. Given arrows $h_1, h_2 : A \rightarrow L(X)$ , we form arrows $H_1, H_2 : N \times A \rightarrow L(X)$ where $H_i(k,a)$ is the list $h_i(a)$ with all but the last $k$ elements removed. We then want to show that $H_1 = H_2$ ; if this is true, then by setting $k = {\operatorname {len}}(h_i(a))$ , we get $h_1(a) = h_2(a)$ , as desired. To show that $H_1 = H_2$ , we go by induction on $k$ : the base case is clear since $H_1(0,a) = H_2(0,a) = \varnothing$ , but the inductive step is more tricky.

For the inductive step, we must analyze the transition from having the last $k$ elements of $h_i$ to having the last $k+1$ elements of $h_i$ . What we’re doing is “adding back” an element to $h_i$ ; specifically, the one in position ${\operatorname {len}}(h_i) \mathrel {\substack {\cdot \\[-1ex]-}} k$ . So, we’d expect to have

\begin{align*} H_i(k+1,a) = {\operatorname {nthDef}}({\operatorname {len}}(h_i(a)) \mathrel {\substack {\cdot \\[-1ex]-}} k, h_i(a)) :: H_i(k,a). \end{align*}

If we’re assuming that $\operatorname {nthDef}$ and $\operatorname {len}$ agree for $h_1$ and $h_2$ , then this gives us a recurrence relation that both $H_1$ and $H_2$ satisfy, and we’re done. However, there’s a problem: $\operatorname {nthDef}$ must include a default parameter. For this reason, $H_i$ must also include a default parameter, making it of the form $H_i(x,k,a)$ . This is why we can only conclude $h_1(a) =_{x,a} h_2(a)$ .

Formalizing this proof idea requires several steps, and we will make heavy use of the if-then-else notation from Section 4.3. First, we must have a better understanding of the arrows $H_i$ . These arrows will involve the mapping $(x,k,\ell ) \mapsto {\operatorname {tail}}({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k, \ell )$ , which we want to show interacts nicely with appending an $n^{th}$ element of $\ell$ . These first two propositions give us more information about this idea.

Proposition 9.1. We have

\begin{align*} {\operatorname {tail}}(m,\ell ) =_{x,m,\ell } \left \{\begin{matrix} \varnothing & \text{if } {\operatorname {len}}(\ell ) \leq m \\ {\operatorname {nthDef}}(x,m,\ell ) :: {\operatorname {tail}}(sm,\ell ) & \text{else} \end{matrix}\right .\!. \end{align*}

Proof. We first prove by induction on $\ell$ that

\begin{align*} \ell =_{x,\ell } \left \{\begin{matrix} \varnothing & \text{if } {\operatorname {len}}(\ell ) = 0 \\ {\operatorname {zerothDef}}(x, \ell ) :: {\operatorname {tr}}(\ell ) & \text{else} \end{matrix}\right .\!. \end{align*}

If $\ell = \varnothing$ , then ${\operatorname {len}}(\ell ) = 0$ , so the right side reduces to $\varnothing$ . If $\ell = y :: \ell '$ , then ${\operatorname {len}}(\ell ) = s({\operatorname {len}}(\ell '))$ , and the right side reduces to ${\operatorname {zerothDef}}(x, y :: \ell ') :: {\operatorname {tr}}(y :: \ell ') = y :: \ell ' = \ell$ .

Now, in the above equality, we replace $\ell$ by ${\operatorname {tail}}(m,\ell )$ . The else case simplifies (using the definition of $\operatorname {nthDef}$ ) to

\begin{align*} {\operatorname {zerothDef}}(x, {\operatorname {tail}}(m,\ell )) :: {\operatorname {tr}}({\operatorname {tail}}(m,\ell )) = {\operatorname {nthDef}}(x,m,\ell ) :: {\operatorname {tail}}(sm,\ell ). \end{align*}

The term ${\operatorname {len}}({\operatorname {tail}}(m,\ell ))$ in the “if” condition simplifies (by Proposition 4.8) to ${\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} m$ , so the condition is equivalent to ${\operatorname {len}}(\ell ) \leq m$ . Thus, we get the desired equality.

Proposition 9.2. We have

\begin{align*} {\operatorname {tail}}(Pm,\ell ) =_{x,m,\ell } \left \{\begin{matrix} {\operatorname {tail}}(m,\ell ) & \text{if } m=0 \\ \varnothing & \text{else if } {\operatorname {len}}(\ell ) \lt m \\ {\operatorname {nthDef}}(x,Pm,\ell ) :: {\operatorname {tail}}(m,\ell ) & \text{else} \end{matrix}\right .\!. \end{align*}

Proof. We prove this by induction on $m$ . If $m=0$ , then the left side is just ${\operatorname {tail}}(0,\ell )$ . On the right side, the condition $m=0$ is true, so it reduces to ${\operatorname {tail}}(0,\ell )$ , as desired.

On the other hand, suppose $m=sn$ . On the right-hand side, the outer condition becomes $sn=0$ , which is false, so it reduces to the else-if. So, the equality we want to prove becomes

\begin{align*} {\operatorname {tail}}(Psn,\ell ) =_{x,n,\ell } \left \{\begin{matrix} \varnothing & \text{if } {\operatorname {len}}(\ell ) \lt sn \\ {\operatorname {nthDef}}(x,Psn,\ell ) :: {\operatorname {tail}}(sn,\ell ) & \text{else} \end{matrix}\right .\!. \end{align*}

Clearly, $Psn=n$ , and the condition ${\operatorname {len}}(\ell ) \lt sn$ is by definition equivalent to $s({\operatorname {len}}(\ell )) \mathrel {\substack {\cdot \\[-1ex]-}} sn = 0$ . But $sa \mathrel {\substack {\cdot \\[-1ex]-}} sb =_{a,b} a \mathrel {\substack {\cdot \\[-1ex]-}} b$ , so this condition is just ${\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} n = 0$ , i.e., ${\operatorname {len}}(\ell ) \leq n$ . Thus, the equality we want to prove is precisely what we have proved in the previous proposition.

In the next lemma, we show that an arrow $H$ (which will act like the arrows $H_1, H_2$ we mentioned) satisfies a recurrence relation like the one we described in the proof outline.

Lemma 9.3. Consider the arrow $A : X \times N \times L(X) \times L(X) \rightarrow L(X)$ given by

\begin{align*} A(x,k,\ell ,L) =_{x,k,\ell ,L} \left \{ \begin{matrix} L & \text{if } {\operatorname {len}}(\ell ) \leq k \\ {\operatorname {nthDef}}(x, P({\operatorname {len}}(\ell )\mathrel {\substack {\cdot \\[-1ex]-}} k), \ell ) :: L & \text{else} \end{matrix} \right .\!. \end{align*}

Next, consider $H : X \times N \times L(X) \rightarrow L(X)$ given by

\begin{align*} H(x,k,\ell ) =_{x,k,\ell } {\operatorname {tail}}({\operatorname {len}}(\ell )\mathrel {\substack {\cdot \\[-1ex]-}} k, \ell ). \end{align*}

Intuitively, $H$ takes $\ell$ and removes all but the last $k$ elements. Then,

\begin{align*} H(x,s(k),\ell ) =_{x,k,\ell } A(x,k,\ell ,H(x,k,\ell )). \end{align*}

Proof. Using the previous proposition, we compute

\begin{align*} & H(x,sk,\ell ) \\ &\quad =_{x,k,\ell } {\operatorname {tail}}({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} sk, \ell ) \\ &\quad =_{x,k,\ell } {\operatorname {tail}}(P({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k), \ell ) \\ &\quad =_{x,k,\ell } \left \{\begin{matrix} {\operatorname {tail}}({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k,\ell ) & \text{if } {\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k=0 \\ \varnothing & \text{else if } {\operatorname {len}}(\ell ) \lt {\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k \\ {\operatorname {nthDef}}(x,P({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k),\ell ) :: {\operatorname {tail}}({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k,\ell ) & \text{else} \end{matrix}\right .\!. \end{align*}

Note that the top condition, ${\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k = 0$ , is the same as ${\operatorname {len}}(\ell ) \leq k$ . Moreover, the else-if condition is just false, so the else-if-else reduces to just the else case. (To justify this formally, we need to show $s({\operatorname {len}}(\ell )) \mathrel {\substack {\cdot \\[-1ex]-}} ({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k) \gt _{k,\ell } 0$ . But by Proposition A.5, this is equivalent to saying ${\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k \leq _{k,\ell } s({\operatorname {len}}(\ell ))$ , which is easy to show.) Finally, we can just replace the term ${\operatorname {tail}}({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k, \ell )$ by $H(x,k,\ell )$ . With all this consideration, the above expression reduces to

\begin{align*} H(x,sk,\ell ) = \left \{\begin{matrix} H(x,k,\ell ) & \text{if } {\operatorname {len}}(\ell ) \leq k \\ {\operatorname {nthDef}}(x, P({\operatorname {len}}(\ell ) \mathrel {\substack {\cdot \\[-1ex]-}} k), \ell ) :: H(x,k,\ell ) & \text{else} \end{matrix}\right .\!, \end{align*}

which is just $A(x,k,\ell , H(x,k,\ell ))$ , as desired.

Finally, we reach the desired result. As noted previously, this theorem does not allow us to conclude $h_1(a) =_a h_2(a)$ , that is, $h_1 = h_2$ . It says that $h_1 \circ \pi _A = h_2 \circ \pi _A$ as maps $X \times A \rightarrow L(X)$ ; we can’t yet get rid of the parameter $X$ .

Theorem 9.4. Let $h_1, h_2 : A \rightarrow L(X)$ . Suppose that

\begin{gather*} {\operatorname {len}}(h_1(a)) =_a {\operatorname {len}}(h_2(a)), \\ {\operatorname {nthDef}}(x, m, h_1(a)) =_{x,m,a} {\operatorname {nthDef}}(x, m, h_2(a)). \end{gather*}

Then, $h_1(a) =_{x,a} h_2(a)$ , where $x$ is a variable of type $X$ .

Proof. For $i=1,2$ , we define the map $A_i : X \times N \times A \times L(X) \rightarrow L(X)$ by setting $A_i(x,k,a,L) =_{x,k,a,L} A(x,k,h_i(a),L)$ , where $A$ is as in the previous lemma. For $i=1,2$ , define $H_i : X \times N \times A \rightarrow L(X)$ by $H_i(x,k,a) =_{x,k,a} H(x,k,h_i(a))$ , where $H$ is as in the previous lemma. By the previous lemma, we know that $H_i(x,sk,a) =_{x,k,a} A_i(x,k,a,H_i(x,k,a))$ .

We claim that $H_1 = H_2$ ; we’ll prove this by induction on $k$ . In the base case, we have $H_1(x,0,a) =_{x,a} \varnothing =_{x,a} H_2(x,0,a)$ ; indeed, for $i=1,2$ , we compute

\begin{align*} H_i(x,0,a) =_{x,a} H(x,0,h_i(a)) &=_{x,a} {\operatorname {tail}}({\operatorname {len}}(h_i(a)) \mathrel {\substack {\cdot \\[-1ex]-}} 0, h_i(a)) \\ &=_{x,a} {\operatorname {tail}}({\operatorname {len}}(h_i(a)), h_i(a)) =_{x,a} \varnothing . \end{align*}

The last equality follows from combining Propositions 4.8 and 4.9. (The length of this list is ${\operatorname {len}}(h_i(a)) \mathrel {\substack {\cdot \\[-1ex]-}} {\operatorname {len}}(h_i(a)) =_{x,a} 0$ , so the list is empty.)

For the inductive step, we note that $A_1 = A_2$ . Indeed, we have

\begin{align*} A_i(x,k,a,L) =_{x,k,a,L} \left \{\begin{matrix} L & \text{if } {\operatorname {len}}(h_i(a)) \leq k \\ {\operatorname {nthDef}}(x, P({\operatorname {len}}(h_i(a)) \mathrel {\substack {\cdot \\[-1ex]-}} k), h_i(a)) :: L & \text{else} \end{matrix}\right .\!, \end{align*}

so the equalities assumed for this theorem give us $A_1 = A_2$ . Writing $A_\times$ for $A_1 = A_2$ , we therefore have $H_i(x,sk,a) = A_\times (x,k,a,H_i(x,a,k))$ for $i=1,2$ .

So, $H_1, H_2$ satisfy the same defining equations, and we conclude by induction that $H_1 = H_2$ . Now, note that

\begin{align*} H_i(x, {\operatorname {len}}(h_i(a)), a) =_{x,a} {\operatorname {tail}}(0, h_i(a)) =_{x,a} h_i(a), \end{align*}

so $H_1 = H_2$ and ${\operatorname {len}}(h_1(a)) =_a {\operatorname {len}}(h_2(a))$ let us conclude $h_1(a) =_{x,a} h_2(a)$ , as desired.

9.2 Equality with extensivity hypotheses

In this section, we use finite limits and hypotheses (H1) and (H2) to supplement Theorem 9.4. First, we show that the conclusion can be changed from $h_1(a) =_{x,a} h_2(a)$ to $h_1 = h_2$ .

Proof. Let $l_A = {\operatorname {len}}_X \circ h_1 = {\operatorname {len}}_X \circ h_2$ . Let $D_0$ be the context $(a:A \mid l_A(a)=0)$ and let $D_{\gt 0}$ be the context $(a:A \mid l_A(a) \gt 0)$ . By Proposition 6.2 (which uses (H2)), we have $A = [D_0] + [D_{\gt 0}]$ . Therefore, to show $h_1 = h_2$ , it suffices to show that

\begin{align*} h_1(a) =_{D_0} h_2(a) \quad \text{and} \quad h_1(a) =_{D_{\gt 0}} h_2(a). \end{align*}

For the first equality, we claim that both terms equal $\varnothing$ . Indeed, in the context $D_0$ , we have ${\operatorname {len}}(h_1(a)) =_{D_0} l_A(a) =_{D_0} 0$ , and this implies that $h_1(a) =_{D_0} \varnothing$ by Proposition 4.9. The same goes for $h_2$ .

For the second equality, we need the existence of a term ${\operatorname {def}}' : X$ in the context $D_{\gt 0}$ . Indeed, if such a term exists, then by substituting $x \mapsto {\operatorname {def}}'$ , $a \mapsto a$ in the equation $h_1(a) =_{x,a} h_2(a)$ , we get the desired equality

\begin{align*} h_1(a) =_{D_{\gt 0}} h_2(a). \end{align*}

To obtain ${\operatorname {def}}'$ , we use Proposition 7.1 (which requires (H1)) to get a term ${\operatorname {def}} : X$ in the context $(m:N, \, \ell : L(X) \mid m \lt {\operatorname {len}}(\ell ))$ . Then, since $0 \lt _{D_{\gt 0}} l_A(a) =_{D_{\gt 0}} {\operatorname {len}}(h_1(a))$ , we can perform a substitution $m \mapsto 0$ , $\ell \mapsto h_1(a)$ to get the term ${\operatorname {def}}' = {\operatorname {def}}[0/m, \, h_1(a)/\ell ]$ of type $X$ in the context $D_{\gt 0}$ , as desired.

Next, we show that the hypotheses of Theorem 9.4 can be changed so that we use $\operatorname {nth}$ instead of $\operatorname {nthDef}$ (recall that assumption (H1) is necessary to talk about ${\operatorname {nth}}_X$ ).

Lemma 9.6. Let $\mathcal{C}$ be a category with finite limits and parametrized list objects and assume (H1) and (H2). Let $h_1, h_2 : A \rightarrow L(X)$ . Suppose that

\begin{align*} {\operatorname {len}} \circ h_1 &= {\operatorname {len}} \circ h_2, \end{align*}

and denote this arrow $l_A$ . Then, in the context $C = (m : N, \; a : A \mid m \lt l_A(a))$ , suppose that

\begin{align*} {\operatorname {nth}}(m, h_1(a)) =_C {\operatorname {nth}}(m, h_2(a)). \end{align*}

Then, ${\operatorname {nthDef}}(x, m, h_1(a)) =_{x,m,a} {\operatorname {nthDef}}(x, m, h_2(a))$ .

Proof. Let $D = (x:X, m:N, a:A)$ , and let $D_0 = (D \mid m \lt l_A(a))$ , $D_1 = (D \mid m \geq l_A(a))$ . Since we’re assuming (H2), we can use Corollary 6.3 to conclude that $[D] = [D_0] + [D_1]$ . Therefore, to show that ${\operatorname {nthDef}}(x, m, h_1(a)) =_D {\operatorname {nthDef}}(x, m, h_2(a))$ , it suffices to show the following.

\begin{align*} {\operatorname {nthDef}}(x, m, h_1(a)) =_{D_0} {\operatorname {nthDef}}(x, m, h_2(a)) \\ {\operatorname {nthDef}}(x, m, h_1(a)) =_{D_1} {\operatorname {nthDef}}(x, m, h_2(a)) \end{align*}

We start with the second equality, since it is the easiest. Indeed, since we have $m \geq _{D_1} l_A(a) =_{D_1} {\operatorname {len}}(h_1(a))$ , Proposition 4.10 tells us that

\begin{align*} {\operatorname {nthDef}}(x, m, h_1(a)) =_{D_1} x. \end{align*}

The same is true if we replace $h_1$ by $h_2$ , so the equality follows.

For the first equality, we note that ${\operatorname {nth}}(m, h_1(a)) =_{D_0} {\operatorname {nth}}(m, h_2(a))$ by assumption (we can “add $x:X$ to the context” by performing a substitution). To establish the desired equality, then, it suffices to show that

\begin{align*} {\operatorname {nthDef}}(x, m, h_1(a)) =_{D_0} {\operatorname {nth}}(m, h_1(a)), \end{align*}

and the same for $h_2$ (which is done the same way). We finish the proof by establishing this equality.

\begin{align*} {\operatorname {nth}}(m, h_1(a)) &=_{D_0} {\operatorname {nthDef}}({\operatorname {def}}', m, h_1(a)) \\&=_{D_0} {\operatorname {nthDef}}( x, m, h_1(a)) \end{align*}

There are two things to note here. First, the second equality is by Proposition 4.10, using the hypothesis $m \lt l_A(a) = {\operatorname {len}}(h_1(a))$ from the context $D_0$ . Second, ${\operatorname {def}}'$ is the term $\operatorname {def}$ used to define $\operatorname {nth}$ , but with the substitution $\ell \mapsto h_1(a)$ (it is originally in the context $(m:N, \ell :L(X) \mid m \lt {\operatorname {len}}(\ell ))$ ).

Putting this all together, we get the following result, which is the uniqueness part of showing that $(L_N(X), {\operatorname {nth}}_X)$ is a universal morphism.