Are there known type-level infinite tuple implementations in ZFC?

Question

Quine-Rosser ordered pair is type-level; i.e., it is definable by a stratified formula that assigns to it the same type it assigns to its projections.

It is known that if $\langle A,B \rangle$ is type-level, then we can define a triplet $ \langle A,B,C \rangle$ using this type-level merit as $\langle \langle A,B \rangle, C \rangle$, and we can go up recursively to define any n-tuple.

However, this extend-ability seems to fail to define infinite type-level tuples, since functions of Quine-Rosser pairs are one type higher than the pairs in them.

Now a definition of a type-level ordered pair that I've presented to MathStackExchange (see here for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

Define: $\iota^2"X = \{ \{\{x\}\}: x \in X\}$

So take any sequence $S: \iota^2"\alpha \to X$, then there exists an $\iota ^2 \alpha$ long tuple $t(S)$ such that:

$$t (S)= \{x \cup \{[\bigcup^2(rng(S))]^*+ i\} | x \in S(\{\{i\}\})\}$$

Where $S(\{\{i\}\})$ is the image of $\{\{i\}\}$ under $S$; and $X^*$ is the smallest ordinal strictly ordinally greater than all elements of $X$

Now clearly $t(S)$ is of the same type of elements of the range of $S$, i.e. $t(S)$ has the same type of each $S(\{\{i\}\})$ where $i \in \alpha$. Now we DEFINE the $i^{th}$ projection of $t(S)$ as $S(\{\{i\}\})$; and this way we get a type-level tuple (i.e. of the same type of its projections) of infinite length!

To retrieve the $i^{th}$ projection of any such tuple $t(S)$ we define $max^{\alpha}(\bigcup t(S))$ as: $$\{max(d) [ordinal(d) \land d \in x]: x \in \bigcup(t(S))\}$$

Now we retrieve the $i^{th}$ projection of $t(S)$ by taking the set of all elements of $\bigcup(t(S))$ that has the $i^{th}$ ordinal in $max^\alpha(\bigcup(t(S))$ in them, and the $i^{th}$ projection of $t(S)$ would be the image of that set under function $f(X)=X\setminus \{max(d)[ordinal(d) \land d \in X]\}$

My question: Are there comparable examples of type-level infinite tuples in ZFC and its extensions.

Answer 1

I'll post this as an answer because it can be thought of being closely related to known work on pairs, although I'm not sure really if it has been worked out before.

I realized that Quine-Rosser pairs can be adapted to suite extending them to implement tuples of any ordinal length! The tuples I'll describe here would be what could be thought of as being the simplest genuine extension of the Quine-Rosser pairs.

Statement: for any ordinal $\alpha$, there is a tuple of length $T^2 \alpha$, and there will be no limitation (unlike the tuple in the question) on which set can be a projection of it.

Let $D$ be the set of all Ordinals.

Define functions $F_i$ for $i \in D\setminus \{0\}$ as:

$F_i(X)= [X \setminus D] \cup \{d \#(i \# 1)| d \in D \cap X \} \cup \{i\} $

, where $``\#"$ is "Hessenberg natural sum"

Now the tuple $t^{\alpha}(S)$ whose projections are entries $s_{\{\{i\}\}}$ of the sequence $S$ from $\iota^2"\alpha \to V$ is defined as:

$ t^{\alpha}(S) = \{F_i(x)| x \in s_{\{\{i\}\}} \in rng(S) \land \{\{i\}\} \in \iota^2" \alpha \}$

Now to retrieve back the $i^{th}$ projection from the pair, the smallest ordinal member of the elements of the pair would serve as the indicator of the projection, so take the set of all elements of the tuple having ordinal $i$ as the smallest ordinal in them, and taking the converse function $F^{-1}$ over those would yield the $i^{th}$ projection of the tuple. So simply:

$i^{th} (p) = \{ x | F_i(x) \in p \}$

This tuple works in the most general manner that a tuple can work in NF\NFU, as well as in NBG, MK set theories. However, in ZF and its extensions, it is equivalent to the tuple mentioned in the question.

Notation: $\iota^2" X = \{\{\{x\}\} : x \in X \}$ ; $T^2|X| = |\iota^2" X |$

Another very closely related pair [due to Randall Holmes] along similar lines is the following:

Define $inc$ as the function sending $(x,n)$ to $(x,n+1)$ for any $x$ and any natural number $n$, and fixing anything not in $V \times N$

Now define $A_x$ as the $\{inc``B \cup \{(x,0)\}: B \in A \}$ This "increments" all elements of elements of $A$ which are in $V \times N$ and adds $(x,0)$ as a further element of each element.

For any function $f$ with domain the set of all double singletons, define $tuple(f)$ as the union of all $(f(\{\{x\}\})_x)$

This gives a $T^2(|V|)$ tuple with projections at the same type as the tuple.

I think that the limit on how many projections there are is intrinsic.

A closely related observation of mine is that we can use similar method to have type level functions of maximally $T|V|$ many entries! For every function $f$ whose domain is a set of singletons, there is a type-level function $t(f)$ corresponding to it defined as:

$t(f)=\{(x,z)| z \in f(\{x\})\}$

Where $(,)$ is the Quine-Rosser type-level pair.