Exercise 11.6 seems to need WLPO not LPO

[jkingdon]

My metamath contributors and I have formalized, not exactly Exercise 11.6 as stated, but something pretty close. What we have is:

• for part (ii) we were able to prove WLPO and not LPO (by itself this means little, as perhaps a different proof would yield LPO): https://us.metamath.org/ileuni/nconstwlpo.html
• for part (i) we were able to prove a stronger version of the exercise where the existence of the function follows form analytic WLPO not full excluded middle: https://us.metamath.org/ileuni/dceqnconst.html

Unless there is some subtlety here (analytic vs non-analytic omniscience principles, IZF set theory versus type theory, etc), this means that LPO, as specified in Exercise 11.6(ii), is not attainable. I'm not proposing alternate wording because I'm not sure what the best fix is. As far as I noticed, the HoTT book doesn't currently mention WLPO at all and perhaps it is too much of a digression to get into it. I suppose perhaps the exercise could be worded as decidability of real number equality (assuming that is indeed doable and easy enough for an exercise - our proof of Exercise 11.6(ii) is for WLPO not analytic WLPO)

cc @benjub