Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.
Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.