5.5 Homotopy-inductive types

In §5.3 (http://planetmath.org/53wtypes) we showed how to encode natural numbers as $\mathsf{W}$-types, with

 $\displaystyle\mathbf{N^{w}}$ $\displaystyle:\!\!\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}),$ $\displaystyle 0^{\mathbf{w}}$ $\displaystyle:\!\!\equiv{\mathsf{sup}}({0_{\mathbf{2}}},({\lambda}x.\,\mathsf{% rec}_{\mathbf{0}}(\mathbf{N^{w}},x))),$ $\displaystyle\mathbf{s^{w}}$ $\displaystyle:\!\!\equiv{\lambda}n.\,{\mathsf{sup}}({1_{\mathbf{2}}},({\lambda% }x.\,n)).$

We also showed how one can define a $\mathsf{double}$ function on $\mathbf{N^{w}}$ using the recursion principle. When it comes to the induction principle, however, this encoding is no longer satisfactory: given $E:\mathbf{N^{w}}\to\mathcal{U}$ and recurrences $e_{z}:E(0^{\mathbf{w}})$ and $e_{s}:\mathchoice{\prod_{(n:\mathbf{N^{w}})}\,}{\mathchoice{{\textstyle\prod_{% (n:\mathbf{N^{w}})}}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}{% \prod_{(n:\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbf{N^{w}})}% }}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N% ^{w}})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbf{N^{w}})}}}{\prod_{(n:% \mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}}% \mathchoice{\prod_{(y:E(n))}\,}{\mathchoice{{\textstyle\prod_{(y:E(n))}}}{% \prod_{(y:E(n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}}{\mathchoice{{\textstyle% \prod_{(y:E(n))}}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}}{% \mathchoice{{\textstyle\prod_{(y:E(n))}}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}{% \prod_{(y:E(n))}}}E(\mathbf{s^{w}}(n))$, we can only construct a dependent function $r(E,e_{z},e_{s}):\mathchoice{\prod_{n:\mathbf{N^{w}}}\,}{\mathchoice{{% \textstyle\prod_{(n:\mathbf{N^{w}})}}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:% \mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(% n:\mathbf{N^{w}})}}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}{% \prod_{(n:\mathbf{N^{w}})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbf{N^{w}})}% }}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N^{w}})}}{\prod_{(n:\mathbf{N% ^{w}})}}}E(n)$ satisfying the given recurrences propositionally, i.e. up to a path. This means that the computation rules for natural numbers, which give judgmental equalities, cannot be derived from the rules for $\mathsf{W}$-types in any obvious way.

This problem goes away if instead of the conventional inductive types we consider homotopy-inductive types, where all computation rules are stated up to a path, i.e. the symbol $\equiv$ is replaced by $=$. For instance, the computation rule for the homotopy version of $\mathsf{W}$-types $\mathsf{W^{h}}$ becomes:

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

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

Homotopy-inductive types have an obvious disadvantage when it comes to computational properties — the behavior of any function constructed using the induction principle can now only be characterized propositionally. But numerous other considerations drive us to consider homotopy-inductive types as well. For instance, while we showed in §5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) that inductive types are homotopy-initial algebras, not every homotopy-initial algebra is an inductive type (i.e. satisfies the corresponding induction principle) — but every homotopy-initial algebra is a homotopy-inductive type. Similarly, we might want to apply the uniqueness argument from §5.2 (http://planetmath.org/52uniquenessofinductivetypes) when one (or both) of the types involved is only a homotopy-inductive type — for instance, to show that the $\mathsf{W}$-type encoding of $\mathbb{N}$ is equivalent to the usual $\mathbb{N}$.

Additionally, the notion of a homotopy-inductive type is now internal to the type theory. For example, this means we can form a type of all natural numbers objects and make assertions about it. In the case of $\mathsf{W}$-types, we can characterize a homotopy $\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)$ as any type endowed with a supremum function and an induction principle satisfying the appropriate (propositional) computation rule:

 $\displaystyle\mathsf{W}_{d}(A,B):\!\!\equiv\mathchoice{\sum_{W:\mathcal{U}}\,}% {\mathchoice{{\textstyle\sum_{(W:\mathcal{U})}}}{\sum_{(W:\mathcal{U})}}{\sum_% {(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(W:% \mathcal{U})}}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(W:\mathcal{U})}}}{\sum_{(W:% \mathcal{U})}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}}\mathchoice{% \sum_{({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(% a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a% )}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)% }}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}\,}{\mathchoice{{% \textstyle\sum_{({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W% )}}}{\sum_{({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_% {({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}% {\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup% }}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\mathchoice{{\textstyle\sum_{({% \mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\sum_{({\mathsf{% sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)% }}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}% }{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}% {\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\mathchoice{{\textstyle\sum_{({% \mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\sum_{({\mathsf{% sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)% }}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}% }{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}% {\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}\mathchoice{\prod_{(E:W\to% \mathcal{U})}\,}{\mathchoice{{\textstyle\prod_{(E:W\to\mathcal{U})}}}{\prod_{(% E:W\to\mathcal{U})}}{\prod_{(E:W\to\mathcal{U})}}{\prod_{(E:W\to\mathcal{U})}}% }{\mathchoice{{\textstyle\prod_{(E:W\to\mathcal{U})}}}{\prod_{(E:W\to\mathcal{% U})}}{\prod_{(E:W\to\mathcal{U})}}{\prod_{(E:W\to\mathcal{U})}}}{\mathchoice{{% \textstyle\prod_{(E:W\to\mathcal{U})}}}{\prod_{(E:W\to\mathcal{U})}}{\prod_{(E% :W\to\mathcal{U})}}{\prod_{(E:W\to\mathcal{U})}}}\\ \displaystyle\mathchoice{\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}\,}{\mathchoice{{% \textstyle\prod_{(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)}}}(% \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)))\to E({\mathsf{sup}}(a,f)))}}}{\prod_{(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)}}}(\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)))\to E({\mathsf% {sup}}(a,f)))}}{\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}{\prod_{(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)}}}(\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)))\to E({\mathsf% {sup}}(a,f)))}}}{\mathchoice{{\textstyle\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}}{% \prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}{\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}{% \prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}}{\mathchoice{{\textstyle\prod_{(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)}}}(\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)))\to E({\mathsf% {sup}}(a,f)))}}}{\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}{\prod_{(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)}}}(\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)))\to E({\mathsf% {sup}}(a,f)))}}{\prod_{(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)}}}(\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)))\to E({\mathsf{sup}}(a,f)))}}}\mathchoice{\sum% _{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)% }}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod% _{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{% \textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}E(w))}% \,}{\mathchoice{{\textstyle\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}}{\mathchoice{{\textstyle\sum_{(\mathsf{ind}:% \mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)% }}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}E(w))}}}{\sum_{(\mathsf{ind}:% \mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)% }}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:% \mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)% }}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:% \mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)% }}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}E(w))}}}{\mathchoice{{% \textstyle\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{\mathchoice{{% \textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}E(w))}}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}{\sum_{(\mathsf{ind}:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}E(w))}}}\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)}}}\\ \displaystyle\mathsf{ind}({\mathsf{sup}}(a,f))=e(a,{\lambda}b.\,\mathsf{ind}(f% (b))).$

In http://planetmath.org/node/87579Chapter 6 we will see some other reasons why propositional computation rules are worth considering.

In this section, we will state some basic facts about homotopy-inductive types. We omit most of the proofs, which are somewhat technical.

Theorem 5.5.1.

For any $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, the type $\mathsf{W}_{d}(A,B)$ is a mere proposition.

It turns out that there is an equivalent characterization of $\mathsf{W}$-types using a recursion principle, plus certain uniqueness and coherence laws. First we give the recursion principle:

• When constructing a function from the $\mathsf{W}$-type $\mathchoice{\mathchoice{{\textstyle\mathsf{W}^{h}}}{\mathsf{W}^{h}}{\mathsf{W}% ^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{\mathchoice{{\textstyle\mathsf{W}^% {h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{% (x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)% }}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}}B(x)$ into the type $C$, it suffices to give its value for ${\mathsf{sup}}(a,f)$, assuming we are given the values of all $f(b)$ with $b:B(a)$. In other words, it suffices to construct a function

 $c:\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)}}}(B(a)\to C)\to C.$

The associated computation rule for $\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}^{h}}}{\mathsf{W}^{% h}}{\mathsf{W}^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{\mathchoice{{% \textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:% A)}}{\mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}B(x)}(C,c):(\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))\to C$ is as follows:

• For any $a:A$ and $f:B(a)\to\mathchoice{\mathchoice{{\textstyle\mathsf{W}^{h}}}{\mathsf{W}^{h}}{% \mathsf{W}^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{\mathchoice{{\textstyle% \mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}B(x)$ we have a witness $\beta(C,c,a,f)$ for equality

 $\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}^{h}}}{\mathsf{W}^{% h}}{\mathsf{W}^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{\mathchoice{{% \textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:% A)}}{\mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}B(x)}(C,c,{\mathsf{sup}}(a,f))% =c(a,{\lambda}b.\,\mathsf{rec}_{\mathchoice{\mathchoice{{\textstyle\mathsf{W}^% {h}}}{\mathsf{W}^{h}}{\mathsf{W}^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{% \mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}B(x)}(% C,c,f(b))).$

Furthermore, we assert the following uniqueness principle, saying that any two functions defined by the same recurrence are equal:

• Let $C:\mathcal{U}$ and $c:\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)}}}(B(a)\to C)\to C$ be given. Let $g,h:(\mathchoice{\mathchoice{{\textstyle\mathsf{W}^{h}}}{\mathsf{W}^{h}}{% \mathsf{W}^{h}}{\mathsf{W}^{h}}({\textstyle x:A}),\ }{\mathchoice{{\textstyle% \mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}^{h}_{(x:A)}}}{\mathsf{W}^{h}_{(x:A)}}{% \mathsf{W}^{h}_{(x:A)}}{\mathsf{W}^{h}_{(x:A)}}}B(x))\to C$ be two functions which satisfy the recurrence $c$ up to propositional equality, i.e., such that we have

 $\displaystyle\beta_{g}$ $\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))=c(a,{\lambda}b.\,g(f(b))),$ $\displaystyle\beta_{h}$ $\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))=c(a,{\lambda}b.\,h(f(b))).$

Then $g$ and $h$ are equal, i.e. there is $\alpha(C,c,f,g,\beta_{g},\beta_{h})$ of type $g=h$.

Recall that when we have an induction principle rather than only a recursion principle, this propositional uniqueness principle is derivable (Theorem 5.3.1 (http://planetmath.org/53wtypes#Thmprethm1)). But with only recursion, the uniqueness principle is no longer derivable — and in fact, the statement is not even true (exercise). Hence, we postulate it as an axiom. We also postulate the following coherence law, which tells us how the proof of uniqueness behaves on canonical elements:

• For any $a:A$ and $f:B(a)\to C$, the following diagram commutes propositionally:

where $\alpha$ abbreviates the path $\alpha(C,c,f,g,\beta_{g},\beta_{h}):g=h$.

Putting all of this data together yields another characterization 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)$, as a type with a supremum function, satisfying simple elimination, computation, uniqueness, and coherence rules:

 $\displaystyle\mathsf{W}_{s}(A,B):\!\!\equiv\mathchoice{\sum_{W:\mathcal{U}}\,}% {\mathchoice{{\textstyle\sum_{(W:\mathcal{U})}}}{\sum_{(W:\mathcal{U})}}{\sum_% {(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(W:% \mathcal{U})}}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(W:\mathcal{U})}}}{\sum_{(W:% \mathcal{U})}}{\sum_{(W:\mathcal{U})}}{\sum_{(W:\mathcal{U})}}}\;\mathchoice{% \sum_{{\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a% )}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)% }}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}% }}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W}\,}{\mathchoice{{% \textstyle\sum_{({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W% )}}}{\sum_{({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_% {({\mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}% {\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup% }}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\mathchoice{{\textstyle\sum_{({% \mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\sum_{({\mathsf{% sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)% }}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}% }{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}% {\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\mathchoice{{\textstyle\sum_{({% \mathsf{sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}{\sum_{({\mathsf{% sup}}:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)% }}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}% }{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}% {\prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}{\sum_{({\mathsf{sup}}:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to W)\to W)}}}\;\mathchoice{\prod_{C:\mathcal{% U}}\,}{\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:\mathcal{U})% }}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(C:\mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{% \prod_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{% \prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}}\;% \mathchoice{\prod_{c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a% )}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)% }}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}% }}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C}\,}{\mathchoice{{% \textstyle\prod_{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)% }}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}% }}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}% }{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}}{\prod_{(c:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}{\prod_{(c:\mathchoice{\prod_{a}% \,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}% }}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}% }{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}% (B(a)\to C)\to C)}}{\prod_{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}}{% \mathchoice{{\textstyle\prod_{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{% \textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C% )}}}{\prod_{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{% \prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}{\prod_{(c:% \mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}{\prod_{(c:\mathchoice{\prod_{a}% \,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}% }}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}% }{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}% (B(a)\to C)\to C)}}}{\mathchoice{{\textstyle\prod_{(c:\mathchoice{\prod_{a}\,}% {\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{% \mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{% \mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B% (a)\to C)\to C)}}}{\prod_{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle% \prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}{\prod% _{(c:\mathchoice{\prod_{a}\,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}% }{\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}% {\prod_{(a)}}{\prod_{(a)}}}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{% \prod_{(a)}}{\prod_{(a)}}}(B(a)\to C)\to C)}}{\prod_{(c:\mathchoice{\prod_{a}% \,}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}% }}{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}% }{\mathchoice{{\textstyle\prod_{(a)}}}{\prod_{(a)}}{\prod_{(a)}}{\prod_{(a)}}}% (B(a)\to C)\to C)}}}\;\mathchoice{\sum_{\mathsf{rec}:W\to C}\,}{\mathchoice{{% \textstyle\sum_{(\mathsf{rec}:W\to C)}}}{\sum_{(\mathsf{rec}:W\to C)}}{\sum_{(% \mathsf{rec}:W\to C)}}{\sum_{(\mathsf{rec}:W\to C)}}}{\mathchoice{{\textstyle% \sum_{(\mathsf{rec}:W\to C)}}}{\sum_{(\mathsf{rec}:W\to C)}}{\sum_{(\mathsf{% rec}:W\to C)}}{\sum_{(\mathsf{rec}:W\to C)}}}{\mathchoice{{\textstyle\sum_{(% \mathsf{rec}:W\to C)}}}{\sum_{(\mathsf{rec}:W\to C)}}{\sum_{(\mathsf{rec}:W\to C% )}}{\sum_{(\mathsf{rec}:W\to C)}}}\\ \displaystyle\;\mathchoice{\sum_{\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}% (f(b)))}\,}{\mathchoice{{\textstyle\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,% \mathsf{rec}(f(b))))}}}{\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}% (f(b))))}}{\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}% }{\sum_{(\beta:\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)}}}\mathsf% {rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}}}{% \mathchoice{{\textstyle\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}% (f(b))))}}}{\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}% }{\sum_{(\beta:\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)}}}\mathsf% {rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}}{\sum_{(% \beta:\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)}}}\mathsf{rec}({\mathsf{sup% }}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}}}{\mathchoice{{\textstyle\sum_% {(\beta:\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)}}}\mathsf{rec}({% \mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}}}{\sum_{(\beta:% \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)}}}\mathsf{rec}({\mathsf{sup}}(a,f% ))=c(a,{\lambda}b.\,\mathsf{rec}(f(b))))}}{\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b% .\,\mathsf{rec}(f(b))))}}{\sum_{(\beta:\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)}}}\mathsf{rec}({\mathsf{sup}}(a,f))=c(a,{\lambda}b.\,\mathsf{rec}% (f(b))))}}}\;\mathchoice{\prod_{g:W\to C}\,}{\mathchoice{{\textstyle\prod_{(g:% W\to C)}}}{\prod_{(g:W\to C)}}{\prod_{(g:W\to C)}}{\prod_{(g:W\to C)}}}{% \mathchoice{{\textstyle\prod_{(g:W\to C)}}}{\prod_{(g:W\to C)}}{\prod_{(g:W\to C% )}}{\prod_{(g:W\to C)}}}{\mathchoice{{\textstyle\prod_{(g:W\to C)}}}{\prod_{(g% :W\to C)}}{\prod_{(g:W\to C)}}{\prod_{(g:W\to C)}}}\;\mathchoice{\prod_{h:W\to C% }\,}{\mathchoice{{\textstyle\prod_{(h:W\to C)}}}{\prod_{(h:W\to C)}}{\prod_{(h% :W\to C)}}{\prod_{(h:W\to C)}}}{\mathchoice{{\textstyle\prod_{(h:W\to C)}}}{% \prod_{(h:W\to C)}}{\prod_{(h:W\to C)}}{\prod_{(h:W\to C)}}}{\mathchoice{{% \textstyle\prod_{(h:W\to C)}}}{\prod_{(h:W\to C)}}{\prod_{(h:W\to C)}}{\prod_{% (h:W\to C)}}}\;\mathchoice{\prod_{\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b)))}\,}{% \mathchoice{{\textstyle\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}{% \prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g% (f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}{% \mathchoice{{\textstyle\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}{% \prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g% (f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}{% \mathchoice{{\textstyle\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}{% \prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g% (f(b))))}}{\prod_{(\beta_{g}:\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))=c(a,{\lambda}b.\,g(f(b))))}}}\\ \displaystyle\;\mathchoice{\prod_{\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b)))}\,}{% \mathchoice{{\textstyle\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}{% \prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h% (f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}{% \mathchoice{{\textstyle\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}{% \prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h% (f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}{% \mathchoice{{\textstyle\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}{% \prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h% (f(b))))}}{\prod_{(\beta_{h}:\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))=c(a,{\lambda}b.\,h(f(b))))}}}\;% \mathchoice{\sum_{\alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle% \prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{% \textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}g(w)=h(w)}\,}{\mathchoice{{\textstyle\sum_{(\alpha:\mathchoice{\prod_{w:% W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{% \prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}}{\sum_{(\alpha:\mathchoice{\prod_{w% :W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{% \prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(\alpha:\mathchoice{\prod_{w:% W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{% \prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(\alpha:\mathchoice{\prod_{w:% W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{% \prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}}{\mathchoice{{\textstyle\sum_{(% \alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{% (w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}}{\sum_{(% \alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{% (w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(% \alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{% (w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(% \alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod% _{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}% }{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{% (w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}}{% \mathchoice{{\textstyle\sum_{(\alpha:\mathchoice{\prod_{w:W}\,}{\mathchoice{{% \textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w:W)}}}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}g(w)=h(w))}}}{\sum_{(\alpha:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(\alpha:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}{\sum_{(\alpha:\mathchoice{\prod_{w:W}\,}{% \mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{\prod_{(w% :W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(w:W)}}{% \prod_{(w:W)}}}{\mathchoice{{\textstyle\prod_{(w:W)}}}{\prod_{(w:W)}}{\prod_{(% w:W)}}{\prod_{(w:W)}}}g(w)=h(w))}}}\\ \displaystyle\;\alpha({\mathsf{sup}}(x,f))\mathchoice{\mathbin{\raisebox{2.15% pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\beta_{h}=\beta_{g}\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}c(a,-)(% \mathsf{funext}\;{\lambda}b.\,\alpha(f(b)))$
Theorem 5.5.2.

For any $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, the type $\mathsf{W}_{s}(A,B)$ is a mere proposition.

Finally, we have a third, very concise characterization 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)$ as an h-initial $\mathsf{W}$-algebra:

 $\mathsf{W}_{h}(A,B):\!\!\equiv\mathchoice{\sum_{I:\mathsf{W}\mathsf{Alg}(A,B)}% \,}{\mathchoice{{\textstyle\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}}{\sum_{(I:% \mathsf{W}\mathsf{Alg}(A,B))}}{\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}{\sum_{(% I:\mathsf{W}\mathsf{Alg}(A,B))}}}{\mathchoice{{\textstyle\sum_{(I:\mathsf{W}% \mathsf{Alg}(A,B))}}}{\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}{\sum_{(I:\mathsf% {W}\mathsf{Alg}(A,B))}}{\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}}{\mathchoice{{% \textstyle\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}}{\sum_{(I:\mathsf{W}\mathsf{% Alg}(A,B))}}{\sum_{(I:\mathsf{W}\mathsf{Alg}(A,B))}}{\sum_{(I:\mathsf{W}% \mathsf{Alg}(A,B))}}}\mathsf{isHinit}_{\mathsf{W}}(A,B,I).$
Theorem 5.5.3.

For any $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, the type $\mathsf{W}_{h}(A,B)$ is a mere proposition.

It turns out all three characterizations of $\mathsf{W}$-types are in fact equivalent:

Lemma 5.5.4.

For any $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, we have

 $\mathsf{W}_{d}(A,B)\simeq\mathsf{W}_{s}(A,B)\simeq\mathsf{W}_{h}(A,B)$

Indeed, we have the following theorem, which is an improvement over Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3):

Theorem 5.5.5.

The types satisfying the formation, introduction, elimination, and propositional computation rules for $\mathsf{W}$-types are precisely the homotopy-initial $\mathsf{W}$-algebras.

Sketch of proof.

Inspecting the proof of Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3), we see that only the propositional computation rule was required to establish the h-initiality 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)$. For the converse implication, let us assume that the polynomial functor associated to $A:\mathcal{U}$ and $B:A\to\mathcal{U}$, has an h-initial algebra $(W,s_{W})$; we show that $W$ satisfies the propositional rules of $\mathsf{W}$-types. The $\mathsf{W}$-introduction rule is simple; namely, for $a:A$ and $t:B(a)\rightarrow W$, we define ${\mathsf{sup}}(a,t):W$ to be the result of applying the structure map $s_{W}:PW\rightarrow W$ to $(a,t):PW$. For the $\mathsf{W}$-elimination rule, let us assume its premisses and in particular that $C^{\prime}:W\to\mathcal{U}$. Using the other premisses, one shows that the type $C:\!\!\equiv\mathchoice{\sum_{w:W}\,}{\mathchoice{{\textstyle\sum_{(w:W)}}}{% \sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:W)}% }}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}{\mathchoice{{\textstyle\sum_{(w:% W)}}}{\sum_{(w:W)}}{\sum_{(w:W)}}{\sum_{(w:W)}}}C^{\prime}(w)$ can be equipped with a structure map $s_{C}:PC\rightarrow C$. By the h-initiality of $W$, we obtain an algebra homomorphism $(f,s_{f}):(W,s_{W})\rightarrow(C,s_{C})$. Furthermore, the first projection $\mathsf{pr}_{1}:C\rightarrow W$ can be equipped with the structure of a homomorphism, so that we obtain a diagram of the form

But the identity function $1_{W}:W\rightarrow W$ has a canonical structure of an algebra homomorphism and so, by the contractibility of the type of homomorphisms from $(W,s_{W})$ to itself, there must be an identity proof between the composite of $(f,s_{f})$ with $(\mathsf{pr}_{1},s_{\mathsf{pr}_{1}})$ and $(1_{W},s_{1_{W}})$. This implies, in particular, that there is an identity proof $p:\mathsf{pr}_{1}\circ f=1_{W}$.

Since $(\mathsf{pr}_{2}\circ f)w:C((\mathsf{pr}_{1}\circ f)w)$, we can define

 $\mathsf{rec}(w,c):\!\!\equiv p_{\,*\,}((\mathsf{pr}_{2}\circ f)w):C(w)$

where the transport $p_{\,*\,}$ is with respect to the family

 ${\lambda}u.\,C\circ u:(W\to W)\to W\to\mathcal{U}.$

The verification of the propositional $\mathsf{W}$-computation rule is a calculation, involving the naturality properties of operations of the form $p_{\,*\,}$. ∎

Finally, as desired, we can encode homotopy-natural-numbers as homotopy-$\mathsf{W}$-types:

Theorem 5.5.6.

The rules for natural numbers with propositional computation rules can be derived from the rules for $\mathsf{W}$-types with propositional computation rules.

Title 5.5 Homotopy-inductive types
\metatable