## Stream: new members

### Topic: Sigma Types - Dependent Sum or Dependent Product?

#### Rajiv (Dec 10 2020 at 11:35):

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.

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

I was wondering which one is correct?

#### Reid Barton (Dec 10 2020 at 11:41):

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

#### Reid Barton (Dec 10 2020 at 11:43):

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

#### Rajiv (Dec 10 2020 at 11:49):

Thanks Reid.

Last updated: May 12 2021 at 05:19 UTC