The lambda calculus, subject to typing restrictions, provides a syntax for
the internal language of cartesian closed categories. This paper establishes a
parallel result: staging annotations, subject to named level restrictions,
provide a syntax for the internal language of (the codomain of) a functor which
preserves a premonoidal enrichment. Such functors are uniquely determined by
functors from an {\it enriching} category to an {\it enriched} category. An
equational axiomatization for the latter form is given, and Arrows are shown to
constitute a special case.

This result is most useful when the enrichment is that of a category of types
and terms in a category of judgments. In such a scenario, the proof of
correspondence yields a translation from well typed multi-level terms to well
typed one-level terms which are parameterized over an instance of a {\it
generalized arrow} (GArrow). The translation is defined by induction on the
structure of the proof that the multi-level program is well typed, relying on
information encoded in the proof's use of structural rules (weakening,
contraction, exchange, and context associativity). When supplied with an
appropriate GArrow instance, the translation preserves big-step semantics.

From a practical perspective, this permits metalanguage designers to factor
out the syntactic machinery of metaprogramming by providing a single
translation from multi-level syntax into expressions of GArrow type. Object
language {\it providers} need only implement the functions of the GArrow type
class in point-free style. Object language {\it users} may write metaprograms
over these object languages in a pointful style, sharing the same binding,
scoping, abstraction, and application mechanisms across both the object
language and metalanguage.