I tried, but without success. The problem seems to lie in the fact that the premise of the elimination rule is $x \in A, f \in B(x) \to W, z \in (\Pi u \in B(x))\, C(f(u)) \vdash d(x,f,z) \in C(\mathsf{sup}(x,f))$ and so I can't possibly exhibit a proof-term that $z$ preserves the equivalence relation (it's a variable!), even though I know that in the computation $z$ will be replaced by a function for which I could prove extensionality in principle. But if it's not clear I can expand my post.

I guess there is no universally accepted definition of "logical framework". Basically, a logical framework is a metalanguage by means of which one can present a particular type theory through a set of axioms (i.e. typings of constants and equalities). It is usually formalized as a type theory itself, but it doesn't necessarily possess the same features of the theories that one defines in it.

You're right, I forgot to say non-zero, I'll edit that.