notation for cartesian product with dependent types? 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?
 A: Given an indexed family of sets $(B_a)_{a\in A}$, the set $\{\langle a,b\rangle\;|\;a\in A\wedge b\in B_a\}$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$\biguplus_{a\in A}B_a$$ or $$\coprod_{a\in A}B_a$$ or $$\sum_{a\in A}B_a.$$ 
A: 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.
A: This is the particular case, where $A \times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.
You can always define
$$C = \{(a,b) : a \in A, b \in B_a\}$$
