mathlib documentation


Cartesian closed categories

Given a category with finite products, the cartesian monoidal structure is provided by the local instance monoidal_of_has_finite_products.

We define exponentiable objects to be closed objects with respect to this monoidal structure, i.e. (X × -) is a left adjoint.

We say a category is cartesian closed if every object is exponentiable (equivalently, that the category equipped with the cartesian monoidal structure is closed monoidal).

Show that exponential forms a difunctor and define the exponential comparison morphisms.


Some of the results here are true more generally for closed objects and for closed monoidal categories, and these could be generalised.

An object X is exponentiable if (X × -) is a left adjoint. We define this as being closed in the cartesian monoidal structure.

The terminal object is always exponentiable. This isn't an instance because most of the time we'll prove cartesian closed for all objects at once, rather than just for this one.


A category C is cartesian closed if it has finite products and every object is exponentiable. We define this as monoidal_closed with respect to the cartesian monoidal structure.

Show that the exponential of the terminal object is isomorphic to itself, i.e. X^1 ≅ X.

The typeclass argument is explicit: any instance can be used.


The internal hom functor given by the cartesian closed structure.


If an initial object I exists in a CCC, then A ⨯ I ≅ I.


If an initial object I exists in a CCC then it is a strict initial object, i.e. any morphism to I is an iso. This actually shows a slightly stronger version: any morphism to an initial object from an exponentiable object is an isomorphism.


If an initial object 0 exists in a CCC then every morphism from it is monic.