open import Cat.Functor.Adjoint.Hom
open import Cat.Instances.Product
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Cartesian
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor
import Cat.Reasoning

module Cat.Diagram.Exponential
  {o ℓ} (C : Precategory o ℓ) (cart : Cartesian-category C) where

Exponential objects🔗

In a Cartesian category $C,$ where by the usual internal logic dictionary we regard a morphism $f : Γ \to A$ as an $A -term$ in context $Γ$ , the notion of exponential object captures what it means for an object to interpret function types. An exponential object for $A$ and $B$ is an object $B^{A}$ equipped with an evaluation map $ev : B^{A} \times A \to B$ standing for the essence of function application: if I have a function $f : A \to B,$ and I have an $x : A,$ then application gives me an $f (x) : B .$

open Cartesian-category cart
open Functor
open _⊣_

private variable
  A B : Ob

Moreover, exponential objects must satisfy a universal property relative to the product functor: if I have a derivation $m : Γ \times A \to B,$ of a $B -term$ in a context extended by $A,$ then I should be able to form the “abstraction” $λm : Γ \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 (Γ, B^{A})$ and $Hom (Γ \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.from   → unlambda
    .is-iso.rinv x → sym (unique x refl)
    .is-iso.linv x → commutes x

  unique₂ : ∀ {C} {m : Hom (C ⊗₀ _) _} m₁ m₂
          → ev ∘ m₁ ⊗₁ id ≡ m
          → ev ∘ m₂ ⊗₁ id ≡ m
          → m₁ ≡ m₂
  unique₂ _ _ p q = unique _ p ∙ sym (unique _ q)

  lambda-ev : ƛ ev ≡ id
  lambda-ev = sym (unique id (sym (intror (×-functor .F-id))))

As an aside, let us remark that the evaluation map $B^{A} \times A \to B$ is sufficient to interpret the more familiar formation rule for function application, $\frac{Γ ⊢ f : B ^{A} Γ ⊢ x : A}{Γ ⊢ f ( x ) : B}$ by relativising to an arbitrary context $Γ$ through composition, and that this indeed interprets the $β -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 _)

module _ where
  is-exponential-is-prop : ∀ {B^A} {ev : Hom (B^A ⊗₀ A) B} → is-prop (is-exponential B^A ev)
  is-exponential-is-prop {B^A = B^A} {ev} x y = q where
    open is-exponential

    p : Path (∀ {C} m → Hom C B^A) (x .ƛ) (y .ƛ)
    p i {C} m = y .unique (x .ƛ m) (x .commutes m) i

    q : x ≡ y
    q i .ƛ = p i
    q i .commutes m =
      is-prop→pathp (λ i → Hom-set _ _ (ev ∘ p i m ⊗₁ id) m) (x .commutes m) (y .commutes m) i
    q i .unique {m = m} m' q =
      is-prop→pathp (λ i → Hom-set _ _ m' (p i m)) (x .unique m' q) (y .unique m' q) i

Putting this data together, we can define an exponential object to be a pair $(B^{A}, ev),$ with a witness that $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 _ A B     where open Exponential (has-exp A B) renaming (B^A to [_,_]) using () public

    unlambda-∘ : ∀ {a b c d} (α : Hom a [ c , d ]) (β : Hom b a) → unlambda (α ∘ β) ≡ unlambda α ∘ β ⊗₁ id
    unlambda-∘ α β = sym (Equiv.adjunctl (ƛ , lambda-is-equiv) (sym (unique (α ∘ β) aux))) where
      aux =
        ev ∘ (α ∘ β) ⊗₁ id            ≡⟨ ap (λ x → ev ∘ (α ∘ β) ⊗₁ x) (sym $ idl id) ⟩
        ev ∘ (α ∘ β) ⊗₁ (id ∘ id) ≡⟨ ap (ev ∘_) (×-functor .F-∘ (α , id) (β , id)) ⟩
        ev ∘ α ⊗₁ id ∘ β ⊗₁ id      ≡⟨ assoc _ _ _ ⟩
        (ev ∘ α ⊗₁ id) ∘ β ⊗₁ id    ∎

    ƛ-∘' : ∀ {a a' b b' c} (f : Hom (a ⊗₀ b) c) (g : Hom a' a) (h : Hom b' b)
        → ƛ (f ∘ g ⊗₁ h) ≡ ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g
    ƛ-∘' f g h = sym (unique _ aux) where
      aux =
        unlambda (ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f ∘ g)
          ≡⟨ unlambda-∘ (ƛ (ev ∘ id ⊗₁ h)) (ƛ f ∘ g) ⟩
        unlambda (ƛ (ev ∘ id ⊗₁ h)) ∘ (ƛ f ∘ g) ⊗₁ id
          ≡⟨ pushl (commutes _) ⟩
        ev ∘ id ⊗₁ h ∘ (ƛ f ∘ g) ⊗₁ id
          ≡⟨ ap (ev ∘_) (sym (×-functor .F-∘ (id , h) (ƛ f ∘ g , id))) ⟩
        ev ∘ (id ∘ (ƛ f ∘ g)) ⊗₁ (h ∘ id)
          ≡⟨ (λ i → ev ∘ idl (ƛ f ∘ g) i ⊗₁ idr h i) ⟩
        ev ∘ (ƛ f ∘ g) ⊗₁ h
          ≡⟨ (λ i → ev ∘ (ƛ f ∘ g) ⊗₁ idl h (~ i)) ⟩
        ev ∘ (ƛ f ∘ g) ⊗₁ (id ∘ h)
          ≡⟨ ap (ev ∘_) (×-functor .F-∘ (ƛ f , id) (g , h)) ⟩
        ev ∘ (ƛ f ⊗₁ id) ∘ (g ⊗₁ h)
          ≡⟨ pulll (commutes _) ⟩
        f ∘ g ⊗₁ h
          ∎

    ƛ-∘-idl
      : ∀ {a b b' c} (f : Hom (a ⊗₀ b) c) (h : Hom b' b)
      → ƛ (f ∘ id ⊗₁ h) ≡ ƛ (ev ∘ id ⊗₁ h) ∘ ƛ f
    ƛ-∘-idl f h = ƛ-∘' f id h ∙ ap₂ _∘_ refl (elimr refl)

    ƛ-∘-idr
      : ∀ {a a' b c} (f : Hom (a ⊗₀ b) c) (g : Hom a' a)
      → ƛ (f ∘ g ⊗₁ id) ≡ ƛ f ∘ g
    ƛ-∘-idr f g = ƛ-∘' f g id ∙ eliml (ap ƛ (elimr (Functor.F-id ×-functor)) ∙ lambda-ev)

    ƛ-⊗
      : ∀ {a b a' b' c} (f : Hom (a ⊗₀ b) c) (g : Hom a' a) (h : Hom b' b)
      → ƛ (f ∘ id ⊗₁ h) ∘ g ≡ ƛ (f ∘ g ⊗₁ h)
    ƛ-⊗ f g h = sym (Equiv.adjunctr (ƛ , lambda-is-equiv) (sym aux)) where
      aux =
        unlambda (ƛ (f ∘ id ⊗₁ h) ∘ g)
          ≡⟨ unlambda-∘ _ _ ⟩
        unlambda (ƛ (f ∘ id ⊗₁ h)) ∘ g ⊗₁ id
          ≡⟨ pushl (commutes _) ⟩
        f ∘ id ⊗₁ h ∘ g ⊗₁ id
          ≡⟨ ap (f ∘_) (sym $ ×-functor .F-∘ (id , h) (g , id)) ⟩
        f ∘ (id ∘ g) ⊗₁ (h ∘ id)
          ≡⟨ ap₂ (λ x y → f ∘ x ⊗₁ y) (idl g) (idr h) ⟩
        f ∘ g ⊗₁ h
          ∎

  open is-exponential

  exponential-unique
    : ∀ {A B B^A B^A'} {ev : Hom (B^A ⊗₀ A) B} {ev' : Hom (B^A' ⊗₀ A) B}
    → is-exponential B^A ev
    → is-exponential B^A' ev'
    → B^A ≅ B^A'
  exponential-unique {ev = ev} {ev'} exp1 exp2 =
    make-iso (exp2 .ƛ ev) (exp1 .ƛ ev')
      (unique₂ exp2 (exp2 .ƛ ev ∘ exp1 .ƛ ev') id
        (  ap (ev' ∘_) (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _)
        ∙∙ pulll (exp2 .commutes _)
        ∙∙ exp1 .commutes _)
        (elimr (×-functor .F-id)))
      (unique₂ exp1 (exp1 .ƛ ev' ∘ exp2 .ƛ ev) id
        (  ap (ev ∘_) (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _)
        ∙∙ pulll (exp1 .commutes _)
        ∙∙ exp2 .commutes _)
        (elimr (×-functor .F-id)))

  ƛ-∘
    : ∀ {A B C X A^X B^X} {evA : Hom (A^X ⊗₀ X) A} {evB : Hom (B^X ⊗₀ X) B}
    → {f : Hom A B} {g : Hom C A^X}
    → (exp : is-exponential B^X evB)
    → exp .is-exponential.ƛ (f ∘ evA) ∘ g ≡ exp .is-exponential.ƛ (f ∘ evA ∘ g ⊗₁ id)
  ƛ-∘ exb = is-exponential.unique exb _
    ( ap₂ _∘_ refl (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _)
    ∙ extendl (is-exponential.commutes exb _))

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) \mapsto B^{A}$ as an internalised analogue of the $Hom -functor.$ In the same way that a pair of morphisms $B \to B^{'}$ and $A \to A^{'}$ would act on the ordinary $Hom$ sets by composition, they act on internal homs, too, defining a mapping $B^{A} \to B^{' A^{'}} .$

module _ (cc : Cartesian-closed) where
  open Cartesian-closed cc

  [-,-]₁ : ∀ {a a' b b'} → Hom b b' → Hom a' a → Hom [ a , b ] [ a' , b' ]
  [-,-]₁ f g = ƛ (f ∘ ev ∘ ⟨ π₁ , g ∘ π₂ ⟩)

  [-,-] : Functor (C ^op ×ᶜ C) C
  [-,-] .F₀ (A , B) = [ 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 $C^{op} \times C \to C .$ With a bit more effort, we can show that our defining equivalence between the $Hom -sets$ $Γ \times A \to B$ and $Γ \to B^{A}$ satisfies the naturality condition required to to characterise $-^{A}$ as the right adjoint to $- \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 (products _ _) (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 $- \times A$ has a right adjoint $-^{A},$ then $C$ is a Cartesian closed category, with the object $B^{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 .ε 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🔗

open /-Obj
open /-Hom
open Pullback

module _ B (exp : ∀ A → Exponential B A) where
  private module _ A where open Exponential (exp A) renaming (B^A to -^B₀) hiding (ƛ ; unlambda ; ev) public
  private module _ {A} where open Exponential (exp A) renaming (unlambda to app) using (ev ; ƛ) public

We refer to an object $B : C$ as exponentiable if, for every other $A : C,$ the exponential object $A^{B}$ exists. This means that we have a right adjoint $-^{B}$ to the functor $- \times B,$ by the discussion above. It will, however, be more useful to us to characterise exponentiability of $B$ by a condition on the slice category $C / 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 \to C / B,$ which sends an object $X$ to the product projection $π_{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 $B$ is exponentiable iff. we have a right adjoint functor $Δ_{B} ⊣ Π_{B} .$

Suppose $B$ is exponentiable. The value $Π_{B} (f)$ on a family $f : A \to B$ is defined to be the pullback

where the map $f^{B} : A^{B} \to B^{B},$ on the right, is the action of $(-)^{B}$ on $f .$ An application of the universal properties at hand shows that we can extend maps $h : X \to Y$ over $B$ to maps $Π_{B} (X) \to Π_{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 .com) ⟩∘⟨refl ⟩
          ƛ ((y .map ∘ h .map) ∘ ev) ∘ pb _ _ .p₁          ≡⟨ pushl (-^B .F-∘ _ _) ⟩
          ƛ (y .map ∘ ev) ∘ ƛ (h .map ∘ ev) ∘ pb _ _ .p₁   ∎

    f .F-id = sym $ pb _ _ .Pullback.unique
      (sym (eliml (-^B .F-id) ∙ intror refl)) (sym (!-unique _))

    f .F-∘ f g = sym $ pb _ _ .Pullback.unique
      (pulll (pb _ _ .p₁∘universal) ∙∙ pullr (pb _ _ .p₁∘universal) ∙∙ pulll (sym (-^B .F-∘ _ _)))
      (sym (!-unique _))

  exponentiable→constant-family⊣product
    : (pb : has-pullbacks C)
    → constant-family products ⊣ exponentiable→product pb
  exponentiable→constant-family⊣product pb =
    hom-iso-inv→adjoints (rem₁ _ .fst) (rem₁ _ .snd) nat where
    module b = Functor (constant-family products)
    module Π = Functor (exponentiable→product pb)

It remains to prove that this functor is actually a right adjoint to the constant-families functor $Δ_{B} : C \to C / B$ like we had claimed. We start with an elementary observation: given maps $f : A \to B$ and $q : X \to A^{B},$ asking for $λ (f \circ ev) \circ q = λ (π_{2}) \circ!$ is equivalent to asking for $f \circ λ^{- 1} (q) = π_{2},$ which is in turn equivalent to asking that $q$ be a map $Δ_{B} (X) \to f,$ over $B .$

    coh₁ : ∀ {X} (f : /-Obj B) (q : Hom X (-^B₀ (f .dom)))
         → (ƛ (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)

      where
        done : ƛ π₂ ∘ ! ≡ ƛ π₂
        done = Exponential.unique (exp _) _ $
             ap₂ _∘_ refl (ap₂ _⊗₁_ refl (sym (idl id)) ∙ ×-functor .F-∘ _ _)
          ∙∙ pulll (Exponential.commutes (exp _) _)
          ∙∙ (π₂∘⟨⟩ ∙ idl _)

    opaque
      rem₁ : ∀ {X} (f : /-Obj B)
           → Hom X (Π.₀ f) ≃ Slice C B .Precategory.Hom (b.₀ X) f
      rem₁ {X = X} f =

This is the last piece that we need to establish an equivalence between the $Hom -sets$ $Hom_{C} (X, Π_{B} (f))$ and $Hom_{C / B} (Δ_{B} (X), f),$ and even though it factors through the rather complicated path displayed below, it definitionally sends $h : Hom_{C} (X, Π_{B} (f))$ to $λ^{- 1} (p_{1} \circ h) .$ 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}$ we’ve been chasing.

        Hom X (Π.₀ f)
          ≃⟨ Pullback.pullback-univ (pb _ _) ⟩
        Σ (Hom X (-^B .F₀ (f .dom))) (λ h → Σ (Hom X top) λ h' → ƛ (f .map ∘ ev) ∘ h ≡ ƛ π₂ ∘ h')
          ≃⟨ Σ-ap-snd (λ x → Σ-contr-fst (has⊤ X)) ⟩
        Σ (Hom X (-^B .F₀ (f .dom))) (λ h → ƛ (f .map ∘ ev) ∘ h ≡ ƛ π₂ ∘ !)
          ≃⟨ Σ-ap (Equiv.inverse (ƛ , lambda-is-equiv _)) (coh₁ f) ⟩
        Σ (Hom (X ⊗₀ B) (f .dom)) (λ h → f .map ∘ h ≡ π₂)
          ≃⟨ Iso→Equiv ((λ x → record { com = x .snd }) , iso (λ x → _ , x .com) (λ _ → ext refl) (λ _ → ext refl)) ⟩
        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 products} {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.