Countable product type

Stream: new members

[Iocta]

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

[Adam Topaz]

It's dependent functions from nat

[Adam Topaz]

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

[Adam Topaz]

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