# 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?

• I am not sure I am following, from where $b$ in the $(a,b)$? – ℋolo Jul 26 '18 at 13:51
• I think this is what is usually called a "multivalued function" or "set-valued function". – Kusma Jul 26 '18 at 14:03
• @Kusma multivalued function is defined using the 2-tuple $(a,\{b\in B\mid aRb\})$ for some well defined $R$ over $A\times B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think) – ℋolo Jul 26 '18 at 14:08
• This is exactly the disjoint union of the $B_a$. – Malice Vidrine Jul 26 '18 at 15:56

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.

• "These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation. – user56834 Jul 27 '18 at 6:12
• In Agda dependent types are written as $(a : A) \to B\ a$. The notations in the post are made up by me based on the one in Agda. – md2perpe Jul 27 '18 at 6:25
• If we're talking about type theory, the notation $\sum_{a:A}B_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about. – Malice Vidrine Jul 27 '18 at 17:01

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

• But $B_a$ is not well defined – ℋolo Jul 26 '18 at 14:40
• This is indeed what I mean. Is there not a more compact , concise way of writing this? – user56834 Jul 26 '18 at 15:44

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

• Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with. – Malice Vidrine Jul 26 '18 at 16:57
• What I've probably seen most frequently is $\bigsqcup_{a\in A} B_a$. – Daniel Schepler Oct 4 '18 at 19:06
• Just in case you're wondering what's going on, take a look at this non-math post for some evidence. – user21820 Dec 3 '18 at 4:16