Lecture 3-3: Constructive Logic

mvrnote: under construction

mvrnote: global choice implies excluded middle https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#global-choice

https://mathoverflow.net/questions/391996/assuming-decidable-equality-but-not-lem-in-hott Note that Σ𝐴 is the same set that appears in the Diaconescu-Goodman-Myhill proof that the axiom of choice implies excluded middle. – Mike Shulman CommentedMay 12, 2021 at 15:51 2 @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). – Peter LeFanu Lumsdaine CommentedMay 12, 2021 at 17:42