For -types we introduce primitive constants and .
An expression of the form is written as
, and an expression of the form is written
if and , then
if moreover, and then .
Here also we can define functions by total recursion. If we have and
as above and , then we can introduce a defined constant
whenever we have
with the defining equation