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.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 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
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 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.  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 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.  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 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  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 _)


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 β©οΈ