module Cat.CartesianClosed.Locally where

Locally cartesian closed categoriesπŸ”—

A finitely complete category C\mathcal{C} is said to be locally Cartesian closed when each of its slice categories is Cartesian closed. Note that requiring finite limits in C\mathcal{C} does exclude some examples, since C\mathcal{C} might have each of its slices Cartesian closed, but lack a terminal object.1 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

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

Recall that, when thinking about dependent type theory in a category C\mathcal{C}, we have the following dictionary: The objects of C\mathcal{C} correspond to the contexts Ξ“,Ξ”,…\Gamma, \Delta, \dots, and the morphisms Ξ“β†’Ξ”\Gamma \to \Delta are the substitutions between those contexts. The objects in C/Ξ“\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 Ξ“βŠ’A\Gamma \vdash A to Ξ”βŠ’Οƒβˆ—A\Delta \vdash \sigma^*A, along the substitution Οƒ:Ξ”β†’Ξ“\sigma : \Delta \to \Gamma.

To make this a bit clearer, let’s focus on the simplest case, where Οƒ\sigma is the projection of a variable Ο€1:Ξ“.Aβ†’Ξ“\pi_1 : \Gamma.A \to \Gamma. Instantiating the discussion above, we discover that base change along Ο€1\pi_1 will map types Ξ“βŠ’B\Gamma \vdash B to their weakenings Ξ“,x:AβŠ’Ο€1βˆ—B\Gamma, x : A \vdash \pi_1^*B.

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

Ξ“,x:A⊒e:BΞ“βŠ’(Ξ»x.e):Ξ (x:A)B(x) \frac{ \Gamma, x : A \vdash e : B }{ \Gamma \vdash (\lambda x. e) : \Pi_{(x : A)}B(x) }

Ξ“βŠ’f:Ξ x:AB(x)Ξ“βŠ’e:AΞ“βŠ’f(x):B(e) \frac{ \Gamma \vdash f : \Pi_{x : A}B(x) \quad \Gamma \vdash e : A }{ \Gamma \vdash f(x) : B(e) }

which, by abstracting away the substitution of the argument3, expresses that there is an isomorphism between derivations Ξ“βŠ’f:Ξ (x:A)B(x)\Gamma \vdash f : \Pi_{(x : A)} B(x) and Ξ“,x:A⊒f(x):B(x)\Gamma, x : A \vdash f(x) : B(x). If we squint, this says precisely that Ξ \Pi is a right adjoint to the action of base change along Ο€1:Ξ“.Aβ†’A\pi_1 : \Gamma.A \to A!

This is our second characterisation of locally Cartesian closed categories. Generalising away from weakenings, we should have a correspondence between Hom(fβˆ—A,B)\mathbf{Hom}(f^*A, B) and Hom(A,Ξ fB)\mathbf{Hom}(A, \Pi_f B), for an arbitrary substitution f:Ξ“β†’Ξ”f : \Gamma \to \Delta. Back to categorical language, that is a right adjoint to the base change functor, fitting into an adjoint triple

Ξ£f⊣fβˆ—βŠ£Ξ f. \Sigma_f \dashv f^* \dashv \textstyle\Pi_f\text{.}

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β†’Af : X \to A, the product functor βˆ’Γ—f:C/Aβ†’C/A- \times f : \mathcal{C}/A \to \mathcal{C}/A is isomorphically given by

C/Aβ†’fβˆ—C/Xβ†’Ξ£fC/A, \mathcal{C}/A \xrightarrow{f^*} \mathcal{C}/X \xrightarrow{\Sigma_f} \mathcal{C}/A \text{,}

since products in a slice are implemented by pullbacks in C\mathcal{C}; We can chase a g:Yβ†’Ag : Y \to A along the above diagram to see that it first gets sent to fβˆ—gf^*g as in the diagram

by the pullback functor, then to f∘(fβˆ—g):XΓ—AYβ†’Af \circ (f^*g) : X \times_A Y \to A by the dependent sum. But this is exactly the object gΓ—fg \times f in C/A\mathcal{C}/A, so that βˆ’Γ—f- \times f and Ξ£ffβˆ—\Sigma_f f^* 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     = /-Hom-path $ idl _
    Slice-product-functor .inv∘eta x     = /-Hom-path $ idl _
    Slice-product-functor .natural x y f = /-Hom-path $ id-comm βˆ™ ap (id ∘_) (pullbacks _ _ .unique
      (pullbacks _ _ .pβ‚βˆ˜universal) (pullbacks _ _ .pβ‚‚βˆ˜universal βˆ™ idl _))

If we then have a functor Ξ f\Pi_f fitting into an adjoint triple Ξ£f⊣fβˆ—βŠ£Ξ f\Sigma_f \dashv f^* \dashv \Pi_f, we can compose that to obtain Ξ£ffβˆ—βŠ£Ξ ffβˆ—\Sigma_f f^* \dashv \Pi_f f^*, and, by the natural isomorphism we just constructed, βˆ’Γ—f⊣Πffβˆ—- \times f \dashv \Pi_f f^*. 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 C\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* _ _))

Recovering the adjunctionπŸ”—

Now suppose that each slice of C\mathcal{C} is Cartesian closed. How do we construct the dependent product Ξ f:C/Aβ†’C/B\Pi_f : \mathcal{C}/A \to \mathcal{C}/B? 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→Bf : A \to B is an exponentiable object in C/B\mathcal{C}/B, there is a product along ff functor, mapping from the double slice (C/B)/f→C/B(\mathcal{C}/B)/f \to \mathcal{C}/B, which is a right adjoint to the constant families functor C/B→(C/B)/f\mathcal{C}/B \to (\mathcal{C}/B)/f. And since (by the yoga of iterated slices) (C/B)/f(\mathcal{C}/B)/f is identical to C/A\mathcal{C}/A, this becomes a functor Πf:C/A→C/B\Pi_f : \mathcal{C}/A \to \mathcal{C}/B, 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 ff. We know that it’s a right adjoint to the constant families functor Ξ”f\Delta_f on C/B\mathcal{C}/B, and that constant families are given by Ο€2:gΓ—fβ†’f\pi_2 : g \times f \to f. Since the Cartesian product in a slice is given by pullback, the base change functor turns out naturally isomorphic to fβˆ—f^*, when regarded as a functor C/Bβ†’C/A\mathcal{C}/B \to \mathcal{C}/A through the equivalence (C/B)/fβ‰…C/A(\mathcal{C}/B)/f \cong \mathcal{C}/A.

  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 = /-Hom-path (idr _)
    remβ‚‚ .inv∘eta x = /-Hom-path (idr _)
    remβ‚‚ .natural x y f = /-Hom-path $
         idr _
      Β·Β· ap (pullbacks _ _ .universal) prop!
      Β·Β· sym (idl _)

  1. An example is the category of locales and local homeomorphisms, LH\mathbf{LH}. Each slice LH/X\mathbf{LH}/X is Cartesian closed β€” they’re even topoi β€” but LH\mathbf{LH} has no terminal object.β†©οΈŽ

  2. Indeed, even for the category Sets\mathbf{Sets}, showing local Cartesian closure is not at all straightforward: the local exponential fgf^g over BB is the set βˆ‘b:Bfβˆ’1(b)β†’gβˆ’1(b)\sum_{b : B} f^{-1}(b) \to g^{-1}(b), though this computation is best understood in terms of slices of sets.β†©οΈŽ

  3. To expand on the idea of this more categorical application, if we have Ξ“βŠ’f:Ξ x:AB(x)\Gamma \vdash f : \Pi_{x : A}B(x), we first β€œopen” it to uncover Ξ“,x:A⊒f(x):B(x)\Gamma, x : A \vdash f(x) : B(x); if we then have an argument Ξ“βŠ’a:A\Gamma \vdash a : A, then we can use substitution to obtain Ξ“βŠ’f(x)[a/x]:B(a)\Gamma \vdash f(x)[a/x] : B(a).β†©οΈŽ