<p>Yes, equality reflection and <span class="math-container">$\eta$</span>-rule for functions together imply function extensionality.</p>

<p>Recall that equality reflection is the rule
<span class="math-container">$$\frac{\vdash p : \mathsf{Id}_A(a,b)}{\vdash a \equiv b : A}$$</span>
Suppose <span class="math-container">$A$</span> is a type, <span class="math-container">$x : A \vdash B(x)$</span> is a type over <span class="math-container">$A$</span>, and <span class="math-container">$f, g : \prod_{x : A} B(x)$</span>. We claim that function extensionality
<span class="math-container">$$\textstyle (\prod_{x:A} \mathsf{Id}(f x, g x)) \to \mathsf{Id}(f, g)$$</span>
is inhabited by <span class="math-container">$\lambda r \,.\, \mathsf{refl} f$</span>. Indeed, suppose <span class="math-container">$r : \prod_{x:A} \mathsf{Id}(f x, g x)$</span>. We have <span class="math-container">$$y : A \vdash r y : \mathsf{Id}(f y, g y),$$</span> therefore by equality reflection <span class="math-container">$$y : A \vdash f y \equiv g y : B(y).$$</span> Now it follows that <span class="math-container">$$(\lambda y : A . f y) \equiv (\lambda y . g y) : \textstyle\prod_{x : A} B(x)$$</span>
By <span class="math-container">$\eta$</span>-rule for functions (it does not matter whether this is propostional or judgemental <span class="math-container">$\eta$</span>, thanks to equality reflection) we get
<span class="math-container">$$f \equiv (\lambda y . f y) \equiv (\lambda y . g y) \equiv g : \textstyle\prod_{x : A} B(x)$$</span>
Because <span class="math-container">$f$</span> and <span class="math-container">$g$</span> are judgmentally equal, <span class="math-container">$\mathsf{refl}\,f$</span> indeed has the type <span class="math-container">$\mathsf{Id}(f,g)$</span>.</p>

CC BY-SA 4.0
2020-02-12T21:40:39.130Z
2020-02-12T21:40:39.130Z
Andrej Bauer
<p>Is the principle of function extensionality
<span class="math-container">$ (\forall x. f(x) = g(x)) \implies f = g$</span>, derivable from ETT?
Most notably is this derivable in Agda with axiom K?</p>

CC BY-SA 4.0
2020-02-12T14:29:57.527Z
Agda with axiom K is most definitely *not* ETT.
cody
CC BY-SA 4.0
2020-02-12T15:28:40.903Z
It is derivable in ETT, but not because of the uniqueness of identity proofs (which is equivalent to K), but because of equality reflection. In fact, function extensionality is still independent of MLTT + K.
daniel gratzer
CC BY-SA 4.0
2020-02-12T15:31:32.633Z
Is the question asking whether equality reflection implies function extensionality?
Andrej Bauer
<type-theory><automated-theorem-proving><agda>
Extensional type theory and function extensionality
Ilk
# Extensional type theory and function extensionality

(Asked by: username_0 on 2020-02-12)

Is the principle of function extensionality
$ (\forall x. f(x) = g(x)) \implies f = g$, derivable from ETT?
Most notably is this derivable in Agda with axiom K?

**Tags:** type-theory, automated-theorem-proving, agda
> **Comments:**
> **username_1**: Agda with axiom K is most definitely *not* ETT.  
> **username_2**: It is derivable in ETT, but not because of the uniqueness of identity proofs (which is equivalent to K), but because of equality reflection. In fact, function extensionality is still independent of MLTT + K.  
> **username_3**: Is the question asking whether equality reflection implies function extensionality?  

---

## 1 answers

### Answer by username_3 on 2020-02-12. Score: 6 | Accepted answer

Yes, equality reflection and $\eta$-rule for functions together imply function extensionality.

Recall that equality reflection is the rule
$$\frac{\vdash p : \mathsf{Id}\_A(a,b)}{\vdash a \equiv b : A}$$
Suppose $A$ is a type, $x : A \vdash B(x)$ is a type over $A$, and $f, g : \prod\_{x : A} B(x)$. We claim that function extensionality
$$\textstyle (\prod\_{x:A} \mathsf{Id}(f x, g x)) \to \mathsf{Id}(f, g)$$
is inhabited by $\lambda r \,.\, \mathsf{refl} f$. Indeed, suppose $r : \prod\_{x:A} \mathsf{Id}(f x, g x)$. We have $$y : A \vdash r y : \mathsf{Id}(f y, g y),$$ therefore by equality reflection $$y : A \vdash f y \equiv g y : B(y).$$ Now it follows that $$(\lambda y : A . f y) \equiv (\lambda y . g y) : \textstyle\prod\_{x : A} B(x)$$
By $\eta$-rule for functions (it does not matter whether this is propostional or judgemental $\eta$, thanks to equality reflection) we get
$$f \equiv (\lambda y . f y) \equiv (\lambda y . g y) \equiv g : \textstyle\prod\_{x : A} B(x)$$
Because $f$ and $g$ are judgmentally equal, $\mathsf{refl}\,f$ indeed has the type $\mathsf{Id}(f,g)$.


---

