module Cat.CartesianClosed.Locally where

# 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.^{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

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^{2}, so fortunately, there is an
alternative characterisation of local cartesian closure, which is
informed by
$\mathcal{C}$βs
*internal type theory*.

Recall that, when thinking about dependent type theory in a category
$\mathcal{C}$,
we have the following dictionary: The objects of
$\mathcal{C}$
correspond to the *contexts*
$\Gamma, \Delta, \dots$,
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 \vdash A$
to
$\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
$\pi_1 : \Gamma.A \to \Gamma$.
Instantiating the discussion above, we discover that base change along
$\pi_1$
will map types
$\Gamma \vdash B$
to their *weakenings*
$\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
$\Gamma$s
and turnstiles. Itβs not much, but itβs honest work. We have the
introduction and elimination rules

$\frac{ \Gamma, x : A \vdash e : B }{ \Gamma \vdash (\lambda x. e) : \Pi_{(x : A)}B(x) }$

$\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 argument^{3}, expresses that there is an
isomorphism between derivations
$\Gamma \vdash f : \Pi_{(x : A)} B(x)$
and
$\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
$\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 $\mathbf{Hom}(f^*A, B)$ and $\mathbf{Hom}(A, \Pi_f B)$, for an arbitrary substitution $f : \Gamma \to \Delta$. Back to categorical language, that is a right adjoint to the base change functor, fitting into an adjoint triple

$\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 \to A$, the product functor $- \times f : \mathcal{C}/A \to \mathcal{C}/A$ is isomorphically given by

$\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 $\mathcal{C}$; We can chase a $g : Y \to A$ along the above diagram to see that it first gets sent to $f^*g$ as in the diagram

by the pullback functor, then to $f \circ (f^*g) : X \times_A Y \to A$ by the dependent sum. But this is exactly the object $g \times f$ in $\mathcal{C}/A$, so that $- \times f$ and $\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 $\Pi_f$ fitting into an adjoint triple $\Sigma_f \dashv f^* \dashv \Pi_f$, we can compose that to obtain $\Sigma_f f^* \dashv \Pi_f f^*$, and, by the natural isomorphism we just constructed, $- \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 $\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$? 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$,
there is a *product along
$f$
functor*, mapping from the double slice
$(\mathcal{C}/B)/f \to \mathcal{C}/B$,
which is a right adjoint to the constant families
functor
$\mathcal{C}/B \to (\mathcal{C}/B)/f$.
And since (by the yoga of iterated
slices)
$(\mathcal{C}/B)/f$
is identical to
$\mathcal{C}/A$,
this becomes a functor
$\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
$f$.
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$.
Since the Cartesian product in a slice is given by pullback, the base
change functor turns out naturally isomorphic to
$f^*$,
when regarded as a functor
$\mathcal{C}/B \to \mathcal{C}/A$
through the equivalence
$(\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 _)

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

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

To expand on the idea of this more

*categorical*application, if we have $\Gamma \vdash f : \Pi_{x : A}B(x)$, we first βopenβ it to uncover $\Gamma, x : A \vdash f(x) : B(x)$; if we then have an argument $\Gamma \vdash a : A$, then we can use substitution to obtain $\Gamma \vdash f(x)[a/x] : B(a)$.β©οΈ