 Any of the usual ordered pair constructions works in NFU. The usual Kuratowski pair is inconvenient in NF or in NFU, because the pair is two types higher than its projections in terms of TST. This means that functions and relations are three types higher than the elements of their domains and ranges. There is a type-level pair defined by Quine (1945; type-level because it is the same type as its projections) which is definable in NF and also on \(V_{\alpha}\) for any infinite ordinal \(\alpha\); this pair can be defined and used in NF and the fact that it is definable on infinite \(V_{\alpha}\) means that it can be assumed in NFU+Infinity that there is a type-level ordered pair (the existence of such a pair also follows from Infinity and Choice together). This would make the type displacement between functions and relations and elements of their domains and ranges just one, the same as the displacement between the types of sets and their elements. We will assume that ordered pairs are of the same type as their projections in the sequel, but we will not present the rather complicated definition of the Quine pair.