<p>Indeed there is a similarity in these two definitions.</p>
<p>Function extensionality that you showed is just a condition that specifies when two functions are equal.</p>
<p>If we talk about logical relations then a relation between two functions of types <span class="math-container">$A \to B$</span> 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 <span class="math-container">$A \to B$</span>) are equal.</p>
<p>Denote by <span class="math-container">$A \leftrightarrow B$</span> the type of relations between values of types <span class="math-container">$A$</span> and <span class="math-container">$B$</span>. The identity relation for the type <span class="math-container">$A$</span> is denoted by <span class="math-container">$[\textrm{id}^A]: A \leftrightarrow A$</span>.</p>
<p>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 <span class="math-container">$A \to B$</span>. That identity relation is denoted by <span class="math-container">$[\textrm{id}^{A \to B}]$</span>. Then we can rewrite the Agda definition of the extensional equality in the language of relations like this:</p>
<p><span class="math-container">$f_1\, [\textrm{id}^{A \to B}]\, f_2$</span> means <span class="math-container">$\forall x_1,\, x_2$</span> if <span class="math-container">$ x_1 \,[\textrm{id}^{A}]\, x_2$</span> then <span class="math-container">$f_1 (x_1) \,[\textrm{id}^{B}]\, f_2 (x_2)$</span></p>
<p>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 <span class="math-container">$[r] : A \leftrightarrow B$</span>  and <span class="math-container">$[s]:C\leftrightarrow D $</span>, we can define the relation <span class="math-container">$[r\to s]: (A \to C)  \leftrightarrow (B \to D)$</span> by the formula similar to what you wrote: for any two functions <span class="math-container">$f: A\to C$</span> and <span class="math-container">$g: B\to D$</span>, we have:</p>
<p><span class="math-container">$f\, [r\to s]\, g$</span> means <span class="math-container">$\forall x:A,\, y:B$</span>, if <span class="math-container">$ x \,[r]\, y$</span> then <span class="math-container">$f(x) \,[s]\, g(y)$</span></p>
<p>Now if we set <span class="math-container">$A=B$</span>, <span class="math-container">$C = D$</span>, <span class="math-container">$[r] = [\textrm{id}^A]$</span>, and <span class="math-container">$[s] = [\textrm{id}^C]$</span>, then we will get: <span class="math-container">$[r \to s] = [\textrm{id}^{A\to C}]$</span>. So, the identity relation on functions is obtained by the function-type construction from identity relations on types <code>A</code> and <code>B</code>. That's all it seems to be.</p>

CC BY-SA 4.0
2023-03-31T08:28:26.557Z
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.
Neel Krishnaswami
CC BY-SA 4.0
2023-03-31T08:34:46.077Z
@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.
winitzki
CC BY-SA 4.0
2023-03-31T08:36:24.777Z
Sorry! I didn't think my commented warranted a whole new answer, but comments make it hard to use rich notation...
Neel Krishnaswami
CC BY-SA 4.0
2023-03-31T09:14:45.033Z
@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.
winitzki
CC BY-SA 4.0
2023-02-28T13:51:28.647Z
2023-03-31T09:18:14.243Z
2023-03-31T09:18:14.243Z
winitzki
<p>In Agda function extensionality can be defined like this:<br />
<code>funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -&gt; f1 x1 ≡ f2 x2) → f1 ≡ f2</code><br />
One may note a similarity in the definition of a (binary) logical relation<br />
<code>f1 [A -&gt; B] f2</code> being:<br />
<code>∀ x1 x2 → x1 [A] x2 -&gt; f1 x1 [B] f2 x2</code>.</p>
<p>What is the relation of logical relations to function extensionality?
Is there perhaps a relation to eta-equality?</p>

CC BY-SA 4.0
2021-03-23T04:56:09.823Z
Might be relevant, since Univalence implies extensionality: https://arxiv.org/abs/1909.05027
Joey Eremondi
<type-theory><parametricity><logical-relations>
What is the relation of parametricity and function extensionality?
Łukasz Lew
# What is the relation of parametricity and function extensionality?

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

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?

**Tags:** type-theory, parametricity, logical-relations

> **Comments:**
> **username_1**: Might be relevant, since Univalence implies extensionality: https://arxiv.org/abs/1909.05027  

---

## 1 answers

### Answer by username_2 on 2023-02-28. Score: 1

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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: @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.  
> **username_3**: Sorry! I didn't think my commented warranted a whole new answer, but comments make it hard to use rich notation...  
> **username_2**: @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.  

---

