
> 
> 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](https://randall-holmes.github.io/head.pdf)), 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?
> 
> 
> 



Are there known general tuple implementations that are 2 types high and withstand absence of extensionality and infinity?
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.


