# 5.3 W-types

Inductive types are very general, which is excellent for their usefulness and applicability, but makes them difficult to study as a whole. Fortunately, they can all be formally reduced to a few special cases. It is beyond the scope of this book to discuss this reduction β which is anyway irrelevant to the mathematician using type theory in practice β but we will take a little time to discuss the one of the basic special cases that we have not yet met. These are Martin-LΓΆfβs $\mathsf{W}$-types, also known as the types of well-founded trees. $\mathsf{W}$-types are a generalization of such types as natural numbers, lists, and binary trees, which are sufficiently general to encapsulate the βrecursionβ aspect of any inductive type.

A particular $\mathsf{W}$-type is specified by giving two parameters $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, in which case the resulting $\mathsf{W}$-type is written $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{% \mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a% :A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a% :A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf% {W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}B(a)$. The type $A$ represents the type of labels for $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{% \mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a% :A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a% :A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf% {W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}B(a)$, which function as constructors (however, we reserve that word for the actual functions which arise in inductive definitions). For instance, when defining natural numbers as a $\mathsf{W}$-type, the type $A$ would be the type $\mathbf{2}$ inhabited by the two elements ${0_{\mathbf{2}}}$ and ${1_{\mathbf{2}}}$, since there are precisely two ways to obtain a natural number β either it will be zero or a successor of another natural number.

The type family $B:A\to\mathcal{U}$ is used to record the arity of labels: a label $a:A$ will take a family of inductive arguments, indexed over $B(a)$. We can therefore think of the β$B(a)$-manyβ arguments of $a$. These arguments are represented by a function $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(% a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a% :A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf% {W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}B(a)$, with the understanding that for any $b:B(a)$, $f(b)$ is the β$b$-thβ argument to the label $a$. The $\mathsf{W}$-type $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{% \mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a% :A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a% :A)}}{\mathsf{W}_{(a:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(a:A)}}}{\mathsf% {W}_{(a:A)}}{\mathsf{W}_{(a:A)}}{\mathsf{W}_{(a:A)}}}B(a)$ can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of $A$ and each node labeled by $a:A$ has $B(a)$-many branches.

In the case of natural numbers, the label ${0_{\mathbf{2}}}$ has arity 0, since it constructs the constant zero; the label ${1_{\mathbf{2}}}$ has arity 1, since it constructs the successor of its argument. We can capture this by using simple elimination on $\mathbf{2}$ to define a function $\mathsf{rec}_{\mathbf{2}}(\mathcal{U},\mathbf{0},\mathbf{1})$ into a universe of types; this function returns the empty type $\mathbf{0}$ for ${0_{\mathbf{2}}}$ and the unit type $\mathbf{1}$ for ${1_{\mathbf{2}}}$. We can thus define

 $\mathbf{N^{w}}:\!\!\equiv\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(b:% \mathbf{2})}}}{\mathsf{W}_{(b:\mathbf{2})}}{\mathsf{W}_{(b:\mathbf{2})}}{% \mathsf{W}_{(b:\mathbf{2})}}}{\mathchoice{{\textstyle\mathsf{W}_{(b:\mathbf{2}% )}}}{\mathsf{W}_{(b:\mathbf{2})}}{\mathsf{W}_{(b:\mathbf{2})}}{\mathsf{W}_{(b:% \mathbf{2})}}}{\mathchoice{{\textstyle\mathsf{W}_{(b:\mathbf{2})}}}{\mathsf{W}% _{(b:\mathbf{2})}}{\mathsf{W}_{(b:\mathbf{2})}}{\mathsf{W}_{(b:\mathbf{2})}}}{% \mathchoice{{\textstyle\mathsf{W}_{(b:\mathbf{2})}}}{\mathsf{W}_{(b:\mathbf{2}% )}}{\mathsf{W}_{(b:\mathbf{2})}}{\mathsf{W}_{(b:\mathbf{2})}}}\mathsf{rec}_{% \mathbf{2}}(\mathcal{U},\mathbf{0},\mathbf{1})$

where the superscript $\mathbf{w}$ serves to distinguish this version of natural numbers from the previously used one. Similarly, we can define the type of lists over $A$ as a $\mathsf{W}$-type with $\mathbf{1}+A$ many labels: one nullary label for the empty list, plus one unary label for each $a:A$, corresponding to appending $a$ to the head of a list:

 $\mathsf{List}(A):\!\!\equiv\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:% \mathbf{1}+A)}}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf{W}_{(x:\mathbf{1}+A)}}% {\mathsf{W}_{(x:\mathbf{1}+A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:\mathbf% {1}+A)}}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{% \mathsf{W}_{(x:\mathbf{1}+A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:\mathbf{% 1}+A)}}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf% {W}_{(x:\mathbf{1}+A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:\mathbf{1}+A)}}% }{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf{W}_{(x:\mathbf{1}+A)}}{\mathsf{W}_{(x% :\mathbf{1}+A)}}}\mathsf{rec}_{\mathbf{1}+A}(\mathcal{U},\;\mathbf{0},\;{% \lambda}a.\,\mathbf{1}).$

In general, the $\mathsf{W}$-type $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$ specified by $A:\mathcal{U}$ and $B:A\to\mathcal{U}$ is the inductive type generated by the following constructor:

• β’

${\mathsf{sup}}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}% }}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_% {(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\Big{(}% B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:% A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W% }_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)\Big{)}\to\mathchoice% {\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$.

The constructor ${\mathsf{sup}}$ (short for supremum) takes a label $a:A$ and a function $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$ representing the arguments to $a$, and constructs a new element of $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$. Using our previous encoding of natural numbers as $\mathsf{W}$-types, we can for instance define

 $0^{\mathbf{w}}:\!\!\equiv{\mathsf{sup}}({0_{\mathbf{2}}},\;{\lambda}x.\,% \mathsf{rec}_{\mathbf{0}}(\mathbf{N^{w}},x)).$

Put differently, we use the label ${0_{\mathbf{2}}}$ to construct $0^{\mathbf{w}}$. Then, $\mathsf{rec}_{\mathbf{2}}(\mathcal{U},\mathbf{0},\mathbf{1},{0_{\mathbf{2}}})$ evaluates to $\mathbf{0}$, as it should since ${0_{\mathbf{2}}}$ is a nullary label. Thus, we need to construct a function $f:\mathbf{0}\to\mathbf{N^{w}}$, which represents the (zero) arguments supplied to ${0_{\mathbf{2}}}$. This is of course trivial, using simple elimination on $\mathbf{0}$ as shown. Similarly, we can define

 $\displaystyle 1^{\mathbf{w}}$ $\displaystyle:\!\!\equiv{\mathsf{sup}}({1_{\mathbf{2}}},\;{\lambda}x.\,0^{% \mathbf{w}})$ $\displaystyle 2^{\mathbf{w}}$ $\displaystyle:\!\!\equiv{\mathsf{sup}}({1_{\mathbf{2}}},\;{\lambda}x.\,1^{% \mathbf{w}})$

and so on.

We have the following induction principle for $\mathsf{W}$-types:

• β’

When proving a statement $E:\big{(}\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)\big{)}\to\mathcal{U}$ about all elements of the $\mathsf{W}$-type $\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$, it suffices to prove it for ${\mathsf{sup}}(a,f)$, assuming it holds for all $f(b)$ with $b:B(a)$. In other words, it suffices to give a proof

 $e:\mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(f:B(a)% \to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}% {\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(% x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}\,}{\mathchoice{{% \textstyle\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A% )}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{% {\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)% )}}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{% \prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{% \prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{% \mathchoice{{\textstyle\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}B(x))}}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}B(x))}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}B(x))}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}B(x))}}}{\mathchoice{{\textstyle\prod_{(f:B(a)\to\mathchoice{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{\prod_{(f:B(a)\to\mathchoice{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice% {{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(f:B(a)\to\mathchoice{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}\mathchoice{\prod_{(g:\mathchoice{\prod_{b:B% (a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:% B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b% :B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b% :B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}\,}{% \mathchoice{{\textstyle\prod_{(g:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(% a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B% (a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}}{\prod_{(g:\mathchoice{% \prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}% {\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}E(f(b)))}}{\prod_{(g:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(% a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B% (a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}{\prod_{(g:\mathchoice{% \prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}% {\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}E(f(b)))}}}{\mathchoice{{\textstyle\prod_{(g:\mathchoice{\prod_{b:B(a)}\,% }{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}% }{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))% }}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))% }}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}}{\prod_{(% g:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{% \prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle% \prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{% \mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}}E(f(b)))}}{\prod_{(g:\mathchoice{\prod_{b:B(a)}\,}{% \mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}% {\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}% }{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}{\prod_{(g:% \mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_% {(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_% {(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{% \mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}}E(f(b)))}}}{\mathchoice{{\textstyle\prod_{(g:\mathchoice{% \prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}% {\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}E(f(b)))}}}{\prod_{(g:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(% a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B% (a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}{\prod_{(g:\mathchoice{% \prod_{b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{% \prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}% {\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}E(f(b)))}}{\prod_{(g:\mathchoice{\prod_{b:B(a)}\,}{\mathchoice{{% \textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a% ))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(% a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B% (a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b)))}}}E({\mathsf{sup}}(a,f))$

The variable $g$ represents our inductive hypothesis, namely that all arguments of $a$ satisfy $E$. To state this, we quantify over all elements of type $B(a)$, since each $b:B(a)$ corresponds to one argument $f(b)$ of $a$.

How would we define the function $\mathsf{double}$ on natural numbers encoded as a $\mathsf{W}$-type? We would like to use the recursion principle of $\mathbf{N^{w}}$ with a codomain of $\mathbf{N^{w}}$ itself. We thus need to construct a suitable function

 $e:\mathchoice{\prod_{(a:\mathbf{2})}\,}{\mathchoice{{\textstyle\prod_{(a:% \mathbf{2})}}}{\prod_{(a:\mathbf{2})}}{\prod_{(a:\mathbf{2})}}{\prod_{(a:% \mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(a:\mathbf{2})}}}{\prod_{(a:% \mathbf{2})}}{\prod_{(a:\mathbf{2})}}{\prod_{(a:\mathbf{2})}}}{\mathchoice{{% \textstyle\prod_{(a:\mathbf{2})}}}{\prod_{(a:\mathbf{2})}}{\prod_{(a:\mathbf{2% })}}{\prod_{(a:\mathbf{2})}}}\mathchoice{\prod_{(f:B(a)\to\mathbf{N^{w}})}\,}{% \mathchoice{{\textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{\prod_{(f:B(a)\to% \mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{% N^{w}})}}}{\mathchoice{{\textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{\prod_{(% f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)% \to\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}% }}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod% _{(f:B(a)\to\mathbf{N^{w}})}}}\mathchoice{\prod_{(g:B(a)\to\mathbf{N^{w}})}\,}% {\mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}}}{\prod_{(g:B(a)\to% \mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{% N^{w}})}}}{\mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}}}{\prod_{(% g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)% \to\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}% }}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod% _{(g:B(a)\to\mathbf{N^{w}})}}}\mathbf{N^{w}}$

which will represent the recurrence for the $\mathsf{double}$ function; for simplicity we denote the type family $\mathsf{rec}_{\mathbf{2}}(\mathcal{U},\mathbf{0},\mathbf{1})$ by $B$.

Clearly, $e$ will be a function taking $a:\mathbf{2}$ as its first argument. The next step is to perform case analysis on $a$ and proceed based on whether it is ${0_{\mathbf{2}}}$ or ${1_{\mathbf{2}}}$. This suggests the following form

 $e:\!\!\equiv{\lambda}a.\,\mathsf{rec}_{\mathbf{2}}(C,e_{0},e_{1},a)$

where

 $C:\!\!\equiv\mathchoice{\prod_{(f:B(a)\to\mathbf{N^{w}})}\,}{\mathchoice{{% \textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{\prod_{(f:B(a)\to\mathbf{N^{w}})% }}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{% \mathchoice{{\textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{\prod_{(f:B(a)\to% \mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{% N^{w}})}}}{\mathchoice{{\textstyle\prod_{(f:B(a)\to\mathbf{N^{w}})}}}{\prod_{(% f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)\to\mathbf{N^{w}})}}{\prod_{(f:B(a)% \to\mathbf{N^{w}})}}}\mathchoice{\prod_{(g:B(a)\to\mathbf{N^{w}})}\,}{% \mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}}}{\prod_{(g:B(a)\to% \mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{% N^{w}})}}}{\mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}}}{\prod_{(% g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)% \to\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(g:B(a)\to\mathbf{N^{w}})}% }}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod_{(g:B(a)\to\mathbf{N^{w}})}}{\prod% _{(g:B(a)\to\mathbf{N^{w}})}}}\mathbf{N^{w}}$

If $a$ is ${0_{\mathbf{2}}}$, the type $B(a)$ becomes $\mathbf{0}$. Thus, given $f:\mathbf{0}\to\mathbf{N^{w}}$ and $g:\mathbf{0}\to\mathbf{N^{w}}$, we want to construct an element of $\mathbf{N^{w}}$. Since the label ${0_{\mathbf{2}}}$ represents $\mathbf{0}$, it needs zero inductive arguments and the variables $f$ and $g$ are irrelevant. We return $0^{\mathbf{w}}$ as a result:

 $e_{0}:\!\!\equiv{\lambda}f.\,{\lambda}g.\,0^{\mathbf{w}}$

Analogously, if $a$ is ${1_{\mathbf{2}}}$, the type $B(a)$ becomes $\mathbf{1}$. Since the label ${1_{\mathbf{2}}}$ represents the successor operator, it needs one inductive argument β the predecessor β which is represented by the variable $f:\mathbf{1}\to\mathbf{N^{w}}$. The value of the recursive call on the predecessor is represented by the variable $g:\mathbf{1}\to\mathbf{N^{w}}$. Thus, taking this value (namely $g(\star)$) and applying the successor operator twice thus yields the desired result:

 $e_{1}:\!\!\equiv\;{\lambda}f.\,{\lambda}g.\,{\mathsf{sup}}({1_{\mathbf{2}}},({% \lambda}x.\,{\mathsf{sup}}({1_{\mathbf{2}}},({\lambda}y.\,g(\star))))).$

Putting this together, we thus have

 $\mathsf{double}:\!\!\equiv\mathsf{rec}_{\mathbf{N^{w}}}(\mathbf{N^{w}},e)$

with $e$ as defined above.

The associated computation rule for the function $\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{% W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}(E,e):% \mathchoice{\prod_{w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}\,}{% \mathchoice{{\textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}% _{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}B(x))}}}{\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{\mathchoice{{% \textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{\mathchoice{{% \textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}E(w)$ is as follows.

• β’

For any $a:A$ and $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(% x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf% {W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$ we have

 $\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{% W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}(E,e,{\mathsf% {sup}}(a,f))\equiv e(a,f,\big{(}{\lambda}b.\,\mathsf{rec}_{\mathchoice{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}(E,f(b))\big{)}).$

In other words, the function $\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{% W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}(E,e)$ satisfies the recurrence $e$.

By the above computation rule, the function $\mathsf{double}$ behaves as expected:

 $\displaystyle\mathsf{double}(0^{\mathbf{w}})$ $\displaystyle\equiv\mathsf{rec}_{\mathbf{N^{w}}}(\mathbf{N^{w}},e,{\mathsf{sup% }}({0_{\mathbf{2}}},\;{\lambda}x.\,\mathsf{rec}_{\mathbf{0}}(\mathbf{N^{w}},x)))$ $\displaystyle\equiv e({0_{\mathbf{2}}},\big{(}{\lambda}x.\,\mathsf{rec}_{% \mathbf{0}}(\mathbf{N^{w}},x)\big{)},\big{(}{\lambda}x.\,\mathsf{double}(% \mathsf{rec}_{\mathbf{0}}(\mathbf{N^{w}},x))\big{)})$ $\displaystyle\equiv e_{t}(\big{(}{\lambda}x.\,\mathsf{rec}_{\mathbf{0}}(% \mathbf{N^{w}},x)\big{)},\big{(}{\lambda}x.\,\mathsf{double}(\mathsf{rec}_{% \mathbf{0}}(\mathbf{N^{w}},x))\big{)})$ $\displaystyle\equiv 0^{\mathbf{w}}$ and $\displaystyle\mathsf{double}(1^{\mathbf{w}})$ $\displaystyle\equiv\mathsf{rec}_{\mathbf{N^{w}}}(\mathbf{N^{w}},e,{\mathsf{sup% }}({1_{\mathbf{2}}},\;{\lambda}x.\,0^{\mathbf{w}}))$ $\displaystyle\equiv e({1_{\mathbf{2}}},\big{(}{\lambda}x.\,0^{\mathbf{w}}\big{% )},\big{(}{\lambda}x.\,\mathsf{double}(0^{\mathbf{w}})\big{)})$ $\displaystyle\equiv e_{f}(\big{(}{\lambda}x.\,0^{\mathbf{w}}\big{)},\big{(}{% \lambda}x.\,\mathsf{double}(0^{\mathbf{w}})\big{)})$ $\displaystyle\equiv{\mathsf{sup}}({1_{\mathbf{2}}},({\lambda}x.\,{\mathsf{sup}% }({1_{\mathbf{2}}},({\lambda}y.\,\mathsf{double}(0^{\mathbf{w}})))))$ $\displaystyle\equiv{\mathsf{sup}}({1_{\mathbf{2}}},({\lambda}x.\,{\mathsf{sup}% }({1_{\mathbf{2}}},({\lambda}y.\,0^{\mathbf{w}}))))$ $\displaystyle\equiv 2^{\mathbf{w}}$

and so on.

Just as for natural numbers, we can prove a uniqueness theorem for $\mathsf{W}$-types:

###### Theorem 5.3.1.

Let $g,h:\mathchoice{\prod_{w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}% }}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)}\,}{% \mathchoice{{\textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}% _{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}B(x))}}}{\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{\mathchoice{{% \textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{\mathchoice{{% \textstyle\prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{% \textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf% {W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}{% \prod_{(w:\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{% (x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}{\prod_{(w:% \mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x))}}}E(w)$ be two functions which satisfy the recurrence

 $e:\mathchoice{\prod_{a,f}\,}{\mathchoice{{\textstyle\prod_{(a,f)}}}{\prod_{(a,% f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle\prod_{(a,f)}}}{% \prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle\prod_{(a% ,f)}}}{\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}\Bigl{(}\mathchoice{\prod_% {b:B(a)}\,}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_% {(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod_{(b:B(a))}}}{\prod% _{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}{\mathchoice{{\textstyle\prod% _{(b:B(a))}}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}{\prod_{(b:B(a))}}}E(f(b))% \Bigr{)}\to E({\mathsf{sup}}(a,f)),$

i.e., such that

 $\displaystyle\mathchoice{\prod_{a,f}\,}{\mathchoice{{\textstyle\prod_{(a,f)}}}% {\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle\prod_{(% a,f)}}}{\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle% \prod_{(a,f)}}}{\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}g({\mathsf{sup}}(% a,f))=e(a,f,{\lambda}b.\,g(f(b))),$ $\displaystyle\mathchoice{\prod_{a,f}\,}{\mathchoice{{\textstyle\prod_{(a,f)}}}% {\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle\prod_{(% a,f)}}}{\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}{\mathchoice{{\textstyle% \prod_{(a,f)}}}{\prod_{(a,f)}}{\prod_{(a,f)}}{\prod_{(a,f)}}}h({\mathsf{sup}}(% a,f))=e(a,f,{\lambda}b.\,h(f(b))).$

Then $g$ and $h$ are equal.

Title 5.3 W-types
\metatable