Closure Converting the Universes

 Type preserving closure conversion of languages with dependent types has proved difficult.  It took until 2018 to get the first solution to the problem, and that solution relies on language constructs custom-made for the purpose.  A first part of the problem is the fact that closure conversion inevitably requires some form of impredicativity since a function can have free variables that belong to a higher universe than itself, but none of the existing forms of impredicativity (other than those known to be inconsistent) satisfy the needs of closure conversion. A second part is that closure conversion exposes internal details of functions, and those details affect the definitional equality of (converted) functions, hence breaking type preservation. 

In this paper we propose to solve the first problem with the use of a new form of impredicativity, and the second with a more restrictive notion of function equality.  This allows us to define a closure conversion that relies only on generic language constructs, yet handles a dependently typed language with a tower of universes.