Models

For a subsorted signature Sigma the  subsorted models are ordinary many-sorted models for Sigma^# that satisfy the following properties (which can be formalized as a set of conditional axioms):

• Embeddings are 1-1 functions.
• The embedding of a sort into itself is the identity function.
• All compositions of embeddings between the same two sorts are equal functions.
• Projections are the partial inverses of embeddings.
• Membership in a subsort holds just when the projection to the subsort is defined.
• Embeddings commute with those functions and predicates that are in the overloading relations.