Zulip Chat Archive

Stream: Type theory

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


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?

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

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: Dec 20 2023 at 11:08 UTC