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