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 (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?

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?