# Assuming decidable equality but not LEM in HoTT

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?

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.

• Is $U$ a term of a set? – Mallon May 5 at 18:42
• I'm using that the type of all propositions is a set, that's what I mean by a "subobject classifier". U is a proposition. – Simon Henry May 5 at 18:44

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.

• Note that $\Sigma A$ is the same set that appears in the Diaconescu-Goodman-Myhill proof that the axiom of choice implies excluded middle. – Mike Shulman May 12 at 15:51
• @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 May 12 at 17:42