Slices of Presheaf Categories

I wanted to give a little attention to a well-known, but I think under-hyped, lemma from elementary category theory. Honestly I think it's about as lovely and simple as the Yoneda lemma or the fact that the Grothendieck construction works, and it has a somewhat related flavor to both of them. You can find it mentioned here on nLab, which has a pointer to some nice sheaf-theoretic generalizations in MacLane and Moerdijk.

the statement of it is: Suppose $\C$ is a category, and $P$ is a presheaf in $\hat \C = \rset^{\C^\op}$. Then \[ \hat \C / P \cong \widehat{\int P} \] That is, the slice category $\hat \C / P$ whose objects are natural transformations $Q \to P$ of any other presheaf $Q$ into $P$, and whose morphisms are commutative triangles, is isomorphic to $\widehat {\int P}$, the presheaf category on the category of elements of $P$, whose objects are pairs $(C, x)$ consisting of an object $C\in \C$ and an element $x \in P(C)$ of the presheaf, and whose morphisms $(C, x) \to (D, y)$ are morphisms $f : C \to D \in \C$ such that $P(f)(y) = x$.

Proof

Stare at the following diagram:

(Mouseover to show other side of isomorphism) If we have a presheaf $Q \in \hat \C$ and a projection $\pi : Q \to P$, then the way we build a presheaf in $\widehat{\int P}$ is by taking the inverse image under $\pi^{-1}$: \[Q'(C, x) = (\pi(C))^{-1}(x)\] Conversely, if we have a presheaf $Q' \in \widehat{\int P}$, we can define \[Q(C) = \bigcup_{x \in P(C)} Q'(C, x)\] and the choice of what to do at morphisms in both directions is pretty much forced.

What It's Good For

For one thing, this is sort of the crux of the reason you can do dependent type theory in presheaf categories. Since slices of presheaf categories are themselves presheaf categories, and since all presheaf categories are cartesian closed, that means all presheaf categories are locally cartesian closed.

Another nice use of it was as a very useful simplifying tool when I was trying to think recently about what sort of situations you might find yourself in where you have a type theory and a type $\ii$ such that something like '$\ii \to \rtype$' is equivalent to a span of types, $(A\ B\ C : \rtype) \x (C \to A) \x (C \to B)$.

Restricting our attention to the situation where 'type' means 'presheaf in $\hat \C$ for some choice of category $\C$', this means that $\ii \in \hat\C$. And thinking Grothendieck-ily, you could instead of '$\ii \to \rtype$' just ask for a choice of type $P\in\hat\C$ and a map $P \to \ii$.

But the above lemma is telling us this is the same thing as a presheaf in $\widehat{\int \ii}$! And "a span of types in $\rset^{\C^\op}$" is also really just a presheaf-y notion, since it's the same thing as $(\rset^{\C^\op})^S = \rset^{\C^\op \x S}$ for the span category $S$ that has three objects $\{A_1, A_2, \star\}$ and only two nontrivial morphisms $\star \to A_1$ and $\star \to A_2$.

Therefore all we really need to find is a $\ii$ such that the base categories of these two different categories are the same, i.e. $\left(\int \ii\right)^\op \cong \C^\op \x S$. This is way simpler than trying to analyze all possible presheaves $\ii$ and other presheaves $P$, and their mappings into $\ii$ directly.

For example, I can say, let the category $\C$ be the category whose objects are

Contexts $\Gamma,\Delta,\Omega$ ::= $\cdot \celse \Gamma , x$ And whose morphisms $\Gamma \to \Delta$ are substitutions $\Gamma \prov \theta : \Delta$ whose syntax is Substitutions $\theta$ ::= $\cdot \celse \theta[M/ x]$ Terms $M$ ::= $x \celse \ep 1 \celse \ep 2$ which are typed like \[ {\Gamma \prov \theta : \Delta \qquad \Omega \prov M \over \Gamma, \Omega \prov \theta[M/x] : \Delta, x} \qquad {\over \cdot \prov \ep 1} \qquad {\over \cdot \prov \ep 2} \qquad {\over x \prov x} \] In the typing of substitutions, we don't assume that contexts have contraction, weakening, or exchange.

Now let $\ii$ be the presheaf in $\hat \C$ such that

$\ii(\cdot)$	$=$	$\{\ep 1, \ep 2\}$
$\ii(\Gamma, x)$	$=$	$\{\ep 1, \ep 2, x\}$

with the action of morphisms being the only reasonable thing it can be; syntactically carrying out the substitution.

I now claim that $(\int \ii)^\op$ is the same thing as $\C^\op \x S$. Let's describe a map $\rho$ from $\C^\op \x S$ to $(\int \ii)^\op$. The input we're given is an object $\Gamma \in \C$ and an object of $S$. The object of $S$ can either be $\star, A_1$, or $A_2$. We need to output a pair consisting of an object in $\C$ and an element of $\ii(\Gamma)$. So we define \[\rho(\Gamma, \star) = ((\Gamma, x), x) \] \[\rho(\Gamma, A_1) = (\Gamma, \ep 1) \] \[\rho(\Gamma, A_2) = (\Gamma, \ep 2) \] And if we examine the morphisms of $\int \ii$ — which are substitutions preserving the distinguished element — we find that they can be classified into "doing something to the context $\Gamma$" and "doing something to what's left", i.e. "a morphism in $\C^\op$" and "a morphism in $S$", respectively.

And I think this example works even if you do add various structural rules to $\Gamma$. Which is interesting since as far as I can tell, Bernardy-Moulin internalized parametricity seems to require — or at least naturally works best with — exactly the structural rules it has, namely, weakening, exchange, and not contraction. Still pretty mysterious to me why! I suppose it must have something to do with what happens with the surrounding context, since everything I'm doing above is considering "closed" types that are full-stop presheaves not depending on any other variables.