<p><span class="math-container">$(F, F^R)$</span> is not necessarily a relational functor. Define <span class="math-container">$F : \text{Set} \to \text{Set}$</span> to be the identity functor on sets and functions, but let <span class="math-container">${F_!}^R$</span> send all relations to the trivial relation. Then <span class="math-container">${F_{\text{map}}^R}$</span> trivially holds (along with <span class="math-container">${F_{\text{id}}^R}$</span> and <span class="math-container">${F_{\text{comp}}^R}$</span> which always hold for any <span class="math-container">$F$</span>, because of the proof-irrelevance of equalities), but <span class="math-container">$F^R$</span> does not preserve identity relations.</p>
<p>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 &quot;free theorem&quot; package, so every internal <span class="math-container">$\text{Type} \to \text{Type}$</span> functor is also a relational functor externally.</p>

CC BY-SA 4.0
2021-03-15T07:46:11.873Z
2021-03-15T18:36:17.590Z
2021-03-15T18:36:17.590Z
András Kovács
<p>I think you might be missing a couple of things. Let me answer three questions:</p>
<ol>
<li>Is <span class="math-container">$F$</span> required to be a covariant functor, or do we expect those properties to hold for arbitrary <span class="math-container">$F : \textrm{Type}\to \textrm{Type}$</span>?</li>
<li>Is <span class="math-container">$F_!^R$</span> something you expect to be able to choose arbitrarily or something you expect to be already defined?</li>
<li>Are <span class="math-container">$F_\textrm{id}^R$</span> and <span class="math-container">$F_\textrm{map}^R$</span> something you are going to define separately or something that must already follow from other definitions?</li>
</ol>
<p>My answers to these questions are:</p>
<ol>
<li><p>You have written <span class="math-container">$F_\textrm{map}$</span> that likely will not exist unless <span class="math-container">$F$</span> is a covariant functor. However, the relational functor <span class="math-container">$F_!^R$</span> exists for any type constructor <span class="math-container">$F_!$</span>, not only for covariant functors.</p>
</li>
<li><p>For any given <span class="math-container">$F_!$</span>, there is a fixed way of defining <span class="math-container">$F_!^R$</span>. The construction of <span class="math-container">$F_!^R$</span> must proceed by induction on the type structure of <span class="math-container">$F_!$</span>. 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 <span class="math-container">$F_!^R$</span> for unit type, for products, for co-products, for function types, and for universally quantified types. The explicit form of <span class="math-container">$F_!^R$</span> is a function that transforms any given relation of type <span class="math-container">$\textrm{Rel}(A, B)$</span> into a relation of type <span class="math-container">$\textrm{Rel}(F_!A, F_!B)$</span>.</p>
</li>
<li><p>The parametricity theorem says that any lambda-term satisfies the relational parametricity law. You can then <em>derive</em> the property that <span class="math-container">$F_!^R(\textrm{Id}(A))=\textrm{Id}(F_!A)$</span> for the identity relation. You can also derive the relational parametricity law of <span class="math-container">$F_\textrm{map}$</span> and that law will be what you are denoting by <span class="math-container">$F_\textrm{map}^R$</span>.</p>
</li>
</ol>
<p>Given a covariant type constructor <span class="math-container">$F_! : \textrm{Type} \to\textrm{Type}$</span> , the terms <span class="math-container">$F_\textrm{map}$</span> and <span class="math-container">$F_\textrm{id}$</span> cannot be chosen arbitrarily. Those terms must be derived from the type structure of <span class="math-container">$F_!$</span> in a fixed way, in order to satisfy the functor's laws.</p>
<p>There is only one freedom here, - that of choosing the type constructor <span class="math-container">$F_! : \textrm{Type} \to\textrm{Type}$</span>. All other terms (<span class="math-container">$F_\textrm{map}$</span>, <span class="math-container">$F_\textrm{id}$</span>, and the relational objects <span class="math-container">$F_!^R$</span>, <span class="math-container">$F_\textrm{map}^R$</span>, <span class="math-container">$F_\textrm{id}^R$</span>) follow rigidly with no possibility of making any further choices. Otherwise the required laws will not be satisfied.</p>

CC BY-SA 4.0
2023-01-05T23:24:47.243Z
Thanks for your answer. Here I assume we are given $F, F_!, F_{map}, F_{id}$ (as terms). The terms $F_!^R, F_{id}^R, F_{map}^R$ are defined as the parametricity translation, as you mention, applied to the terms $F_!, F_{id}, F_{map}$.
Couchy
CC BY-SA 4.0
2023-01-06T09:35:45.297Z
@Couchy In my view, once you choose $F_!$, 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 actually only one freedom here, - that of choosing the type constructor $F_!$. Everything else follows rigidly with no possibility of making any further choices, if we want to satisfy the required laws.
winitzki
CC BY-SA 4.0
2023-01-05T21:28:30.873Z
2023-01-09T14:11:51.443Z
2023-01-09T14:11:51.443Z
winitzki
<p><span class="math-container">$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$</span>
In attempting to answer the question: <a href="https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici/136624#136624">Rigorous proof that parametric polymorphism implies naturality using parametricity?</a> I tried showing that one obtains the theory of <em>relational functors</em> by applying the parametricity translation to the theory of functors, where relational functors are defined in <a href="https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf" rel="noreferrer">Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages</a>.</p>
<p>Specifically, if we are given
<span class="math-container">\begin{align*}
F_! &amp;: \Type\to\Type\\
F_{\map} &amp;: (A,B:\Type)\to(A\to B)\to(F_!A\to F_!B)\\
F_{\id}&amp;:(A:\Type)\to F_{\map}(\id(A)) = \id(F_!A)
\end{align*}</span></p>
<p>I was able to show (with generous hand-waving) that
<span class="math-container">\begin{align*}
F_!^R &amp;: (A,B:\Type)\to \text{Rel}(A,B)\to\text{Rel}(F_!A,F_!B)\\
F_\map^R &amp;:(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))\\
&amp;\quad\to(f_0:A_0\to B_0)\to(f_1 : A_1\to B_1)\\
&amp;\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))\\
&amp;\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) \\
&amp;\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*}</span></p>
<p>But I am having trouble showing that <span class="math-container">$F_\id^R$</span> gives some form of the identity extension property, namely that
<span class="math-container">$$A:\Type\vdash F_!^R(A,A,\text{Id}(A)) = \text{Id}(F_!^RA) $$</span></p>
<p>It seems to me that the pair <span class="math-container">$(F,F^R)$</span> should give a relational functor in the sense of <a href="https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf" rel="noreferrer">definition 6.1</a>.</p>
<p>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?)?</p>

<type-theory><ct.category-theory><parametricity>
Relating functors to relational functors with the parametricity translation
Couchy
# Relating functors to relational functors with the parametricity translation

(Asked by: username_0 on 2021-03-14)

$\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?](https://cs.stackexchange.com/questions/136359/rigorous-proof-that-parametric-polymorphism-implies-naturality-using-parametrici/136624#136624) 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](https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf).

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](https://www.cs.bham.ac.uk/%7Eudr/papers/logical-relations-and-parametricity.pdf).

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

**Tags:** type-theory, ct.category-theory, parametricity

---

## 2 answers

### Answer by username_1 on 2021-03-15. Score: 4

$(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 by username_2 on 2023-01-05. Score: 0

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.

> **Comments:**
> **username_0**: Thanks for your answer. Here I assume we are given $F, F_!, F_{map}, F_{id}$ (as terms). The terms $F_!^R, F_{id}^R, F_{map}^R$ are defined as the parametricity translation, as you mention, applied to the terms $F_!, F_{id}, F_{map}$.  
> **username_2**: @Couchy In my view, once you choose $F_!$, 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 actually only one freedom here, - that of choosing the type constructor $F_!$. Everything else follows rigidly with no possibility of making any further choices, if we want to satisfy the required laws.  

---

