Zulip Chat Archive

Stream: Type theory

Topic: Do identity types reduce to non-indexed W-types?


view this post on Zulip Roman Bars (Mar 14 2021 at 09:44):

In intensional type theory identity types are indexed W-types (from what I understand). I saw some references discussing the reduction of indexed W-types to ordinary W-types for extensional type theory or at least intensional type theory assuming function extensionality. But what if we don't assume that?

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:17):

I don't think you need function extensionality, but you do need eta for product types which lean doesn't have

view this post on Zulip Mario Carneiro (Mar 14 2021 at 12:19):

Even then, the reduction of indexed W-types to ordinary W-types uses eq as a primitive. Without eq, you can't ever make an indexed inductive


Last updated: May 08 2021 at 21:09 UTC