Sigma Types - Dependent Sum or Dependent Product?

Stream: new members

[Rajiv]

In section 2.8, of Theorem proving in Lean, https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types following is mentioned.

In the coming chapters, you will come across many instances of dependent types. Here we will mention just one more important and illustrative example, the Sigma types, Σ x : α, β x, sometimes also known as dependent products. These are, in a sense, companions to the Pi types. The type Σ x : α, β x denotes the type of pairs sigma.mk a b where a : α and b : β a.

As I was trying to develop my intuition for Sigma Types, I came across the following two links.

https://ncatlab.org/nlab/show/dependent+sum+type
https://ncatlab.org/nlab/show/dependent+product+type

Here, it seems like Sigma types are classified to be under dependent sum type.

I was wondering which one is correct?

[Reid Barton]

Products are also sums, e.g., 4 * 3 = 3 + 3 + 3 + 3. So both terms are in use.

[Reid Barton]

Sigma types are what the nlab calls dependent sums and Pi types are what the nlab calls dependent products.

[Rajiv]

Thanks Reid.