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?

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?