A.1.7 $W$-types

For $W$-types we introduce primitive constants $c_{𝖶}$ and $c_{\mathrm{𝗌𝗎𝗉}}$.An expression of the form $c_{𝖶}(A,\lambda x.B)$ is written as${𝖶}_{(x:A)}B$, and an expression of the form $c_{\mathrm{𝗌𝗎𝗉}}(x,u)$ is writtenas $\mathrm{𝗌𝗎𝗉}(x,u)$:

• if $A:{𝒰}_n$ and $B:A\to {𝒰}_n$, then ${𝖶}_{(x:A)}B(x):{𝒰}_n$

• if moreover, $a:A$ and $g:B(a)\to {𝖶}_{(x:A)}B(x)$ then $\mathrm{𝗌𝗎𝗉}(a,g):{𝖶}_{(x:A)}B(x)$.

Here also we can define functions by total recursion. If we have $A$ and $B$as above and $C:{𝖶}_{(x:A)}B(x)\to {𝒰}_m$, then we can introduce a defined constant$f:{\prod }_{(z:{𝖶}_{(x:A)}B(x))}C(z)$ whenever we have

$$d:{\prod }_{(x:A)}{\prod }_{(u:B(x)\to {𝖶}_{(x:A)}B(x))}(({\prod }_{(y:B(x))}C(u(y)))\to C(\mathrm{𝗌𝗎𝗉}(x,u)))$$

with the defining equation

$$f(\mathrm{𝗌𝗎𝗉}(x,u)):\equiv d(x,u,f\circ u).$$