Universes

Given an inductive definition of a type I, one can exploit its generated elimination principle to define functions with domain I. The range of such a definition is limited by the universe of the elimination principle i.e., Prop, Type(i) or Type. Recall that Prop ${}\subsetneq{}$Type(i) ${}\subsetneq{}$ Type. Hence, the theories of inductive definition vary according to the choice of universe. In particular, one cannot prove disjointness of constructors for any inductive definition which is eliminated over the kind Prop.

The environmental variable LEGOPATH controls the search path for LEGO modules. By default it accommodates elimination over Type and inductive types inhabiting Type. It is set to .:$LIBDIR/lib_Type:$LIBDIR where LIBDIR records the root directory of the library.

Users who prefer elimination over

Prop

need to replace lib_Type by lib_Prop in their LEGOPATH. In this configuration, inductive types inhabit the kind Prop.

Type(2)

need to replace lib_Type by lib_TYPE in their LEGOPATH. In this configuration, inductive types inhabit the kind Type(0)

More exotic configurations can be achieved by setting the variables SET, TYPE, TYPE_minus1, and TYPE_minus2 in a module called parameters and ensure that

• their LEGOPATH considers their version of parameters before any such module in the library
• LEGOPATH has to include lib_TYPE.

Inductive types inhabit SET and the elimination rule eliminates over TYPE. Notice that some theorems in the library fail unless TYPE_minus2 : TYPE_minus1 : TYPE.