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

d:(x:A)(u:B(x)𝖶(x:A)B(x))(((y:B(x))C(u(y)))C(𝗌𝗎𝗉(x,u)))

with the defining equation

f(𝗌𝗎𝗉(x,u)):d(x,u,fu).
Title A.1.7 W-types
\metatable