The elimination axiom for natural numbers, surreal numbers, lists, and trees can all be properly called induction. However, I don’t think the expression `if b then x else y`

is an example of recursion, and so I don’t think **2 **should be called an inductive type. Similarly, I don’t like how the term inductive type is used for dependent sums, unit and null types, and the various new types of homotopy type theory. What all these types share in common is that they have a set of constructors and an elimination axiom which essentially says that these constructors are the only way to obtain an element of these types. A better terminology would be such a type is the free type over a set of

constructors, and to call such a type a free type.

### Like this:

Like Loading...

*Related*