Assuming decidable equality but not LEM in HoTT

Question

The law of excluded middle in homotopy type theory is a term of $$\prod_{A:\mathcal{U}}\Big(\mathrm{isProp}(A)\to(A+\neg A)\Big).$$What if we assume a term of$$\prod_{A:\mathcal{U}}\Big(\mathrm{isSet}(A)\to\prod_{x,y:A}\big((x=y)+\neg (x=y)\big)\Big)$$instead?

Is this a strictly weaker axiom than LEM? Is it useful? Are there any philosophical reasons to accept this axiom but not LEM?

EDIT: If we only assume a term of$$\prod_{A:\mathcal{U}_0}\Big(\mathrm{isSet}(A)\to\prod_{x,y:A}\big((x=y)+\neg (x=y)\big)\Big)$$does that change much?

Answer 1

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.

Answer 2

In addition to Simon Henry's proof you can also use suspensions to show that decidable equality implies the law of excluded middle. Given a proposition $A : \mathrm{hProp}$ you can show using an encode-decode argument that the suspension $\Sigma A$ is a set and that the equality $N = S$ is equivalent to $A$. So decidable equality for every set of the form $\Sigma A$ implies the law of excluded middle.