Are there known general tuple implementations that are 2 types high and withstand absence of extensionality and infinity?

Question

Is there a general $\alpha$-tuple implementation that is of height $2$, that both doesn't require infinity of the naturals, and is at the same time stable under lack of Extensionality?

My own try to solve this question depends on a modified Holmes ordered pairs.

Define: $\langle x,y,z,..,s \rangle = \{ (x,1), (y,2),(z,3),..,(s,n) \}$

Where $1,2,3,..,n$ are the usual von Neumann naturals; and where $(,)$ is defined after Holmes (see page 221), but with slight modification, as: $$(x,y)= \{\{x',0,1\},\{x',2,3\} ,\{y',4,5\} ,\{y',6,7\}\mid \\x' \in x,y' \in y \} \cup \{x \mid \not \exists k \ (k\in x) \} \\ \cup \{y \mid \not \exists k \ (k\in y) \}$$

This tuple can work even if Extensionality fails, can be of any ordinal length and it doesn't beg having infinitely many naturals (as Quine-Rosser pairs demand), and it is just $2$-type higher than its projections, which I think it's the minimal height a tuple can have if it's to meet these criteria. However, it does have a pretty much complex definition.

Are there simpler general $\alpha$-tuple implementations that can meet the above mentioned three criteria?

Answer 1

This is a partial answer to this question:

I was always under the impression that a type-level pair must depend on having some kind of well ordered infinite class of objects, well at least this was the experience I found with the Quine-Rosser pair, and in addition it should presuppose Extensionality (like Quine-Rosser pairs, or even Holmes's $1$-high type pairs). However, it's only today when I came to realize that this is not necessarily correct.

I think I can cook up a pair that fulfills the aforementioned criteria.

Lets work in $\sf ZFA \neg C$.

Now, let $F$ be a total injective function that sends sets to nonempty sets of nonempty sets not having sets $1,2$ among their elements. That is: $$ F(x)=y \to \\ \exists z\, (z \in y) \land \forall z (z \in y \to \exists u \, (u \in z) \land 1 \not \in z \land 2 \not \in z)$$ Now, we define an "inserter" function $I_\alpha$ that inserts $\alpha$ to all elements of a set, that is:

$$I_\alpha(x)=\{y \cup \{\alpha\} \mid y \in x \}$$

Now, we define the following pair:

$$(x,y) = I_1 (F(x)) \cup I_2 (F(y))$$

We can easily retrieve the $\alpha^{th}$ projection of $(x,y)$: We take the set of all elements of $(x,y)$ that have $\alpha$ among their elements, apply the de-inserter function $I_\alpha^{-1}$ on it, then apply $F^{-1}$ and we get the $\alpha^{th}$ projection of $(x,y)$.

We can extend that to any $\lambda$-tuple: $$(x_1,x_2,...)^\lambda = \underset {\alpha < \lambda} \bigcup I_\alpha(F(x_\alpha))$$

Of course, to answer the above question, we can simply take the tuple to be: $$\{\{(x_1,x_2,...)^\lambda\}\}$$ The main drawback is that this definition is not that general, for instance it doesn't work in the usual known models of $\sf NFU$, where we have strictly more empty objects than nonempty. In such models I only know of pairs with height of at least $2$ that can do the job.