# What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this:
funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2
One may note a similarity in the definition of a (binary) logical relation
f1 [A -> B] f2 being:
∀ x1 x2 → x1 [A] x2 -> f1 x1 [B] f2 x2.

What is the relation of logical relations to function extensionality? Is there perhaps a relation to eta-equality?

• Might be relevant, since Univalence implies extensionality: arxiv.org/abs/1909.05027 Mar 23, 2021 at 4:56

Indeed there is a similarity in these two definitions.

Function extensionality that you showed is just a condition that specifies when two functions are equal.

If we talk about logical relations then a relation between two functions of types $$A \to B$$ does not necessarily have to express equality between two functions. But the equality relation is a possible binary relation between functions. Let us see how we can formulate a logical relation that specifies that two functions (both of type $$A \to B$$) are equal.

Denote by $$A \leftrightarrow B$$ the type of relations between values of types $$A$$ and $$B$$. The identity relation for the type $$A$$ is denoted by $$[\textrm{id}^A]: A \leftrightarrow A$$.

The logical relation for the extensional equality is formulated like this: Two functions are equal when they are in the identity relation for the type $$A \to B$$. That identity relation is denoted by $$[\textrm{id}^{A \to B}]$$. Then we can rewrite the Agda definition of the extensional equality in the language of relations like this:

$$f_1\, [\textrm{id}^{A \to B}]\, f_2$$ means $$\forall x_1,\, x_2$$ if $$x_1 \,[\textrm{id}^{A}]\, x_2$$ then $$f_1 (x_1) \,[\textrm{id}^{B}]\, f_2 (x_2)$$

Now we can further rewrite this definition via the function-type construction for relations. The function-type construction is defined like this: Given any two relations $$[r] : A \leftrightarrow B$$ and $$[s]:C\leftrightarrow D$$, we can define the relation $$[r\to s]: (A \to C) \leftrightarrow (B \to D)$$ by the formula similar to what you wrote: for any two functions $$f: A\to C$$ and $$g: B\to D$$, we have:

$$f\, [r\to s]\, g$$ means $$\forall x:A,\, y:B$$, if $$x \,[r]\, y$$ then $$f(x) \,[s]\, g(y)$$

Now if we set $$A=B$$, $$C = D$$, $$[r] = [\textrm{id}^A]$$, and $$[s] = [\textrm{id}^C]$$, then we will get: $$[r \to s] = [\textrm{id}^{A\to C}]$$. So, the identity relation on functions is obtained by the function-type construction from identity relations on types A and B. That's all it seems to be.

• This answer is totally correct, but let me add one additional comment. Parametric models satisfy the identity extension property: if $A[a]$ is a type with a free variable $a$, and $\mathsf{Id}_X$ is the identity relation for $X$, then $[\![ A[a] ]\!] (\mathsf{Id}_X/a) = \mathsf{Id}_{A[X]}$. This forces all parametric models to satisfy the condition above. Mar 31, 2023 at 8:28
• @NeelKrishnaswami It is hard for me to follow the notation in your comment. I will revise my answer a bit. I think the main point is that we must show a proof that [A -> B] = id follows from [A] = id and [B] = id, it does not follow automatically. Mar 31, 2023 at 8:34
• Sorry! I didn't think my commented warranted a whole new answer, but comments make it hard to use rich notation... Mar 31, 2023 at 8:36
• @NeelKrishnaswami I have rewritten my answer and introduced new notation. I showed the derivation now. I'm not an expert in programming language theory, and I don't really understand the notation or the substance of what's going on in Reynolds's papers. For example, you said that "parametric models" will satisfy the "identity extension lemma". I think a practical programmer will not need to worry about the details of the models of the programming language. A programmer would never expect the programming language to implement a model that doesn't satisfy the identity extension lemma. Mar 31, 2023 at 9:14