Infinite product of types

Stream: Type theory

[Will Bradley]

Is this the right notion for an infinite product of types, corresponding to an infinite product of sets $\beta_i, i \in I$ over some index set $I$?

def infiniteProduct (I: Type u) (βs: I → Type v) :=
  (i: I) → βs i

I want to double-check my reasoning before I put it in my project.

[Matt Diamond]

I think Latex works if you use two dollar signs instead of one... $\beta_i$ (I typed $$\beta_i$$)

[Will Bradley]

Thank you!

Matt Diamond said:

I think Latex works if you use two dollar signs instead of one... $\beta_i$ (I typed $$\beta_i$$)

[Mario Carneiro]

yes, this is called a dependent product or Pi type

[Will Bradley]

Mario Carneiro said:

yes, this is called a dependent product or Pi type

I am familiar with Pi types. It's neat they correspond to infinite set products though

[Mario Carneiro]

what else would they be?

[Mario Carneiro]

it's the set of functions where the codomain depends on the value, that's exactly what an indexed product type is in set theory