We develop a theoretical foundation for compiling the programming language Agda to System Fω, which is a stepping stone towards a compiler from Agda to Haskell. The practical relevance for software engineering and the ...