Induction-induction

In intuitionistic type theory (ITT), some discipline within mathematical logic, induction-induction is for simultaneously declaring some inductive type and some inductive predicate over this type.
An inductive definition is given by rules for generating elements of some type. One can then define some predicate on that type by providing constructors for forming the elements of the predicate , such inductively on the way the elements of the type are generated. Induction-induction generalizes this situation since one can "simultaneously" define the type and the predicate, because the rules for generating elements of the type formula_1 are allowed to refer to the predicate formula_2.
Induction-induction can be used to define larger types including various universe constructions in type theory. and limit constructions in category/topos theory.
Example 1.
Present the type formula_3 as having the following constructors , note the early reference to the predicate formula_4 :
and-simultaneously present the predicate formula_4 as having the following constructors :
Example 2.
A simple common example is the Universe à la Tarski type former. It creates some inductive type formula_17 and some inductive predicate formula_18. For every type in the type theory (except formula_19 itself!), there will be some element of formula_19 which may be seen as some code for this corresponding type ; The predicate formula_21 inductively encodes each possible type to the corresponding element of formula_19 ; and constructing new codes in formula_19 will require referring to the decoding-as-type of earlier codes , via the predicate formula_21 .