open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
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