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 AA, the functor βˆ’Γ—A- \times A has a right adjoint, to be denoted [A,βˆ’][A,-].

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

Hom(AΓ—B,C)β‰…Hom(A,[B,C]) \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][A,B] is that it is the space of maps between AA and BB. Indeed, every actual map f:Aβ†’Bf : A \to B in the category corresponds to a unique map ⌜f⌝:1β†’[A,B]\ulcorner f \urcorner : 1 \to [A,B] (called the name of ff), by the following sequence of isomorphisms:

Hom(A,B)β‰…Hom(1Γ—A,B)β‰…Hom(1,[A,B]) \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
    terminal  : Terminal C

  open Cat.Reasoning C
  open Binary-products C cartesian public

    module Γ—-Bifunctor = Bifunctor {C = C} {C} {C} Γ—-functor

    [_,-]      : 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 XX, YY gives rise to an evaluation map ev:[X,Y]×X→Y\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 ff 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