A cartesian closed category is a category $\mathsf{C}$ with finite products in which the product bifunctor \(\mathsf{C} \times \mathsf{C} \xrightarrow{\times} \mathsf{C}\) is closed.