The general schema does not only cover inductively defined types, but also inductively defined families of types, such as the identity relation. The above mentioned type \(A^n\) of \(n\)-tuples of type \(A\) was defined above by primitive recursion on \(n\). It can also be defined as an inductive family with the following introduction rules