Using conventional set theory as a foundation, there are two most popular definitions of an $n$-tuple of elements of $X$:
A function $n\to X$.
For any $x_1,...,x_n \in X$, $(x_1,...,x_n, x_{n+1}) = ((x_1,...,x_n),x_{n+1}).$
I'm interested in how we can formalize the second one. Most say that it is a definition by induction. However, the formal way to deal with such matters is recursion.
Recursion theorem. Given a set $A$, an element $a$ of $A$ and a function $g\colon A\to A$, there is a unique function $f\colon\mathbb{N}\to A$ such that
$f(0) = a$,
$\forall n \in \mathbb{N}, f(n+1) = g(f(n))$.
I'm trying to understand how can we use recursion to formalize the second definition of an $n$-tuple.
I can see that we would like a function $f$ with $\mathrm{dom}(f) = \mathbb{N}$ so that
$f(0) = \{\varnothing\}$,
$f(1) = X$,
$f(2) = X \times X$ and
$\forall n \in \mathbb{N}_{\geq 2}$, $f(n+1) = f(n) \times X$.
However, I don't see what the codomain of such function can be. It probably can be done with transfinite recursion, but do we really need to use it for something so basic such as this?
You could use the set $A=\{X^n\mid n\in\mathbb N\}$ as codomain, where $X^n$ denotes the set of functions $\{1,\dots,n\}\to X$ and $g:A\to A$ is prescribed by $X^n\mapsto X^{n+1}$ and $f(0)=X^0$.