jcreed blog > Parametricity and Comma Categories

Parametricity and Comma Categories

Here's something that seems to work. I like it because it seems to do what category theory does best: tell you what your definitions ought to be.

Shapes

Let's say a preshape is a functor $G : \D \to \C$ that preserves finite limits between two categories that have all finite limits. We say a preshape extends to a full shape whenever there exists
  1. A functor $F : \C \to \D$ going in the opposite direction that preserves "just about every finite structure". I'm going to leave this unspecified for now, but imagine that it means finite limits, finite colimits, exponentials, universe structure, etc.
  2. A natural transformation $\eta : \rid_\C \to GF$.
In other words: almost an adjunction $F \dashv G$, but missing the counit.

An Example To Think Of

The role of a shape is to answer, in an abstract way, the question: what's the $n$ for which we're doing parametricity with $n$-ary relations? An example of a shape is the pair of functors (that actually are adjoint) $F = \Delta$ and $G = \prod$ that have types \[ \Delta : \rset \to \rset^n : \prod\] and exhibit how you ($\Delta$) take a set to an $n$-tuple of sets by duplicating it, and ($\prod$) how you take the cartesian product of $n$ sets.

Shape Morphisms

A morphism from a shape $(F', G', \eta')$ to a shape $(F, G, \eta)$ consists of a functor $\delta$ (which, like $F$ and $F'$, should "preserve just about all finite structure") and a natural transformation $\gamma$ that fits in the left diagram below, such that the right diagram below commutes (maybe up to some natural isomorphism that I'm not going to concern myself with right now)

Moving to the Comma Category

Given a preshape $G : \D \to \C$, we can define another preshape $G' : \D' \to \C$ from it. We set $\D'$ to the comma category $\rid_\C / G$. The objects of $\D'$ are tuples $(C, D, f : C \to GD)$, and its morphisms are commutative squares arising from choices of morphisms in $\C$ and $\D$. The functor $G'$ we set to the projection $\D' \to \C$ that picks out the $C$-part of the tuple.

We note that we already have some candidate data from which to build a shape morphism from $(?, G', ?)$ to $(F, G, \eta)$, if only we had an $F'$ and $\eta'$. For we could define $\partial : \D' \to \D$ to be the projection that picks out the $D$-part of the tuple, and $\gamma : G' \to G \o \partial$ to be the projection that picks out the $f$-part of the tuple.

What is this situation really about, in the case of our example? $\D'$ is the category of $n$-ary relations and relation homomorphisms. $G'$ projects out the type of the total space. $\partial$ projects out the boundary; the $n$ types that the relation is among, as an object in $\D$. $G$ takes those types and yields their product. $\gamma$ tells us how to map from a point in the total space of the relation to its coordinates in the boundary types.

Parametricity

I claim that $G'$ is a preshape; check that it is a functor preserving finite limits. Also, for many structures of interest (exponentials, universes, etc.) it seems that if $\C$ and both $\D$ have that structure, then $\D'$ has it in a sensible way. So we can make the definition:
$\C$ has parametricity of shape $(F, G, \eta)$ if we can find $F', \eta'$ that
(Perhaps we might even ask for there to be a unique $F', \eta'$ that fulfill these conditions?)

Why do I think this has anything to do with parametricity theorems? If I have an object $C \in \C$, then the property above says that there is some morphism $\eta'_C : C \to G'F'C$. This takes the object $C$ to a point in the total space of a relation — the relation being the object $F'C \in \D'$. The map $\partial$ carries $F'C$ over to $\D$, where I find that it is the same as $FC$, the 'all-$C$' boundary. So $\eta'$ is really telling me that any element of $C$ belongs to the identity relation on $C$.

The real points get scored because $F'$ is supposed to "preserve all structure". I don't have to creatively decide what parametricity should say about function types, because I can extract the ump of the exponential. What happens if $C$ is an internal hom-object, like $C_1 \imp C_2$? $F$ is supposed to preserve "all structure", so $F(C_1 \imp C_2) = FC_1 \imp FC_2$ But that latter $\imp$ is taking place in $\D'$, and I can simply investigate what the exponential structure in that category must be (up to isomorphism), taking exponential structure in $\C$ and $\D$ as given.

Fortunately, it turns out to be exactly the "two functions are related if they map related things to related things" definition that we'd expect. And I think the right thing happens as well with universes. It goes something like: you supply a category $\C$ with some extra structure that stratifies its morphisms into levels, intuitively 'according to the size of their fibers'. A level-$i$ universe is a map $e_i : \E_i \to \U_i$ such that that any size-$i$ map arises uniquely as a pullback of it. We suppose $\C$ and $\D$ have universes for every level, and that $F$ preserves them, and we can describe them in $\rid_C/G$ &mdash finding that they are essentially types of codes for relations in the same way ordinary universes are types of codes for sets — and require that $F'$ preserve them.