Timeline for Practical example in using (homotopy) type theory
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 19, 2019 at 13:46 | vote | accept | Andrea Ferretti | ||
| Jul 18, 2019 at 20:43 | history | became hot network question | |||
| Jul 18, 2019 at 19:57 | comment | added | Noah Snyder | Alternatively, if you don't care about working constructively, you can see Lagrange's theorem fully proved in code in a type theory with LEM in the Lean Mathlib where I think it's the lemma "card_subgroup_dvd_card". | |
| Jul 18, 2019 at 19:03 | answer | added | Mike Shulman | timeline score: 13 | |
| Jul 18, 2019 at 18:57 | comment | added | Noah Snyder | As discussed below this isn't really about group theory, it's about finite sets. There's a paper on finite sets in HoTT that you might like. cs.ru.nl/~nweide/FiniteSetsInHoTT.pdf | |
| Jul 18, 2019 at 16:29 | answer | added | Neil Strickland | timeline score: 4 | |
| Jul 18, 2019 at 15:40 | answer | added | Valery Isaev | timeline score: 6 | |
| Jul 18, 2019 at 15:00 | answer | added | Noah Snyder | timeline score: 6 | |
| Jul 18, 2019 at 12:34 | history | asked | Andrea Ferretti | CC BY-SA 4.0 |