## Stream: new members

### Topic: Countable product type

#### Iocta (Aug 24 2020 at 22:54):

What's the notation for a product of types likevariables (α β : Type u) (p: α × β) but with countable elements instead of two elements?

#### Adam Topaz (Aug 24 2020 at 23:02):

It's dependent functions from nat

#### Adam Topaz (Aug 24 2020 at 23:04):

I.e. given T : nat -> Type*, you could do this \Pi (n : nat), T n.

#### Adam Topaz (Aug 24 2020 at 23:04):

T is the analogue of your choice of alpha and beta, and the Pi type is the analogue of the product

Last updated: May 16 2021 at 21:11 UTC