Internal language

Summary

The internal language of a category with enough structure is a formal language read inside the category. Its types are the objects of the category, and its terms are interpreted as morphisms. For a topos it is the Mitchell–Bénabou language, a higher-order intuitionistic logic; for a Cartesian closed category it is the simply typed lambda calculus. It lets one reason about objects of the category as if they were sets, with elements, functions and subsets. The reasoning then stays valid in the category. It is one of the main tools of categorical logic.