## 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: May 08 2021 at 21:09 UTC