  We extend our approach to abstract syntax (with binding constructions)
through modules and linearity. First we give a new general definition of arity,
yielding the companion notion of signature. Then we obtain a modularity result
as requested by Ghani and Uustalu (2003): in our setting, merging two
extensions of syntax corresponds to building an amalgamated sum. Finally we
define a natural notion of equation concerning a signature and prove the
existence of an initial semantics for a so-called representable signature
equipped with a set of equations.

Logic in Computer Science