3
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.