Normally, for a cartesian product between sets $A$ and $B$, we have the notation
$$A\times B$$
But what if the set $B$ depends on the first element of the cartesian product?
i.e., for each $a\in A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $b\in B_a$.
Is there a concise notation for this?
Best Answer
Since you are talking about dependent types, I suggest $(a:A) \to B_a$ or $(a \in A) \to B_a,$ where the former is more "typish" and the latter more mathematical.
If you think "that's a function, not a pair", remember that in mathematics, a function $f : X \to Y$ is defined as a subset of $X \times Y$ such that for all $x \in X$ there exists a unique $y \in Y$ such that $(x,y) \in f.$
But if you want it to look more like a Cartesian product, you could write it as $(a \in A) \times B_a.$
These notations are not standard in mathematics, so make sure to define them in whatever you write.