The type formers \(0, 1, +, \times, \rightarrow, \Sigma,\) and \(\Pi\) which interpret the logical constants for intuitionistic predicate logic are examples of degenerate inductive definitions. Even the identity type (in intensional intuitionistic type theory) is inductively generated; it is the type of proofs generated by the reflexivity axiom. Its elimination rule expresses proof by pattern matching on the proof of reflexivity.