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