Logical Reations for an Impredicative System in a Predicative MetaTheory
In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent types as a ($n$-ary) relation $R \subseteq \cal A^n$.

This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. Shürmann and Sarnat: Structural Logical Relations where a predicative logic (that of Twelf) is used to prove a certain property (decidability of equality) for a predicative calculus (simply typed $\lambda$-calculus) using logical relations.

As you may have suspected, however, it is not possible to prove normalization of system F in Agda (if Agda isn't secretly stronger than expected, i.e. about the strength of Martin-Löf type theory with a bunch of universes). This is because normalization of system F implies consistency of 2nd order arithmetic ($\mathrm{PA}_2$) which is stronger than M-L type theory with any number of (predicative) universes.

It's instructive to work out exactly where the proof goes wrong in Agda, though. It indeed occurs when you try to define the logical relations interpretation of the impredicative quantification. The interpretation of the non-impredicative connectives though (including "dependent" quantification) is kosher in a theory like Agda.