Timeline for Assuming decidable equality but not LEM in HoTT
Current License: CC BY-SA 4.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 12, 2021 at 17:42 | comment | added | Peter LeFanu Lumsdaine | @MikeShulman: and indeed the D–G–M proof can usefully be factored as “If all subsets of A satisfy choice, then A has decidable equality” (which doesn’t need general quotients/suspension, just propositional truncation) and “if all sets have decidable equality, then LEM holds” (using set quotients/suspension as you say). | |
| May 12, 2021 at 15:51 | comment | added | Mike Shulman | Note that $\Sigma A$ is the same set that appears in the Diaconescu-Goodman-Myhill proof that the axiom of choice implies excluded middle. | |
| May 12, 2021 at 15:46 | history | answered | aws | CC BY-SA 4.0 |