The types created still remain predicative inside ITT.
An inductive definition is given by rules for generating elements of a type.
Induction-recursion generalizes this situation since one can simultaneously define the type and the function, because the rules for generating elements of the type are allowed to refer to the function.
[1] Induction-recursion can be used to define large types including various universe constructions.
It increases the proof-theoretic strength of type theory substantially.
Nevertheless, inductive-recursive recursive definitions are still considered predicative.
Induction-Recursion came out of investigations to the rules of Martin-Löf's intuitionistic type theory.
Martin-Löf had hinted that the rules for each type former followed a pattern, which preserved the properties of the type theory (e.g., strong normalization, predicativity).
Researchers started looking for the most general description of the pattern, since that would tell what kinds of type formers could be added (or not added!)
The "universe" type former was the most interesting, because when the rules were written "à la Tarski", they simultaneously defined the "universe type" and a function that operated on it.
This eventually lead Dybjer to Induction-Recursion.
Dybjer's initial papers called Induction-Recursion a "schema" for rules.
Later, he and Setzer would write a new type former with rules that allowed new Induction-Recursion definitions to be made inside the type theory.
[2] This was added to the Half proof assistant (a variant of Alf).
Constructors for Inductive types can be self-referential, but in a limited way.
is the function being (simultaneously) defined, these parameter declarations are positive: This is half-positive: These are not positive nor half-positive: A simple common example is the Universe à la Tarski type former.
that will map to the type of the parameter, and a function
maps to the return type of the function (which is dependent on the value of the parameter,
says that the result of the constructor is an element of type
is operating on a smaller part of the input.
Without going into the details, Induction-Recursion states what kinds of definitions (or rules) can be added to the theory such that the function calls will always terminate.
Induction-Recursion is implemented in Agda and Idris.