There is a sense in which the most natural definition of the Cartesian product is as follows:
Let $X$ and $Y$ be sets, and $F:X\to Y$. The product of $F$ is the set of functions $f:X\to\bigcup Y$ such that for every $x\in X$, $f(x)\in F(x)$. In notation:
$$\prod F=\prod_{x\in X}F(x)=\left\{f:X\to\bigcup Y:(\forall x\in X)(f(x)\in F(x))\right\}$$
The Cartesian power $Y^X$ is the set of all function $f:X\to Y$. In notation:
$$Y^X=\{f:(\forall x\in X)(\exists!y\in Y)((x,y)\in f)\}$$
There is one thing about this definition that bothers me, though. Given an arbitrary set $X$, convention dictates that $X\times X\times\cdots\times X=X^n$. This is not the case by the above definition, since $X\times X\times\cdots\times X$ is a set of $n$-tuples (defined as you like), whereas $X^n$ is a set of functions from $n=\{0,1,\ldots,n-1\}$ to $X$.$^*$
Even though these are distinct sets (assuming $X\ne\emptyset$), we often treat tuples as though they were functions. For example, even if we maintain the convention that $X^n$ is a set of $n$-tuples, we might still write something like "suppose $\mathbf r\in\Bbb R^n$ and $r_i\le r_j$ for all $i\le j<n$." Here, the relationship between "$\mathbf r$" and the subscripts "$i$" and "$j$" is the relation of function to argument - we evaluate $\mathbf r$ at $i\in n$ to get a value in $\Bbb R$, the same way that we would evaluate a function at a point to get a value in its codomain. The fact that this same notation is used to indicate the values of sequences (which cannot generally be regarded as "tuples" without violating the axiom of foundation) only serves to reinforce the identification of $n$-tuples as functions. As it turns out, this is a desirable property for a number of reasons.
Here is where we run into a problem. If we accept that every tuple is a function while retaining the standard definition of function (a set of ordered pairs such that...) we violate the axiom of foundation.
Suppose that we take $X\times Y$ to be a set of functions from $2=\{0,1\}$ to $X\cup Y$ (as the "tuple=function" paradigm suggests). Pick an element $x\in X$ and an element $y\in Y$. Now, using the conventional definition of "function" the pair $u=(x,y)\in X\times Y$ is the function $\{(0,x),(1,y)\}$ (this way, have $u_0=u(0)=x,u_1=u(1)=y$, as desired.) Now choose an element of $u$ - let's say $u_0=(0,x)$ - this is the function $\{(0,0),(1,x)\}$. Now choose an element of $u_0$..., and so on ad infinitum.
My favorite AI pointed out that this problem only occurs when we assume the definition of $n$-tuple to be recursive, and suggested that I make a distinction between "pairs," which are elements of a function, and "$2$-tuples" which are functions on $2$. In this case, $X\times Y$ is a set of pairs which is distinct from the set of functions $\{\{(0,x),(1,y)\}:x\in X,y\in Y\}$.
This ensures regularity. It also ensures that $X\times X\ne X^2$, which I just spent a paragraph arguing against.
Is there some way to define everything so that so that I can have my Von Neumann and eat my Curry too?
Notes:
$^*$ For the sake of compatibility with other established definitions, I will regard a natural number $n$ as being the set of all natural numbers $k\le n$, with $0=\emptyset$ being the least natural number. This makes "$x_0$" the first element of a tuple "$x$" by default. In the event that we want "$x_1$" to be the first element instead, we must change the definition of "$n$." This can be done with little effort, but it can lead to some inconveniences down the road.
Do we not have a tag for products in general? Like, what if I wanted to ask about how categorical products relate to dependent typing? Or factoring vector spaces to construct isomorphisms? Or constructing ultrapowers for arbitrary families of structures?