jcreed blog > Another Parametricity Construction

Another Parametricity Construction

I wanted to write down another very cute construction that seems to work thanks to parametricity.
Claim: For any category $\C$, there exists a type $B$ such that we can faithfully embed $\C$ into types-over-$B$.
That is, for each object $C \in \C$ there exists a type $T_C$ and a morphism $p_C : T_C \to B$, such that the functions $g$ that fit in the diagram \[\begin{CD} T_{C} @>{g}>> T_{D} \\ @V{p_C}VV @VV{p_D}V\\ B @= B \\ \end{CD}\] are in bijective correspondence to the morphisms $C \to D \in \C$.

Here's how it works.

  1. Let $B$ be the type of copresheaves over $\C$, i.e. functors $\C \to \rset$.
  2. For each $C\in\C$, set \[T_C = (b : B) \x b(C) \qquad p_C\ \langle b, x\rangle = b\]
  3. Fix two objects $C, D \in \C$. Define the type $H$ by \[ H := (b : B) \to b(C) \to b(D)\] Observe that asking for an $g$ that fits in the commutative diagram above is equivalent to asking for a term of type of $H$. Given any morphism $f : C \to D$, we can construct a term \[ (\lambda b x . b(f)\ x) : H\] from it, by using functoriality of $b$. Conversely, given any term $h : H$, we can compute \[ h\ \C[C, \hbox{—}]\ \rid_C \in \C[C, D] \] The round trip starting from a morphism, converting to $H$, and converting back to a morphism is easily seen to be the identity. The other round trip requires parametricity.

    So let's prove that now. Let $h : H$ be given. We want to show \[ h \equiv (\lambda b x . b(h\ \C[C, \hbox{—}]\ \rid_C)\ x) \] By function extensionality it suffices to show for any $b: B$ and $x:b(C)$ that \[ h\ b\ x \equiv b\ (h\ \C[C, \hbox{—}]\ \rid_C)\ x \tag{*}\] Now consider the parametricity free theorem for $h$. It tells us:

    Suppose we have presheaves $b_1, b_2 : B$, and a family of relations \[\_{\sim_C}\_ : b_1(C) \to b_2(C) \to \rset\] indexed by objects $C$ of $\C$. Suppose these relations are compatible with presheaf restriction in the sense that for any morphism $f : C \to D$ we have that \[x \sim_D y \Rightarrow x|_f \sim_C y|_f \] for any $x \in b_1(D), y\in b_2(D)$.
    Suppose $x_1 \in b_1(C)$ and $x_2 \in b_2(C)$ and $x_1 \sim_C x_2$.
    Then $h\ b_1\ x_1 \sim_D h\ b_2\ x_2$.
    We obtain $(*)$ by invoking the free theorem at \[\begin{array}{ll} b_1 := b & x_1 := x \\ b_2 := \C[C, \hbox{—}] & x_2 := \rid_C\end{array}\] and the relation defined by \[y_1 \sim y_2 \quad :\Longleftrightarrow\quad y_1 \equiv b(y_2) (x)\]