Zulip Chat Archive

Stream: new members

Topic: Countable product type


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

view this post on Zulip Adam Topaz (Aug 24 2020 at 23:02):

It's dependent functions from nat

view this post on Zulip Adam Topaz (Aug 24 2020 at 23:04):

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

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