Cartesian closed category

A category with finite products and an exponential object for every pair of objects. Its exponentials represent morphisms from products, giving the category an internal notion of function.

Connect

Category: A structure of objects and composable morphisms satisfying identity and associativity laws. Cartesian closed categories add products and exponentials to this basic structure.
Cartesian closed adjunction: The natural correspondence between morphisms X×A→B and morphisms X→B^A. This adjunction is the defining relationship behind exponential objects.
Simply typed lambda calculus: A lambda calculus whose expressions carry types built from base types and function types. Its function types are modeled by exponential objects in categorical semantics.
Locally cartesian closed category: A category with finite limits whose slice categories are cartesian closed. It strengthens cartesian closure by providing dependent function objects in every slice.
Product (category theory): An object equipped with projections that represents pairs of morphisms into two objects. Finite products provide the pairing operation required by the definition.
Evaluation morphism: The canonical morphism B^A×A→B that applies an internal function to its argument. It realizes function application inside the category.
Propositions as types: The correspondence between logical propositions and types, and between proofs and programs. Cartesian closed categories model implication as an exponential and conjunction as a product.
Monoidal closed category: A monoidal category with internal hom objects representing morphisms out of tensor products. It generalizes the exponential adjunction by replacing cartesian product with a monoidal product.
Terminal object: An object receiving exactly one morphism from every object in a category. A terminal object is the empty finite product required by the definition.
Currying: The conversion of a function of several arguments into a function returning another function. The exponential universal property turns maps X×A→B into maps X→B^A.