module Cat.Diagram.Exponential
  {o β„“} (C : Precategory o β„“) (fp : has-products C) (term : Terminal C) where

Exponential objectsπŸ”—

In a category with all finite products (including a terminal object!), where by the usual internal logic dictionary we regard a morphism as an in context , the notion of exponential object captures what it means for an object to interpret function types. An exponential object for and is an object equipped with an evaluation map

standing for the essence of function application: if I have a function and I have an then application gives me an

Moreover, exponential objects must satisfy a universal property relative to the product functor: if I have a derivation of a in a context extended by then I should be able to form the β€œabstraction”

record is-exponential (B^A : Ob) (ev : Hom (B^A βŠ—β‚€ A) B) : Type (o βŠ” β„“) where
  no-eta-equality
  field
    Ζ›        : βˆ€ {Ξ“} (m : Hom (Ξ“ βŠ—β‚€ A) B) β†’ Hom Ξ“ B^A
    commutes : βˆ€ {Ξ“} (m : Hom (Ξ“ βŠ—β‚€ A) B) β†’ ev ∘ Ζ› m βŠ—β‚ id ≑ m
    unique   : βˆ€ {Ξ“} {m : Hom (Ξ“ βŠ—β‚€ _) _} m'
             β†’ ev ∘ m' βŠ—β‚ id ≑ m
             β†’ m' ≑ Ζ› m

The data above is an unpacked way of saying that the evaluation map extends to an equivalence between and since being an equivalence is a proposition, once we have fixed the evaluation map, having abstractions is a property, not extra structure.

  unlambda : βˆ€ {C} (m : Hom C B^A) β†’ Hom (C βŠ—β‚€ A) B
  unlambda m = ev ∘ m βŠ—β‚ id

  lambda-is-equiv : βˆ€ {C} β†’ is-equiv (Ζ› {C})
  lambda-is-equiv = is-iso→is-equiv λ where
    .is-iso.inv    β†’ unlambda
    .is-iso.rinv x β†’ sym (unique x refl)
    .is-iso.linv x β†’ commutes x

As an aside, let us remark that the evaluation map is sufficient to interpret the more familiar formation rule for function application,

by relativising to an arbitrary context through composition, and that this indeed interprets the rule:

  private
    app : βˆ€ {Ξ“} (f : Hom Ξ“ B^A) (x : Hom Ξ“ A) β†’ Hom Ξ“ B
    app f x = ev ∘ f βŠ—β‚ id ∘ ⟨ id , x ⟩

    beta : βˆ€ {Ξ“} (f : Hom (Ξ“ βŠ—β‚€ A) B) (x : Hom Ξ“ A)
         β†’ app (Ζ› f) x ≑ f ∘ ⟨ id , x ⟩
    beta f x = pulll (commutes _)

Putting this data together, we can define an exponential object to be a pair with a witness that supports abstraction.

  record Exponential (A B : Ob) : Type (o βŠ” β„“) where
    no-eta-equality
    field
      B^A        : Ob
      ev         : Hom (B^A βŠ—β‚€ A) B
      has-is-exp : is-exponential B^A ev
    open is-exponential has-is-exp public

Since a finite-products category is called Cartesian monoidal, a finite-products category where every pair of objects has an exponential is called Cartesian closed, and we abbreviate the phrase β€œCartesian closed category” to β€œCCC”.

  record Cartesian-closed : Type (o βŠ” β„“) where
    no-eta-equality

    field has-exp : βˆ€ A B β†’ Exponential A B

    module _ {A} {B} where open Exponential (has-exp A B) hiding (B^A) public
    module Exp A B = Exponential (has-exp A B)

The connection between Cartesian closed categories and the lambda calculus is fundamental: however, it would take us too far afield of the basic properties of CCCs to discuss that in this module. You can find extended discussion, and an implementation, in the page on simply typed lambda calculus.

FunctorialityπŸ”—

In a Cartesian closed category, we can think of the exponential-assigning operation as an internalised analogue of the In the same way that a pair of morphisms and would act on the ordinary sets by composition, they act on internal homs, too, defining a mapping

  [-,-]₁ : βˆ€ {a a' b b'} β†’ Hom b b' β†’ Hom a' a β†’ Hom (Exp.B^A a b) (Exp.B^A a' b')
  [-,-]₁ f g = Ζ› (f ∘ ev ∘ ⟨ π₁ , g ∘ Ο€β‚‚ ⟩)

  [-,-] : Functor (C ^op Γ—αΆœ C) C
  [-,-] .Fβ‚€ (A , B) = Exp.B^A A B
  [-,-] .F₁ (f , g) = [-,-]₁ g f

Through some calculations that are just annoying enough to stun the unsuspecting reader, we can show that this is indeed a functor With a bit more effort, we can show that our defining equivalence between the and satisfies the naturality condition required to to characterise as the right adjoint to

  [-,-] .F-id =
    Ζ› (id ∘ ev ∘ ⟨ π₁ , id ∘ Ο€β‚‚ ⟩) β‰‘βŸ¨ ap Ζ› (idl _ βˆ™ ap (ev ∘_) (sym (apβ‚‚ ⟨_,_⟩ (idl _) refl))) βŸ©β‰‘
    Ζ› (ev ∘ id βŠ—β‚ id)              β‰‘Λ˜βŸ¨ unique id refl βŸ©β‰‘Λ˜
    id                             ∎
  [-,-] .F-∘ (f , g) (f' , g') = sym $ unique _ $
    ev ∘ ⟨ (Ζ› (g ∘ ev ∘ ⟨ π₁ , f ∘ Ο€β‚‚ ⟩) ∘ Ζ› (g' ∘ ev ∘ ⟨ π₁ , f' ∘ Ο€β‚‚ ⟩)) ∘ π₁ , id ∘ Ο€β‚‚ ⟩ β‰‘βŸ¨ refl⟩∘⟨ apβ‚‚ _βŠ—β‚_ refl (introl refl) βˆ™ Γ—-functor .F-∘ _ _ βŸ©β‰‘
    ev ∘ Ζ› (g ∘ ev ∘ ⟨ π₁ , f ∘ Ο€β‚‚ ⟩) βŠ—β‚ id ∘ Ζ› (g' ∘ ev ∘ ⟨ π₁ , f' ∘ Ο€β‚‚ ⟩) βŠ—β‚ id          β‰‘βŸ¨ pulll (commutes _) βŸ©β‰‘
    (g ∘ ev ∘ ⟨ π₁ , f ∘ Ο€β‚‚ ⟩) ∘ Ζ› (g' ∘ ev ∘ ⟨ π₁ , f' ∘ Ο€β‚‚ ⟩) βŠ—β‚ id                       β‰‘βŸ¨ pullr (pullr (apβ‚‚ _∘_ (apβ‚‚ ⟨_,_⟩ (introl refl) refl) refl βˆ™ sym (Bifunctor.first∘second Γ—-functor))) βŸ©β‰‘
    g ∘ ev ∘ Ζ› (g' ∘ ev ∘ ⟨ π₁ , f' ∘ Ο€β‚‚ ⟩) βŠ—β‚ id ∘ id βŠ—β‚ f                                 β‰‘βŸ¨ refl⟩∘⟨ pulll (commutes _) βŸ©β‰‘
    g ∘ (g' ∘ ev ∘ ⟨ π₁ , f' ∘ Ο€β‚‚ ⟩) ∘ id βŠ—β‚ f                                              β‰‘βŸ¨ pulll refl βˆ™ extendr (pullr (pullr (Product.unique (fp _ _) (pulll Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· idl _) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ extendr Ο€β‚‚βˆ˜βŸ¨βŸ©)))) βŸ©β‰‘
    (g ∘ g') ∘ ev ∘ ⟨ π₁ , (f' ∘ f) ∘ Ο€β‚‚ ⟩                                                  ∎

  product⊣exponential : βˆ€ {A} β†’ Bifunctor.Left Γ—-functor A ⊣ Bifunctor.Right [-,-] A
  product⊣exponential {A} = hom-isoβ†’adjoints Ζ› lambda-is-equiv nat where
    module _ {a b c d} (g : Hom a b) (h : Hom c d) (x : Hom (d βŠ—β‚€ A) a) where
      nat : Ζ› (g ∘ x ∘ ⟨ h ∘ π₁ , id ∘ Ο€β‚‚ ⟩) ≑ Ζ› (g ∘ ev ∘ ⟨ π₁ , id ∘ Ο€β‚‚ ⟩) ∘ Ζ› x ∘ h
      nat = sym $ unique _ $
        ev ∘ (Ζ› (g ∘ ev ∘ ⟨ π₁ , id ∘ Ο€β‚‚ ⟩) ∘ Ζ› x ∘ h) βŠ—β‚ id        β‰‘βŸ¨ refl⟩∘⟨ apβ‚‚ _βŠ—β‚_ refl (introl refl) βˆ™ Γ—-functor .F-∘ _ _ βŸ©β‰‘
        ev ∘ Ζ› (g ∘ ev ∘ ⟨ π₁ , id ∘ Ο€β‚‚ ⟩) βŠ—β‚ id ∘ (Ζ› x ∘ h) βŠ—β‚ id  β‰‘βŸ¨ pulll (commutes _) βŸ©β‰‘
        (g ∘ ⌜ ev ∘ ⟨ π₁ , id ∘ Ο€β‚‚ ⟩ ⌝) ∘ (Ζ› x ∘ h) βŠ—β‚ id           β‰‘βŸ¨ ap! (elimr (apβ‚‚ ⟨_,_⟩ (introl refl) refl βˆ™ Γ—-functor .F-id)) βŸ©β‰‘
        (g ∘ ev) ∘ (Ζ› x ∘ h) βŠ—β‚ id                                  β‰‘βŸ¨ pullr (apβ‚‚ _∘_ refl (Bifunctor.first∘first Γ—-functor)) βŸ©β‰‘
        g ∘ ev ∘ Ζ› x βŠ—β‚ id ∘ h βŠ—β‚ id                                β‰‘βŸ¨ refl⟩∘⟨ pulll (commutes _) βŸ©β‰‘
        g ∘ x ∘ h βŠ—β‚ id                                             ∎

From an adjunctionπŸ”—

As a converse to the results above, if each product functor has a right adjoint then is a Cartesian closed category, with the object serving as the exponential. This means that we can prove that a category is Cartesian closed by appealing to general facts about the existence of right adjoints, if any apply.

product-adjoint→cartesian-closed
  : (-^_ : Ob β†’ Functor C C)
  β†’ (βˆ€ A β†’ Bifunctor.Left Γ—-functor A ⊣ -^ A)
  β†’ Cartesian-closed
product-adjoint→cartesian-closed A→ adj = cc where
  open Exponential
  open is-exponential

  exp : βˆ€ A B β†’ Exponential A B
  exp A B .B^A = A→ A .F₀ B
  exp A B .ev = adj A .Ξ΅ B
  exp A B .has-is-exp .Ζ›          = L-adjunct (adj A)
  exp A B .has-is-exp .commutes m = R-L-adjunct (adj A) m
  exp A B .has-is-exp .unique m' x = sym $
    Equiv.injectiveβ‚‚ (_ , R-adjunct-is-equiv (adj A))
      (R-L-adjunct (adj A) _) x

  cc : Cartesian-closed
  cc .Cartesian-closed.has-exp = exp

Exponentiable objectsπŸ”—

We refer to an object as exponentiable if, for every other the exponential object exists. This means that we have a right adjoint to the functor by the discussion above. It will, however, be more useful to us to characterise exponentiability of by a condition on the slice category

  -^B : Functor C C
  -^B .Fβ‚€ = -^Bβ‚€
  -^B .F₁ h = Ζ› (h ∘ ev)
  -^B .F-id = ap Ζ› (idl ev) βˆ™ lambda-ev _
  -^B .F-∘ f g = sym $ Exponential.unique (exp _) _
    (  apβ‚‚ _∘_ refl (apβ‚‚ _βŠ—β‚_ refl (introl refl) βˆ™ Γ—-functor .F-∘ _ _)
    Β·Β· pulll (Exponential.commutes (exp _) _)
    Β·Β· extendr (Exponential.commutes (exp _) _))

Recall the constant families functor which sends an object to the product projection Following (Johnstone 2002, A1.5.2), we have the following characterisation of exponentiability: In a category with pullbacks, an object is exponentiable iff. we have a right adjoint functor

Suppose is exponentiable. The value on a family is defined to be the pullback

where the map on the right, is the action of on An application of the universal properties at hand shows that we can extend maps over to maps The calculation that this is functorial is routine, so we omit it from the page.

  exponentiable→product
    : has-pullbacks C
    β†’ Functor (Slice C B) C
  exponentiable→product pb = f where
    f : Functor (Slice C B) C
    f .Fβ‚€ h = pb {B = top} (-^B .F₁ (h .map)) (Ζ› Ο€β‚‚) .apex
    f .F₁ {x} {y} h = pb _ _ .universal (sym p) where abstract
      p : Ζ› Ο€β‚‚ ∘ !  ≑ -^B .F₁ (y .map) ∘ -^B .F₁ (h .map) ∘ pb {B = top} (-^B .F₁ (x .map)) (Ζ› Ο€β‚‚) .p₁
      p = Ζ› Ο€β‚‚ ∘ !                                         β‰‘βŸ¨ ap (Ζ› Ο€β‚‚ ∘_) (!-unique _) βŸ©β‰‘
          Ζ› Ο€β‚‚ ∘ pb _ _ .pβ‚‚                                β‰‘Λ˜βŸ¨ pb _ _ .square βŸ©β‰‘Λ˜
          Ζ› (x .map ∘ ev) ∘ pb _ _ .p₁                     β‰‘Λ˜βŸ¨ ap (-^B .F₁) (h .commutes) ⟩∘⟨refl βŸ©β‰‘Λ˜
          Ζ› ((y .map ∘ h .map) ∘ ev) ∘ pb _ _ .p₁          β‰‘βŸ¨ pushl (-^B .F-∘ _ _) βŸ©β‰‘
          Ζ› (y .map ∘ ev) ∘ Ζ› (h .map ∘ ev) ∘ pb _ _ .p₁   ∎

It remains to prove that this functor is actually a right adjoint to the constant-families functor like we had claimed. We start with an elementary observation: given maps and asking for

is equivalent to asking for

which is in turn equivalent to asking that be a map over

    coh₁ : βˆ€ {X} (f : /-Obj B) (q : Hom X (-^Bβ‚€ (f .domain)))
         β†’ (Ζ› (f .map ∘ ev) ∘ q ≑ Ζ› Ο€β‚‚ ∘ !)
         ≃ (f .map ∘ app q ≑ Ο€β‚‚)
    coh₁ f h = prop-ext!
      (Ξ» p β†’ Equiv.injective (_ , lambda-is-equiv _) (sym (Ζ›-∘ (has-is-exp _)) Β·Β· p Β·Β· done))
      (Ξ» p β†’ Ζ›-∘ (has-is-exp _) Β·Β· ap Ζ› p Β·Β· sym done)

This is the last piece that we need to establish an equivalence between the and and even though it factors through the rather complicated path displayed below, it definitionally sends to

Having this very simple computational description will greatly simplify the proof that this meandering equivalence is actually natural β€” and that naturality is all that stands between us and the adjunction we’ve been chasing.

        Hom X (Ξ .β‚€ f)
          β‰ƒβŸ¨ Pullback.pullback-univ (pb _ _) βŸ©β‰ƒ
        Ξ£ (Hom X (-^B .Fβ‚€ (f .domain))) (Ξ» h β†’ Ξ£ (Hom X top) Ξ» h' β†’ Ζ› (f .map ∘ ev) ∘ h ≑ Ζ› Ο€β‚‚ ∘ h')
          β‰ƒβŸ¨ Ξ£-ap-snd (Ξ» x β†’ Ξ£-contr-eqv (has⊀ X)) βŸ©β‰ƒ
        Ξ£ (Hom X (-^B .Fβ‚€ (f .domain))) (Ξ» h β†’ Ζ› (f .map ∘ ev) ∘ h ≑ Ζ› Ο€β‚‚ ∘ !)
          β‰ƒβŸ¨ Ξ£-ap (Equiv.inverse (Ζ› , lambda-is-equiv _)) (coh₁ f) βŸ©β‰ƒ
        Ξ£ (Hom (X βŠ—β‚€ B) (f .domain)) (Ξ» h β†’ f .map ∘ h ≑ Ο€β‚‚)
          β‰ƒβŸ¨ Isoβ†’Equiv ((Ξ» x β†’ record { commutes = x .snd }) , iso (Ξ» x β†’ _ , x .commutes) (Ξ» _ β†’ trivial!) (Ξ» _ β†’ trivial!)) βŸ©β‰ƒ
        Slice C B .Precategory.Hom (b.β‚€ X) f
          β‰ƒβˆŽ

      rem₁-Ξ² : βˆ€ {X} (f : /-Obj B) (h : Hom X (Ξ .β‚€ f))
             β†’ Equiv.to (rem₁ f) h .map ≑ app (pb _ _ .p₁ ∘ h)
      rem₁-Ξ² f h = refl

    nat : hom-iso-inv-natural {L = constant-family fp} {R = exponentiableβ†’product pb} (rem₁ _ .fst)
    nat g h x = ext $
     rem₁ _ .fst (Ξ .₁ g ∘ x ∘ h) .map                           β‰‘βŸ¨ rem₁-Ξ² _ _ βŸ©β‰‘
     app (pb _ _ .p₁ ∘ Ξ .₁ g ∘ x ∘ h)                           β‰‘βŸ¨ ap app (pulll (pb _ _ .pβ‚βˆ˜universal βˆ™ Ζ›-∘ {f = g .map} {g = pb _ _ .p₁} (has-is-exp _))) βŸ©β‰‘
     app (Ζ› (g .map ∘ ev ∘ pb _ _ .p₁ βŠ—β‚ id) ∘ x ∘ h)           β‰‘βŸ¨ apβ‚‚ _∘_ refl (apβ‚‚ _βŠ—β‚_ refl (sym (idl id)) βˆ™ Γ—-functor .F-∘ _ _) βˆ™ pulll refl βŸ©β‰‘
     app (Ζ› (g .map ∘ ev ∘ pb _ _ .p₁ βŠ—β‚ id)) ∘ (x ∘ h) βŠ—β‚ id   β‰‘βŸ¨ apβ‚‚ _∘_ (Equiv.Ξ· (_ , lambda-is-equiv _) _) refl βŸ©β‰‘
     (g .map ∘ ev ∘ pb _ _ .p₁ βŠ—β‚ id) ∘ (x ∘ h) βŠ—β‚ id           β‰‘βŸ¨ pullr (pullr (sym (Γ—-functor .F-∘ _ _) βˆ™ apβ‚‚ _βŠ—β‚_ (assoc _ _ _) refl βˆ™ Γ—-functor .F-∘ _ _)) βŸ©β‰‘
     g .map ∘ ev ∘ (pb _ _ .p₁ ∘ x) βŠ—β‚ id ∘ h βŠ—β‚ id             β‰‘βŸ¨ refl⟩∘⟨ (pulll refl βˆ™ apβ‚‚ _∘_ refl (apβ‚‚ ⟨_,_⟩ refl (idl _))) βŸ©β‰‘
     g .map ∘ (ev ∘ (pb _ _ .p₁ ∘ x) βŠ—β‚ id) ∘ b.₁ h .map        β‰‘βŸ¨ apβ‚‚ _∘_ refl (apβ‚‚ _∘_ (sym (rem₁-Ξ² _ _)) refl) βŸ©β‰‘
     g .map ∘ rem₁ _ .fst x .map ∘ b.₁ h .map                   ∎

References

  • Johnstone, Peter T. 2002. Sketches of an Elephant: a Topos Theory Compendium. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.