# Relating functors to relational functors with the parametricity translation

$$\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?)?

$$(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.