As for Markov's principle, Toby Bartels made a similar claim on the nLab in 2011 when he wrote on the nLab "Equivalent forms: ... If a Cauchy real number does not equal zero, then it is apart from zero in that it has a multiplicative inverse." but didn't provide a proof or reference for that either.

@AndrejBauer We do not have countable choice here. We are using the Cauchy real numbers here because that is what Toby Bartels was talking about in 2012 when he wrote on the nLab "In any case, if we use the Cauchy real numbers (sequential real numbers), then the sequential analytic (L)LPO is the same as the (L)LPO for natural numbers." but he did not provide a proof or reference for that statement.

@Gro-Tsen These Cauchy sequences come with a modulus as that is the convention in constructive mathematics when constructing the Cauchy real numbers as far as I am aware. I have edited the question to clarify that.

There remains a gap to proving Mochizuki's corollary 3.12.

To answer my question above, Peter Scholze writes in the comments of mathoverflow.net/q/468079 that "In any case, this whole discussion is only about Joshi's proof, not Mochizuki's; I do not think that there is a real error internally in IUT IV."

Peter Scholze doesn't believe that Joshi's version of Corollary 3.12 is the same as Mochizuki's version of Corollary 3.12 either. He writes in mathoverflow.net/q/468079 that "The critical difference between Joshi and Mochizuki is that "Joshi's version of Mochizuki's Corollary 3.12" (=Joshi's Theorem 9.11.1) has a purely local proof and hence cannot have the same content as Mochizuki's Corollary 3.12."

Does the mistake in Proposition 6.10.7 also invalidate Mochizuki's original proof of Theorem 1.10 in IUTT IV, thus invalidating Mochizuki's original proof of the abc conjecture?

The floor and ceiling in general were first defined by Adrien-Marie Legendre in 1798 for Legendre's formula, but those were defined as functions from the rational numbers to the integers. When were the floor and ceiling functions first defined on the real numbers? The real floor and ceiling functions can't be proven to exist in constructive mathematics.

Booij writes in section 6.1: "The structure of a locator has been used previously by The Univalent Foundations Program in a proof that assuming either countable choice or excluded middle, the Cauchy reals and the Dedekind reals coincide [91, Section 11.4]."

Locators are the name Auke Booij gave to the elements of the dependent product that appears in Lemma 11.4.1 in the HoTT book.