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][1] for details) can indeed be extended to define type-level $\alpha$-tuples, for any ordinal $\alpha$ whether finite or not!

So take any sequence $S: \alpha \to X$, then there exists an $\alpha$ long tuple $t$ such that:

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

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$, where each $s(i)$ is considered as the $i^{th}$ projection of $t(S)$.

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. 


  [1]: https://math.stackexchange.com/questions/3408107/reference-request-what-are-the-known-kinds-of-type-level-ordered-pairs-other-th