Introducing function types to our system

So far we can call what we did a picture-math, because whatever we can get we can also lay out as a diagram. Thus, we obtain the picture of data. We cannot do it with functions, however. There are simply too many functions to name (this is a canonical matter - e.g. NN). The other problem with functions is that, trying to write a type

we get into trouble, because is not monotone. So far, there is no successful theory for primitive recursive nonmonotonic type-forming functions. We may hope that some theory will emerge and cope with those "types" as well. Thus, we will allow function type "" in provided F is monotone set-based mapping. In such settings, rules for formation, membership and induction remain unchanged.