Suppose we want to rigorously build up all of mathematics within some standard set theory, e.g. NBG or ZFC. Then, given some notion of ordered pair $\langle a,b\rangle$ of sets $a$ and $b$ (e.g. Kuratowski), what would be good definitions for the concepts map and tuple?
Option 1: Given a set $I$, define an $I$-tuple to be any set of the form $$\{\langle i,a_i\rangle\,;\, i \in I\}$$ and let map with domain $I$ mean just the same thing as $I$-tuple.
Option 2: Define $I$-tuple as above and define a map with domain $I$ to be any set of the form $$\{(i,a_i)\,;\, i \in I\}$$ where $( a, b)$ denotes the $2$-tuple of sets $a$ and $b$ (i.e. $(a,b) := \{\langle 0,a \rangle, \langle 1, b \rangle \}$ given the von Neumann definition of $2$ as $\{0,1\}$).
Option 2 has the advantage that maps are special binary relations, which are subsets of $2$-products, which in turn are special cases of $I$-products over arbitrary index sets $I$. In option 1, one would have to choose between letting binary relations either be a generalization of maps (i.e. a set of ordered pairs) or a special case of $n$-ary relations (i.e. a set of $2$-tuples). The nice thing about maps as special binary relations is that concepts like „composite“, „image“, „domain“, „fibre“, „surjective“, „inverse“ etc. make sense and are useful applied to binary relations. Another advantage of option 2 (which is connected to this) is that in the context of option 1 both the products $$A \times B := \{\langle a,b\rangle; a\in A, b\in B\}\quad\text{}$$ and $$A \sqcap B := \{(a,b); a\in A,b\in B\} $$ would be of interest, so one would have to develop the corresponding concepts (projection maps etc.) twice.
Option 1 has the advantage that tuples can be treated like maps (since they are maps), so all the concepts developed for maps can be applied to both. As an example, given a tuple $(a_0,\dots,a_n)$ over some set $A$ and a map $f : A \to B$, we can just write $f \circ (a_0,\dots,a_n)$ for $(f(a_0),\dots,f(a_n))$ (this is particularly useful if the tuple is not explicitly given but just as $\tau \in A^{n+1}$).
Both options have in common that finite tuples are defined as „functions“ of natural numbers. My main reason for not considering the usual definition as recursively nested ordered pairs is that the length of a thus defined tuple is not always uniquely determined and it would not make sense in general to speak of the $k$th component of a finite tuple. Another reason is that finite tuples would not be tuples in the general sense and we would accordingly have to distinguish between finite and arbitrary products. (See also this post).
Are there any further relevant advantages/disadvantages for each of these two options or can anyone think of a third possibility which shares (only) the good aspects with both options?
An ideal situation: The following might clarify what I am looking for, even though I am quite convinced that it cannot be realised:
- there is one general concept of $I$-product over an index set $I$; finite products are $n$-products where $n$ is a (von Neumann) natural number.
- $n$-ary relations are subsets of $n$-products.
- maps are special binary (i.e. $2$-ary) relations.
- tuples (i.e. elements of products) are maps and vice versa (i.e. the two words are synonyms).
- ordered pairs are $2$-tuples. (Not so important).