# Extensional type theory and function extensionality

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?

• Agda with axiom K is most definitely not ETT.
– cody
Commented Feb 12, 2020 at 14:29
• 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. Commented Feb 12, 2020 at 15:28
• Is the question asking whether equality reflection implies function extensionality? Commented Feb 12, 2020 at 15:31

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