Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in terms of all typed relations. In an impredicative system (like CiC/Coq) that's fine, but it seems to be impossible in a predicative system (like Agda).
How can this be done? For example, how would you prove normalization for System F in Agda? Do you have to build your own impredicative universe?
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.
