Timeline for Why are dependent sums and products called sums and products?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| 4 hours ago | comment | added | Meven Lennon-Bertrand♦ | Also note that more and more people seem to be adopting the notation $(x : A) \to B$ instead of $\prod_{x : A} B$ and $(x : A) \times B$ instead of $\sum_{x : A} B$. This makes it a bit clearer what each one generalises. Although this does not solve the ambiguity of "dependent product type"… | |
| 4 hours ago | comment | added | Meven Lennon-Bertrand♦ | To repeat here an intuition from that post which I find very useful to understand the issue: we learn in kindergarten that the product of two numbers is an iterated sum. The same pattern also applies for types, and is part of what causes this confusion. | |
| 5 hours ago | history | became hot network question | |||
| 7 hours ago | comment | added | Andrej Bauer | See this answer of mine to a similar question. It explains how binary sums and products generalize in two ways. Thus $A \times B$ is both a special case of a dependent sum and a special case of a dependent product. | |
| 12 hours ago | vote | accept | Greg Nisbet | ||
| 12 hours ago | answer | added | Trebor♦ | timeline score: 6 | |
| 13 hours ago | comment | added | Trebor♦ | Your line of thought is exactly why the name "dependent product" is so confusing and ambiguous. I would prefer using Sigma/Pi types to disambiguate. | |
| 13 hours ago | history | asked | Greg Nisbet | CC BY-SA 4.0 |