We already mentioned that there are two main definition principles in intuitionistic type theory: the inductive definition of types (sets) and the (primitive, structural) definition of functions by recursion on the way the elements of such types are inductively generated. Usually, the inductive definition of a set comes first: the formation and introduction rules make no reference to the elimination rule. However, there are definitions in intuitionistic type theory for which this is not the case and we simultaneously inductively generate a type and a function from that type defined by structural recursion. Such definitions are simultaneously inductive-recursive.