We present a new class of inductive definitions in type theory, which define binary relations instead of simple types (sets). The basic differen ce with ordinary inductive types is that the elimination rule (induction princip le) associated to such a type has two conclusions, one for elements and one for the pairs of the binary relation. In order for the calculus to be easier to use we develop a ``graph based'' calculus, which has many properties in common with the lambda calculus, including the possibility of abstraction. For example we gi ve the countable ordinal omega and a ``monotone'' system of ordinal notations.