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?

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

1 Answer 1


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.