 It is straightforward to extend the untyped \(\lambda\)-calculus so that it discriminates between different kinds of objects. This entry limits itself to the type-free \(\lambda\)-calculus. See the entries on  type theory  and  Church’s type theory  for a detailed discussion of the extensions of \(\lambda\)-calculus that we get when we add types, and see (Barendregt, Dekkers, Statman, 2013) for a book length treatment of the subject.