Abstract signatures for substitution systems

A new semantical/categorical notion of signature is introduced that is intended to capture all kinds of syntax with variable binding in the style of inductive families, which could also be called locally nameless or typeful deBruijn representation. In particular, the new notion encompasses the notion of signature introduced by the author and Uustalu that has a strength-like datum and is used to study heterogeneous substitution systems. The latter are based on the presentation of monads with monad multiplication that is notoriously difficult to generalize to the setting of relative monads. Abstract signatures allow definitions relative to a given functor, so that variable names of terms can also be taken from a restricted set, such as the natural numbers. The module concept of Hirschowitz and Maggesi (however, rather the relativization by Ahrens) is adapted through "proto-modules" that come with less data than modules, which is crucial in the construction process. This is work in progress.