A.1.7 W-types

For W-types we introduce primitive constants c𝖶 and c𝗌𝗎𝗉. An expression of the form c𝖶(A,λx.B) is written as 𝖶(x:A)B, and an expression of the form c𝗌𝗎𝗉(x,u) is written as 𝗌𝗎𝗉(x,u):

  • if A:𝒰n and B:A𝒰n, then 𝖶(x:A)B(x):𝒰n

  • if moreover, a:A and g:B(a)𝖶(x:A)B(x) then 𝗌𝗎𝗉(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)𝒰m, then we can introduce a defined constant f:(z:𝖶(x:A)B(x))C(z) whenever we have


with the defining equation

Title A.1.7 W-types