Timeline for Why are W-types called "W"?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 24, 2021 at 23:55 | history | became hot network question | |||
| Aug 24, 2021 at 20:33 | comment | added | Andrej Bauer | I said that W-types are a proof-relevant manifestation of well-founded roders. | |
| Aug 24, 2021 at 18:52 | vote | accept | user347155 | ||
| Aug 24, 2021 at 18:49 | answer | added | Peter LeFanu Lumsdaine | timeline score: 17 | |
| Aug 24, 2021 at 18:07 | comment | added | user347155 | @AndrejBauer You say W-types are orders? I would say they are types. | |
| Aug 24, 2021 at 17:18 | comment | added | Andrej Bauer | W-types are associated with order theory. They are proof-relevant well-founded orders. | |
| Aug 24, 2021 at 16:32 | comment | added | Simon Henry | The set theoretic interpretation of W-types are sets of well founded tree, so I wouldn't say it has nothing to do with the notion, and it would make sense that the W is for 'wellfounded' or 'wellorder'. But I don't know of any reference that makes this explicit. | |
| Aug 24, 2021 at 15:57 | review | First posts | |||
| Aug 24, 2021 at 17:12 | |||||
| Aug 24, 2021 at 15:54 | history | asked | user347155 | CC BY-SA 4.0 |