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

Stream: Type theory

[Roman Bars]

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]

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

[Mario Carneiro]

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