A subsorted signature Sigma=(S,TF,PF,P, < S) consists of a many-sorted signature (S,TF,PF,P) together with a pre-order < S of subsort embeddings on the set S of sorts. < S is extended to sequences of sorts. We may drop the subscript S when obvious from the context.
For a subsorted signature, we can define overloading relations for function and predicate symbols. Let f1:w1 -> s1 < F f2:w2 -> s2 hold if w1 < w2, s1 and s2 have a common supersort, and f1=f2; similarly for predicate symbols, let p1:w1 < P p2:w2 hold if w1 < w2 and p1=p2.
A subsorted signature morphism sigma: Sigma -> Sigma' is a many-sorted signature morphism that preserves the pre-order < S and the overloading relations < F and < P.
With each subsorted signature Sigma=(S,TF,PF,P, < S) a many-sorted signature Sigma# is associated, extending (S,TF,PF,P) for each pair of sorts s < S s' by a total embedding function (from s into s'), a partial projection function (from s' onto s), and a membership predicate (testing whether values in s' are embeddings of values in s). We assume that the symbols used for embeddings, projections and membership are not used otherwise in Sigma.