Intuition for difference between eta for function from top and empty functions in Agda

The ⊤ type has the eta rule which says that any terms with that type are definitionally equal. Hence, f ≡ (λ x → f x) ≡ (λ x → f tt).

⊥ does not have an eta rule in Agda. If f : ⊥ → A, then we only know that f ≡ λ x → f x. λ () is essentially syntactic sugar for ⊥-elim, and f is not definitionally equal to ⊥-elim.

I draw your attention that the first statement is attempting to prove the uniqueness of ⊥ → A. Usually it is true up to isomorphism.

The full correspondence would have been between ∀ {A : Set} (f : ⊤ → A) → f ≡ λ _ → f tt and ∀ {A : Set} (f : ⊥ → A) → f ≡ λ _ → f () - the expression for ⊤ constructs the value tt, so you should be constructing a value for ⊥.

Agda has no means of constructing a value of ⊥, so () is not a valid constructor, it is only a placeholder for what you want.

Although it isn't really pattern-matching, it probably is not harmful to see the use of () as pattern-matching for the empty type - it is allowed to occur only in the pattern-matching positions.

This is intended to show the similarity is superficial, so should amend your intuition about the expressions.

Shouldn't f ≡ λ () be some form of eta law?

It is not clear what you would gain from that. Many things can be proven only up to isomorphism. So, for example, proving the uniqueness of ⊥ → A could correspond to proving the uniqueness of A → ⊤ (not eta-equality of f and λ _ → f tt). Both of these is doable.