Another example is that \(\W\)-types can be used for encoding other inductively defined types in Extensional Type Theory. For example, the Brouwer ordinals of the second and higher number classes can be defined as special instances of the \(\W\)-type (Martin-Löf 1984). More generally, it can be shown that all inductively defined types which are given by a strictly positive type operator can be represented as instances of well-founded trees (Dybjer 1997).