TPIL confusion about dependent product

Stream: new members

[Martin Dvořák]

Am I the only one who finds it confusing that TPIL calls "Sigma types" in Chapter 2.8. also "dependent products"?

[Horatiu Cheval]

I personally like "dependent product" for Sigma but I still prefer to call it just Sigma. For me dependent product is intuitive because it's like a "normal" product made of pairs (a, b), just that the type of b may dependent on a. But I've seen other texts calling Pi the dependent product, so I think that's the really confusing thing :) That's why I prefer just Pi/Sigma-type

[Martin Dvořák]

Yes. Let's stick to Sigma and Pi.