Cartesian closed category

Summary

A Cartesian closed category is a category with finite products in which every pair of objects has an exponential object. In it, morphisms $X \times Y \to Z$ match morphisms $X \to Z^Y$, as in currying of functions. Sets, small categories, presheaf categories and every topos are Cartesian closed. Cartesian closed categories are the models of the simply typed lambda calculus.