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 is a basic rule of definitional equality for functions, called the eta rule. It's built into the type checker. Implementations of type theory commonly support it.