open import Cat.Functor.Adjoint.Compose
open import Cat.Instances.Slice.Twice
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Exponential
open import Cat.Instances.Functor
open import Cat.Diagram.Pullback
open import Cat.Functor.Pullback
open import Cat.Diagram.Product
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Prelude

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

module Cat.CartesianClosed.Locally where

open make-natural-iso
open Functor
open /-Obj
open /-Hom

Locally cartesian closed categories🔗

A finitely complete category $\mathcal{C}$ is said to be locally Cartesian closed when each of its slice categories is Cartesian closed. Note that requiring finite limits in $\mathcal{C}$ does exclude some examples, since $\mathcal{C}$ might have each of its slices Cartesian closed, but lack a terminal object.¹ With the extra condition, a locally Cartesian closed category is Cartesian closed.

record Locally-cartesian-closed {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
  field
    has-is-lex : Finitely-complete C
    slices-cc  : ∀ A → Cartesian-closed (Slice C A)
      (Slice-products (Finitely-complete.pullbacks has-is-lex))
      Slice-terminal-object

module _ {o ℓ} (C : Precategory o ℓ) (fp : Finitely-complete C) where
  open Locally-cartesian-closed
  open Finitely-complete fp
  open Cat.Reasoning C
  open Pullback

  module _ {A : Ob} where
    private module Fc = Cat.Reasoning Cat[ Slice C A , Slice C A ]
    ×/ = Binary-products.×-functor (Slice C A) (Slice-products pullbacks)
    open make-natural-iso

The idea of exponentials in a slice is pretty complicated², so fortunately, there is an alternative characterisation of local cartesian closure, which is informed by $\mathcal{C}\text{’s}$ internal type theory.

Recall that, when thinking about dependent type theory in a category $\mathcal{C}\text{,}$ we have the following dictionary: The objects of $\mathcal{C}$ correspond to the contexts $\Gamma ,\Delta ,\dots \text{,}$ and the morphisms $\Gamma \to \Delta$ are the substitutions between those contexts. The objects in $\mathcal{C}/\Gamma$ are the types in context $\Gamma$. From this point of view, the pullback functors implement substitution in a dependent type, mapping a type $\Gamma ⊢A$ to $\Delta ⊢{\sigma }^{\ast }A\text{,}$ along the substitution $\sigma :\Delta \to \Gamma \text{.}$

To make this a bit clearer, let’s focus on the simplest case, where $\sigma$ is the projection of a variable ${\pi }_1:\Gamma .A\to \Gamma \text{.}$ Instantiating the discussion above, we discover that base change along ${\pi }_1$ will map types $\Gamma ⊢B$ to their weakenings $\Gamma ,x:A⊢{\pi }_1^{\ast }B\text{.}$

Under this correspondence, what do dependent function types correspond to? Let’s roll up our sleeves and write out some gosh-darn $\Gamma \text{s}$ and turnstiles. It’s not much, but it’s honest work. We have the introduction and elimination rules

which, by abstracting away the substitution of the argument³, expresses that there is an isomorphism between derivations $\Gamma ⊢f:{\Pi }_{(x:A)}B(x)$ and $\Gamma ,x:A⊢f(x):B(x)\text{.}$ If we squint, this says precisely that $\Pi$ is a right adjoint to the action of base change along ${\pi }_1:\Gamma .A\to A\text{!}$

This is our second characterisation of locally Cartesian closed categories. Generalising away from weakenings, we should have a correspondence between $\mathbf{Hom}(f^{\ast }A,B)$ and $\mathbf{Hom}(A,{\Pi }_{f}B)\text{,}$ for an arbitrary substitution $f:\Gamma \to \Delta \text{.}$ Back to categorical language, that is a right adjoint to the base change functor, fitting into an adjoint triple

From dependent products🔗

But how does this correlate to the characterisation in terms of Cartesian closed slices? Other than the intuition about “function types (in context) between dependent types”, we can do some honest category theory. First, observe that, for $f:X\to A\text{,}$ the product functor $-\times f:\mathcal{C}/A\to \mathcal{C}/A$ is isomorphically given by

since products in a slice are implemented by pullbacks in $\mathcal{C}\text{;}$ We can chase a $g:Y\to A$ along the above diagram to see that it first gets sent to $f^{\ast }g$ as in the diagram

by the pullback functor, then to $f\circ (f^{\ast }g):X{\times }_{A}Y\to A$ by the dependent sum. But this is exactly the object $g\times f$ in $\mathcal{C}/A\text{,}$ so that $-\times f$ and ${\Sigma }_f{f}^{\ast }$ are indeed naturally isomorphic.

    Slice-product-functor : ∀ {X} → make-natural-iso
      (Σf (X .map) F∘ Base-change pullbacks (X .map))
      (Bifunctor.Left ×/ X)

    Slice-product-functor .eta x .map      = id
    Slice-product-functor .eta x .commutes = idr _ ∙ pullbacks _ _ .square
    Slice-product-functor .inv x .map      = id
    Slice-product-functor .inv x .commutes = idr _ ∙ sym (pullbacks _ _ .square)
    Slice-product-functor .eta∘inv x     = ext $ idl _
    Slice-product-functor .inv∘eta x     = ext $ idl _
    Slice-product-functor .natural x y f = ext $ id-comm ∙ ap (id ∘_) (pullbacks _ _ .unique
      (pullbacks _ _ .p₁∘universal) (pullbacks _ _ .p₂∘universal ∙ idl _))

If we then have a functor ${\Pi }_f$ fitting into an adjoint triple ${\Sigma }_f⊣f^{\ast }⊣{\Pi }_f\text{,}$ we can compose that to obtain ${\Sigma }_f{f}^{\ast }⊣{\Pi }_f{f}^{\ast }\text{,}$ and, by the natural isomorphism we just constructed, $-\times f⊣{\Pi }_f{f}^{\ast }\text{.}$ Since a right adjoint to Cartesian product is exactly the definition of an exponential object, such an adjoint triple serves to conclude that each slice of $\mathcal{C}$ is Cartesian closed.

  dependent-product→lcc
    : (Πf    : ∀ {a b} (f : Hom a b) → Functor (Slice C a) (Slice C b))
    → (f*⊣Πf : ∀ {a b} (f : Hom a b) → Base-change pullbacks f ⊣ Πf f)
    → Locally-cartesian-closed C
  dependent-product→lcc Πf adj = record { has-is-lex = fp ; slices-cc = slice-cc } where
    slice-cc : (A : Ob) → Cartesian-closed (Slice C A) _ _
    slice-cc A = product-adjoint→cartesian-closed (Slice C A) _ _
      (λ f → Πf (f .map) F∘ Base-change pullbacks (f .map))
      λ A → adjoint-natural-isol (to-natural-iso Slice-product-functor)
              (LF⊣GR (adj _) (Σf⊣f* _ _))

module _ {o ℓ} (C : Precategory o ℓ) (lcc : Locally-cartesian-closed C) where
  open Locally-cartesian-closed lcc
  open Finitely-complete has-is-lex
  open Cat.Reasoning C
  open Pullback

  private
    module _ A where open Cartesian-closed (slices-cc A) public

    prod/ : ∀ {a} → has-products (Slice C a)
    prod/ = Slice-products pullbacks

    pullback/ : ∀ {b} → has-pullbacks (Slice C b)
    pullback/ = Slice-pullbacks pullbacks

Recovering the adjunction🔗

Now suppose that each slice of $\mathcal{C}$ is Cartesian closed. How do we construct the dependent product ${\Pi }_f:\mathcal{C}/A\to \mathcal{C}/B\text{?}$ Happily, this is another case where we just have to assemble preëxisting parts, like we’re putting together a theorem from IKEA.

We already know that, since $f:A\to B$ is an exponentiable object in $\mathcal{C}/B\text{,}$ there is a product along $f$ functor, mapping from the double slice $(\mathcal{C}/B)/f\to \mathcal{C}/B\text{,}$ which is a right adjoint to the constant families functor $\mathcal{C}/B\to (\mathcal{C}/B)/f\text{.}$ And since (by the yoga of iterated slices) $(\mathcal{C}/B)/f$ is identical to $\mathcal{C}/A\text{,}$ this becomes a functor ${\Pi }_f:\mathcal{C}/A\to \mathcal{C}/B\text{,}$ of the right type.

  lcc→dependent-product
    : ∀ {a b} (f : Hom a b) → Functor (Slice C a) (Slice C b)
  lcc→dependent-product {a} {b} f =
       exponentiable→product _ _ _ _ (has-exp b (cut f)) pullback/
    F∘ Slice-twice f

It remains to verify that it’s actually an adjoint to pullback along $f\text{.}$ We know that it’s a right adjoint to the constant families functor ${\Delta }_f$ on $\mathcal{C}/B$, and that constant families are given by ${\pi }_2:g\times f\to f\text{.}$ Since the Cartesian product in a slice is given by pullback, the base change functor turns out naturally isomorphic to $f^{\ast }\text{,}$ when regarded as a functor $\mathcal{C}/B\to \mathcal{C}/A$ through the equivalence $(\mathcal{C}/B)/f\cong \mathcal{C}/A\text{.}$

  lcc→pullback⊣dependent-product
    : ∀ {a b} (f : Hom a b) → Base-change pullbacks f ⊣ lcc→dependent-product f
  lcc→pullback⊣dependent-product {b = b} f = adjoint-natural-isol
    (to-natural-iso rem₂) (LF⊣GR rem₁ (Twice⊣Slice f))
    where
    rem₁ : constant-family prod/ ⊣ exponentiable→product (Slice C _) _ _ _ _ _
    rem₁ = exponentiable→constant-family⊣product _ _ _ _ _ _

    rem₂ : make-natural-iso (Twice-slice f F∘ constant-family prod/)
                            (Base-change pullbacks f)
    rem₂ .eta x .map      = id
    rem₂ .eta x .commutes = idr _
    rem₂ .inv x .map      = id
    rem₂ .inv x .commutes = idr _
    rem₂ .eta∘inv x = ext (idr _)
    rem₂ .inv∘eta x = ext (idr _)
    rem₂ .natural x y f = ext $
         idr _
      ∙∙ ap (pullbacks _ _ .universal) prop!
      ∙∙ sym (idl _)