Topoi as models of constructive mathematics

Question

In this question, it is argued that constructive mathematics cannot prove the existence of a discontinuous real function, because there is a topos $\mathcal{E}$ where all real functions are continuous. However it is not clear to me why the mere existence of this topos $\mathcal{E}$ affects constructive frameworks like Coq, Agda or Homotopy type theory. If we managed to define a discontinuous function $f:\mathbb{R}\to\mathbb{R}$ in Coq, it would produce a contradiction in $\mathcal{E}$ only if $\mathcal{E}$ can interpret $f$ and all the Coq machinery that was used to define $f$.

For instance the Coq model I know in the topos of sets needs the extra assumption that there is a countable infinity of inaccessible cardinals (to interpret Coq's universes). And I doubt that topos $\mathcal{E}$ automatically has those inaccessible cardinals. Furthermore, if we add the excluded middle axiom in Coq we will easily define discontinuous real functions, and that will still be fine in $\mathcal{E}$, because $\mathcal{E}$ cannot interpret the excluded middle.

So I wonder whether topoi like $\mathcal{E}$ only give favorable clues, but not proofs, that some propositions cannot be proved constructively.

Answer 1

First, it is clear that once we add classical logic to Coq, we're no longer doing constructive mathematics.

Second, for the special case of Coq, it is clear that Coq can be interpreted in any autological topos (a topos in which collection + separation are satisfied) with countably many Grothendieck universes. Conversely, if Coq is consistent, then so is ZFC + $\omega$-many Grothendieck universes (which implies the consistency of the theory of an autological topos with $\omega$-many Grothendieck universes - namely, the category of sets is such a topos) - see this answer for details.

Now there are quite a few toposes in which all functions $\mathbb{R} \to \mathbb{R}$ are continuous. Generally, when one is interpreteting Brouwerian intuitionism, the canonical tool one uses is Kleene's second realizability model. The topos-theoretic version of this is the realizability topos over Kleene's second PCA. As explained here, realizability toposes are automatically autological when the ambient set theory satisfies collection and separation.

It turns out that, as explained here, if there are $\omega$-many Grothendieck universes in the ambient set theory, then there are $\omega$-many in a realizability topos.

Thus, the construction results in a model of Coq in which all functions $\mathbb{R} \to \mathbb{R}$ are continuous. So it is relatively consistent with Coq that all such functions are continuous.

It's also possible to derive this principle by going through a certain sheaf topos as per Mac Land and Moerdijk. Sheaf toposes are also automatically autological when the metatheory satisfies collection + replacement, and they also inherit $\omega$-many Grothendieck universes from the ambient set theory. So this is another way of coming to the same result.

I don't know what the situation is with HoTT or Agda. I'm sure that Agda and Coq's situations will be similar, but I have no expertise in that area. I imagine that HoTT will admit some sort of sheaf-like models which will let us parallel the constructions mentioned above, but I'm not sure.