In particular, this means that derivations can output derivations. But that ramification isn't (yet!) useful as we would want, since there is no way to have a dependent derivation that is itself a dependent derivation.