notation for cartesian product with dependent types?

Question

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?

Answer 1

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.

Answer 2

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\}$$

Answer 3

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.$$