module Cat.CartesianClosed.Locally where

Locally cartesian closed categoriesπŸ”—

A finitely complete category is said to be locally Cartesian closed when each of its slice categories is Cartesian closed. Note that requiring finite limits in does exclude some examples, since 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
    has-is-lex : Finitely-complete C
    slices-cc  : βˆ€ A β†’ Cartesian-closed (Slice C A)
      (Slice-products (Finitely-complete.pullbacks has-is-lex))

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 internal type theory.

Recall that, when thinking about dependent type theory in a category we have the following dictionary: The objects of correspond to the contexts and the morphisms are the substitutions between those contexts. The objects in are the types in context . From this point of view, the pullback functors implement substitution in a dependent type, mapping a type to along the substitution

To make this a bit clearer, let’s focus on the simplest case, where is the projection of a variable Instantiating the discussion above, we discover that base change along will map types to their weakenings

Under this correspondence, what do dependent function types correspond to? Let’s roll up our sleeves and write out some gosh-darn 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 argument3, expresses that there is an isomorphism between derivations and If we squint, this says precisely that is a right adjoint to the action of base change along

This is our second characterisation of locally Cartesian closed categories. Generalising away from weakenings, we should have a correspondence between and for an arbitrary substitution 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 the product functor is isomorphically given by

since products in a slice are implemented by pullbacks in We can chase a along the above diagram to see that it first gets sent to as in the diagram

by the pullback functor, then to by the dependent sum. But this is exactly the object in so that and 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 fitting into an adjoint triple we can compose that to obtain and, by the natural isomorphism we just constructed, 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 is Cartesian closed.

    : (Ξ 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 is Cartesian closed. How do we construct the dependent product 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 is an exponentiable object in there is a product along functor, mapping from the double slice which is a right adjoint to the constant families functor And since (by the yoga of iterated slices) is identical to this becomes a functor of the right type.

    : βˆ€ {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 We know that it’s a right adjoint to the constant families functor on , and that constant families are given by Since the Cartesian product in a slice is given by pullback, the base change functor turns out naturally isomorphic to when regarded as a functor through the equivalence

    : βˆ€ {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))
    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 _)

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

  2. Indeed, even for the category showing local Cartesian closure is not at all straightforward: the local exponential over is the set 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 we first β€œopen” it to uncover if we then have an argument then we can use substitution to obtain β†©οΈŽ