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 embedding on the set S of sorts. < S is extended pointwise 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). The symbols used for embedding, projection, and membership are chosen arbitrarily so as not to be used otherwise in Sigma.
Any subsorted signature morphism sigma: Sigma1 -> Sigma2 expands to a many-sorted signature morphism sigma#: Sigma1# -> Sigma2#, preserving the symbols used for embedding, projection, and membership.