Return to Answer

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think you're axiom is indeed strictly weaker than LEM. (Edit: as pointed out in aws answer below, having some higher inductive type and assuming they are in $\mathcal{U}_0$ also allows to deduce LEM from your axiom)

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that's only my opinion.

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = \mathsf{True}$ or $U \neq \mathsf{True}$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think your axiom is indeed strictly weaker than LEM. (Edit: as pointed out in aws answer below, having some higher inductive type and assuming they are in $\mathcal{U}_0$ also allows to deduce LEM from your axiom)

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that's only my opinion.

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think you're axiom is indeed strictly weaker than LEM.

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that only my opinion.

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think you're axiom is indeed strictly weaker than LEM. (Edit: as pointed out in aws answer below, having some higher inductive type and assuming they are in $\mathcal{U}_0$ also allows to deduce LEM from your axiom)

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that's only my opinion.

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think you're axiom is indeed strictly weaker than LEM.

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that only my opinion.