Why doesn't this proof require extensionality? (Agda)

Question

The following proves the equality of two functions:

?-? : ? {A B : Set} (f : A ? B) ? (? (x : A) ? f x) ? f
?-? f = refl

Why doesn't it need extensionality? How does Agda know that the function to the left of the ? simplifies to f?

Answer 1

(? x ? f x) ? f是函数定义相等的基本规则，称为 eta 规则。它内置于类型检查器中。类型理论的实现通常支持它。