Timeline for How big can function spaces get without extensionality?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 16 at 14:36 | history | edited | Z. A. K. | CC BY-SA 4.0 |
added 107 characters in body
|
| Jul 15 at 11:11 | answer | added | Peter LeFanu Lumsdaine | timeline score: 5 | |
| Jul 15 at 5:12 | answer | added | Dan Doel | timeline score: 7 | |
| Jul 14 at 2:17 | history | edited | Z. A. K. | CC BY-SA 4.0 |
uniformize terminology
|
| Jul 13 at 20:55 | comment | added | Peter LeFanu Lumsdaine | Richard Garner’s 2008 paper On the strength of dependent products in the type theory of Martin-Löf (arXiv:0803.4466) is very relevant — it looks at various ways to blow up dependent products in the absence of extensionality. I don’t immediately see if its techniques can give your specific statement $\mathrm{big}_C$, and don’t have much time to play around with it right now, but it might well be do-able. | |
| Jul 13 at 17:47 | history | edited | Z. A. K. | CC BY-SA 4.0 |
add explicit definition of injectivity
|
| Jul 13 at 17:42 | history | edited | Z. A. K. | CC BY-SA 4.0 |
added 2 characters in body
|
| Jul 13 at 16:54 | history | edited | Z. A. K. | CC BY-SA 4.0 |
replaced $\bot$ with $\mathbf{0}$ for consistency
|
| Jul 13 at 16:48 | history | asked | Z. A. K. | CC BY-SA 4.0 |