Timeline for How much duplication does universe polymorphism actually save us?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 28, 2022 at 18:02 | vote | accept | Trebor♦ | ||
| Mar 15, 2022 at 19:27 | answer | added | ice1000♦ | timeline score: 3 | |
| Mar 11, 2022 at 8:21 | comment | added | François G. Dorais | Is it meant to save time in the first place? Or is it just to ensure a broader generality/applicability of the results? | |
| Mar 10, 2022 at 4:45 | comment | added | Trebor♦ | @JasonRute That's exactly what I meant, thanks! | |
| Mar 10, 2022 at 4:44 | history | edited | Trebor♦ | CC BY-SA 4.0 |
added 58 characters in body
|
| Mar 10, 2022 at 0:31 | comment | added | Jason Rute |
Is this the Zulip conversation you had in mind (I'm using the public link)? leanprover-community.github.io/archive/stream/113488-general/… Mario's calculation at the time says in Lean's mathlib you only need up to Type 3 (or ZFC + 4 inaccessible cardinals) (which I understand is not exactly what you are asking for this question).
|
|
| Mar 10, 2022 at 0:06 | history | asked | Trebor♦ | CC BY-SA 4.0 |