Relating functors to relational functors with the parametricity translation

Question

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using parametricity? I tried showing that one obtains the theory of relational functors by applying the parametricity translation to the theory of functors, where relational functors are defined in Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages.

Specifically, if we are given \begin{align*} F_! &: \Type\to\Type\\ F_{\map} &: (A,B:\Type)\to(A\to B)\to(F_!A\to F_!B)\\ F_{\id}&:(A:\Type)\to F_{\map}(\id(A)) = \id(F_!A) \end{align*}

I was able to show (with generous hand-waving) that \begin{align*} F_!^R &: (A,B:\Type)\to \text{Rel}(A,B)\to\text{Rel}(F_!A,F_!B)\\ F_\map^R &:(A_0,A_1: \Type)\to(A^R:\text{Rel}(A_0,A_1))\to (B_0,B_1:\Type)\to(B^R:\text{Rel}(B_0,B_1))\\ &\quad\to(f_0:A_0\to B_0)\to(f_1 : A_1\to B_1)\\ &\quad\to((x_0:A_0)\to(x_1:A_1)\to A^R(x_0,x_1)\to B^R(f_0x_0,f_1x_1))\\ &\quad\to(x_0 : F_! A_0)\to(x_1 : F_! A_1)\to F_!^R(A_0,A_1,A^R,x_0,x_1) \\ &\quad\to F_!^R(B_0,B_1,B^R,F_\map (A_0,B_0,f_0,x_0),F_\map (A_1,B_1,f_1,x_1)) \end{align*}

But I am having trouble showing that $F_\id^R$ gives some form of the identity extension property, namely that $$A:\Type\vdash F_!^R(A,A,\text{Id}(A)) = \text{Id}(F_!^RA) $$

It seems to me that the pair $(F,F^R)$ should give a relational functor in the sense of definition 6.1.

Is my intuition that this should be the case correct, and if so, is there some higher level explanation for this (perhaps some sort of Yoneda embedding?)?

Answer 1

$(F, F^R)$ is not necessarily a relational functor. Define $F : \text{Set} \to \text{Set}$ to be the identity functor on sets and functions, but let ${F_!}^R$ send all relations to the trivial relation. Then ${F_{\text{map}}^R}$ trivially holds (along with ${F_{\text{id}}^R}$ and ${F_{\text{comp}}^R}$ which always hold for any $F$, because of the proof-irrelevance of equalities), but $F^R$ does not preserve identity relations.

Going back to the linked question: if a functor is defined internally in a parametric type theory, we don't really care about whether identity extension is derivable: we always get it as part of the "free theorem" package, so every internal $\text{Type} \to \text{Type}$ functor is also a relational functor externally.

Answer 2

I think you might be missing a couple of things. Let me answer three questions:

1. Is $F$ required to be a covariant functor, or do we expect those properties to hold for arbitrary $F : \textrm{Type}\to \textrm{Type}$?
2. Is $F_!^R$ something you expect to be able to choose arbitrarily or something you expect to be already defined?
3. Are $F_\textrm{id}^R$ and $F_\textrm{map}^R$ something you are going to define separately or something that must already follow from other definitions?

My answers to these questions are:

1. You have written $F_\textrm{map}$ that likely will not exist unless $F$ is a covariant functor. However, the relational functor $F_!^R$ exists for any type constructor $F_!$, not only for covariant functors.

2. For any given $F_!$, there is a fixed way of defining $F_!^R$. The construction of $F_!^R$ must proceed by induction on the type structure of $F_!$. The possible type structures are determined by the lambda-calculus for which you are defining these things. For example, in System F you need to show how to define $F_!^R$ for unit type, for products, for co-products, for function types, and for universally quantified types. The explicit form of $F_!^R$ is a function that transforms any given relation of type $\textrm{Rel}(A, B)$ into a relation of type $\textrm{Rel}(F_!A, F_!B)$.

3. The parametricity theorem says that any lambda-term satisfies the relational parametricity law. You can then derive the property that $F_!^R(\textrm{Id}(A))=\textrm{Id}(F_!A)$ for the identity relation. You can also derive the relational parametricity law of $F_\textrm{map}$ and that law will be what you are denoting by $F_\textrm{map}^R$.

Given a covariant type constructor $F_! : \textrm{Type} \to\textrm{Type}$ , the terms $F_\textrm{map}$ and $F_\textrm{id}$ cannot be chosen arbitrarily. Those terms must be derived from the type structure of $F_!$ in a fixed way, in order to satisfy the functor's laws.

There is only one freedom here, - that of choosing the type constructor $F_! : \textrm{Type} \to\textrm{Type}$. All other terms ($F_\textrm{map}$, $F_\textrm{id}$, and the relational objects $F_!^R$, $F_\textrm{map}^R$, $F_\textrm{id}^R$) follow rigidly with no possibility of making any further choices. Otherwise the required laws will not be satisfied.