Zulip Chat Archive

Stream: new members

Topic: Sigma Types - Dependent Sum or Dependent Product?


view this post on Zulip 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.

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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rajiv (Dec 10 2020 at 11:49):

Thanks Reid.


Last updated: May 12 2021 at 05:19 UTC