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

Exponential objects🔗

In a category C\mathcal{C} with all finite products (including a terminal object!), where by the usual internal logic dictionary we regard a morphism f:Γ→Af : \Gamma \to A as an AA-term in context Γ\Gamma, the notion of exponential object captures what it means for an object to interpret function types. An exponential object for AA and BB is an object BAB^A equipped with an evaluation map

ev:BA×A→B \mathrm{ev} : B^A \times A \to B

standing for the essence of function application: if I have a function f:A→Bf : A \to B, and I have an x:Ax : A, then application gives me an f(x):Af(x) : A.

Moreover, exponential objects must satisfy a universal property relative to the product functor: if I have a derivation m:Γ×A→Bm : \Gamma \times A \to B, of a BB-term in a context extended by AA, then I should be able to form the “abstraction” λm:Γ→BA\lambda m : \Gamma \to B^A.

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 Hom(Γ,BA)\mathbf{Hom}(\Gamma, B^A) and Hom(Γ×A,B)\mathbf{Hom}(\Gamma \times A, B): 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 BA×A→BB^A \times A \to B is sufficient to interpret the more familiar formation rule for function application,

Γ⊢f:BAΓ⊢x:AΓ⊢f(x):B \frac{\Gamma \vdash f : B^A\quad \Gamma \vdash x : A} {\Gamma \vdash f(x) : B}

by relativising to an arbitrary context Γ\Gamma through composition, and that this indeed interprets the β\beta-reduction 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 (BA,ev)(B^A, \mathrm{ev}), with a witness that ev\mathrm{ev} 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 (A,B)↦BA(A,B) \mapsto B^A as an internalised analogue of the Hom\mathbf{Hom}-functor. In the same way that a pair of morphisms B→B′B \to B' and A→A′A \to A' would act on the ordinary Hom\mathbf{Hom} sets by composition, they act on internal homs, too, defining a mapping BA→B′A′B^A \to B'^{A'}.

  [-,-]₁ : ∀ {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 Cop×C→C\mathcal{C}^{\mathrm{op}} \times \mathcal{C} \to \mathcal{C}. With a bit more effort, we can show that our defining equivalence between the Hom\mathbf{Hom}-sets Γ×A→B\Gamma \times A \to B and Γ→BA\Gamma \to B^A satisfies the naturality condition required to to characterise −A-^A as the right adjoint to −×A- \times A.

  [-,-] .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 −×A- \times A has a right adjoint −A-^A, then C\mathcal{C} is a Cartesian closed category, with the object BAB^A 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 .counit.ε 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 B:CB : \mathcal{C} as exponentiable if, for every other A:CA : \mathcal{C}, the exponential object ABA^B exists. This means that we have a right adjoint −B-^B to the functor −×B- \times B, by the discussion above. It will, however, be more useful to us to characterise exponentiability of BB by a condition on the slice category C/BC/B.

  -^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 ΔB:C→C/B\Delta_B : \mathcal{C} \to \mathcal{C}/B, which sends an object XX to the product projection π2:X×B→B\pi_2 : X \times B \to B. Following (Johnstone 2002, A1.5.2), we have the following characterisation of exponentiability: In a category with pullbacks, an object BB is exponentiable iff. we have a right adjoint functor ΔB⊢ΠB\Delta_B \vdash \Pi_B.

Suppose BB is exponentiable. The value ΠB(h)\Pi_B(h) on a family h:A→Bh : A \to B is defined to be the pullback

where the map fB:AB→BBf^B : A^B \to B^B, on the right, is the action of (−)B(-)^B on ff. An application of the universal properties at hand shows that we can extend maps h:X→Yh : X \to Y over BB to maps ΠB(X)→ΠB(Y)\Pi_B(X) \to \Pi_B(Y). 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 ΔB:C→C/B\Delta_B : \mathcal{C} \to \mathcal{C}/B like we had claimed. We start with an elementary observation: given maps f:A→Bf : A \to B and q:X→ABq : X \to A^B, asking for

λ(f∘ev)∘q=λ(π2)∘!⁡ \lambda (f \circ \mathrm{ev}) \circ q = \lambda(\pi_2) \circ \operatorname{!}

is equivalent to asking for

f∘λ−1(q)=π2, f \circ \lambda^{-1}(q) = \pi_2\text{,}

which is in turn equivalent to asking that qq be a map ΔB(X)→f\Delta_B(X) \to f, over BB.

    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 Hom\mathbf{Hom}-sets HomC(X,ΠB(f))\mathbf{Hom}_\mathcal{C}(X, \Pi_B(f)) and HomC/B(ΔB(X),f)\mathbf{Hom}_{\mathcal{C}/B}(\Delta_B(X), f), and even though it factors through the rather complicated path displayed below, it definitionally sends h:HomC(X,ΠB(f))h : \mathbf{Hom}_\mathcal{C}(X, \Pi_B(f)) to

λ−1(p1∘h). \lambda^{-1}(p_1\circ h)\text{.}

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 ΔB⊣ΠB\Delta_B \dashv \Pi_B 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.