open import Cat.Diagram.Terminal open import Cat.Diagram.Product open import Cat.Functor.Adjoint open import Cat.Prelude import Cat.Functor.Bifunctor as Bifunctor import Cat.Reasoning module Cat.CartesianClosed.Base where

# Cartesian closed categoriesπ

Recall that we defined a **cartesian category** to be
one which admits all binary products, hence products of any finite
positive cardinality. Such a category is called **cartesian
closed** (abbreviation: ccc) if it has a terminal object (hence
products of any natural number of objects), and, for any object
$A$,
the functor
$- \times A$
has a right adjoint, to be
denoted
$[A,-]$.

The object
$[A,B]$
provided by this functor is called the **exponential of
$B$
by
$A$**,
and thus it is also written
$B^A$.
The adjunction is best understood in terms of isomorphisms between Hom-functors: In a ccc, the following
Hom-sets are naturally isomorphic.

$\mathbf{Hom}(A \times B, C) \cong \mathbf{Hom}(A, [B,C])$

The right-to-left direction of this isomorphism is called
**currying**; The left-to-right direction can thus be
called **uncurrying**. Generally, if you have an object in
one side, its image under the isomorphism is called its
**exponential transpose**. The interpretation of
$[A,B]$
is that it is the *space of maps* between
$A$
and
$B$.
Indeed, every *actual* map
$f : A \to B$
in the category corresponds to a unique map
$\ulcorner f \urcorner : 1 \to [A,B]$
(called the **name** of
$f$),
by the following sequence of isomorphisms:

$\mathbf{Hom}(A,B) \cong \mathbf{Hom}(1 \times A, B) \cong \mathbf{Hom}(1, [A,B])$

record is-cc {o β} (C : Precategory o β) (cartesian : β A B β Product C A B) : Type (o β β) where field terminal : Terminal C open Cat.Reasoning C open Binary-products C cartesian public private module Γ-Bifunctor = Bifunctor {C = C} {C} {C} Γ-functor field [_,-] : Ob β Functor C C tensorβ£hom : β A β Γ-Bifunctor.Left A β£ ([ A ,-]) module [-,-] (a : Ob) = Functor [ a ,-] module Tβ£H {a : Ob} = _β£_ (tensorβ£hom a) [_,_] : Ob β Ob β Ob [ A , B ] = [-,-].β A B

We now make the structure of a ccc more explicit.

module CartesianClosed {o β} {C : Precategory o β} {cart : β A B β Product C A B} (cc : is-cc C cart) where open Cat.Reasoning C open Functor open is-cc cc public private variable X Y Z : Ob

Each pair of objects
$X$,
$Y$
gives rise to an **evaluation** map
$\mathrm{ev} : [X, Y] \times X \to Y$.
This is the counit of the tensor-hom adjunction. The adjuncts (the exponential
transposes mentioned before) generated by a map
$f$
give the currying and uncurrying transformations:

ev : Hom ([ X , Y ] ββ X) Y ev = Tβ£H.counit.Ξ΅ _ curry : Hom (X ββ Y) Z β Hom X [ Y , Z ] curry = L-adjunct (tensorβ£hom _) uncurry : Hom X [ Y , Z ] β Hom (X ββ Y) Z uncurry = R-adjunct (tensorβ£hom _)

By the triangle identities, curry and uncurry are inverse equivalences.

curryβuncurry : β {X Y Z} β is-left-inverse (curry {X} {Y} {Z}) uncurry curryβuncurry f = L-R-adjunct (tensorβ£hom _) f uncurryβcurry : β {X Y Z} β is-right-inverse (curry {X} {Y} {Z}) uncurry uncurryβcurry f = R-L-adjunct (tensorβ£hom _) f