3.1 Requirements to the semantics

1. semantics of functional types
2. subtyping for functional types

1. the carrier set A_{s1...sn -> s}/A_s1...sn+s of any total/partial functional type is (isomorphic to) a (sub)set of the total/partial functions from A_s1 ×... ×A_sn to A_s
2. the subsort relation < between basic sorts is extended to the subtype relation < ^=> (defined below) between types,
3. the embeddings function from A_s to A_s' for any s < ^=> s' is only required to be injective if s < ^-> s', where < ^-> is a subrelation of < ^=> , defined below
4. there is only a projection function from A_s' to A_s for s < ^-> s' (as non-injective embeddings can not have an inverse projection function)