According to the Wikipedia article on the set theory New Foundations, the variant of New Foundations but with the comprehension axiom limited to theories that can be stratified using only three types (henceforth $\mathrm{NF3}$) lacks a convenient ordered pair, or is not known to have one.
I tried writing down the Kuratowski pair to see why it wouldn't go through, but I don't see where the construction breaks. Why does the Kuratowski pair not work as a definition of an ordered pair in $\mathrm{NF3}$? What mistake am I making in my argument?
I strongly suspect I am misusing parameters or misunderstanding something fundamental about how stratification and parameters interact in NF-like set theories.
$\mathrm{NF3}$ has two axioms.
It has the axiom of extensionality.
$$ (\forall x \mathop. x \in a \leftrightarrow x \in b) \leftrightarrow a = b $$
It also has a version of the comprehension axiom. In the formula below, the variable $a$ must occur in $\varphi$ with exactly one type and $\varphi$ must be stratifiable as a whole using only 3 types. As with $\mathrm{NF}$, parameters are not required to take on a consistent type in $\varphi$.
$$ \exists x \mathop. a \in x \leftrightarrow \varphi(\cdots, a) $$
Here is a construction of the unordered pair using set-builder notation with explicit type superscripts.
$ \{X, Y\} $ is equivalent to $ \{ z^1 : z^1 = X^1 \lor z^1 = Y^1 \} $. The variable $z$ and each of the parameters occur with one type ascription apiece. I think this demonstrates the existence of the unordered pair once I have two sets that I want to pair together.
For the ordered pair $(X, Y)$, I pick the Kuratowski pair $\{\{X\}, \{X, Y\}\}$. I construct it as follows.
$$ \{ z^3 : \\ ((\exists! a^2 \mathop. a^2 \in z^3) \land X^2 \in z^3 ) \;\text{or} \\ ( X^2 \neq Y^2 \land (\exists! a^2 \mathop. a^2 \in z^3 \land (a^2 \neq X^2)) \land X^2 \in z^3 \land Y^2 \in z^3) \} $$
$z$ consistently has type $3$ and the two parameters consistently appear with type $2$.
I think I can create a set of all pairs without too much trouble. Basically, I inspect every candidate pair $p^3$ and check that there exist $x$ and $y$ such that $p$ contains $\{x\}$, $p$ contains $\{x, y\}$ and $p$ is a singleton when $x=y$ and $p$ is a doubleton when $x \neq y$. This is especially confusing since the set of all pairs doesn't use any parameters at all.
$$ \{ p^3 : \exists x^1 \exists y^1 \mathop. \\ (\exists! a^2 \mathop. (\exists! b^1 \mathop. b^1 \in a^2) \land (x^1 \in a^2 \land a^2 \in p^3)) \;\text{and}\\ (x^1 \neq y^1 \to (\exists! a^2 \mathop. (\exists! b^1 \mathop. b^1 \neq x^1 \land b^1 \in a^2 ) \land a^2 \in p^3 \land x^1 \in a^2 \land y^1 \in a^2)) \;\text{and}\\ (x^1 = y^1 \to (\exists! a^2 \mathop. a^2 \in p^3)) \;\text{and}\\ (x^1 \neq y^1 \to (\exists w^2 \mathop. w^2 \in p^3 \land (\exists! u^2 \mathop. u^2 \neq w^2 \land u^2 \in p^3))) \\ \} $$
I'm not entirely sure what the author of the Wikipedia article had in mind, but I suspect it is a reference not to an inability to construct Kuratowski pairs, but that they're not very good pairs, and we cannot implement the superior Quine-Russell type-level ordered pair in $NF_3$.
The Kuratowski ordered pair can, as you've correctly observed, be defined using only three types, but it is an unsatisfactory pair in any form of NF for the reason that the projection and pairing functions have unstratified definitions. The result is that the category of sets, where the functions are implemented with Kuratowski pairs, is not finitely complete; which is pretty unfortunate for a set theory.
The Quine-Russell ordered pair is the preferred pair for working in $\mathit{NF}$ (though not for $\mathit{NFU}$) since it has none of these flaws; it but the construction depends on the existence of sets that cannot be defined using only three types.