do this we introduce the terminology that a function is from to if its domain equals and its range is contained in . In this way, every function is a function from its domain to its range, and a function from to is also a function from to for any set containing . Indeed, no matter which set we consider to be the codomain of a function, the function does not change as a set since by definition it is just a set of ordered pairs. That is, a function does not determine its codomain by our definition. If one finds this unappealing then one can instead define a function as the ordered pair , where is a functional relation and is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as - then one could define a function as the ordered triple so as to also include the domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let be a binary relation", but formally is a set of ordered pairs such that and . In NFU, has the same type as , and is three types higher than (one type higher, if a type-level ordered pair is used). To solve this problem, one could define as for any set , but this is more conveniently written as . Then, if is a set and is any functional relation, the Axiom of Replacement assures that is a set in ZFC. In NFU, and now have the same type, and is two types higher than (the same type, if a type-level ordered pair is used). The function such that is not a set in ZFC because it is "too large". is however a set in NFU. The function (predicate) such that is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be stratified. Moreover, can be proved not to exist in NFU (see the resolution of Cantor's paradox in New Foundations.) Operations on functions Let and be arbitrary functions. The composition of and , , is defined as the relative product , but only if this results in a function such that is also a