What is an injection in a topos? I am reading the paper of Andrej Bauer that proves there is a realizability topos in which there is an injection from the internal Baire Space $\mathbb{N}^\mathbb{N}$ to the natural numbers $\mathbb{N}$.
This is discussed in Andrej's blog too.
My question is about the definitions. What does it mean when we say that there is an injection or a surjection in the internal logic of a topos? Does an injection correspond to a monomorphism and a surjection to an epimorphism? Can I please, get some references to that definition if it is true.
If that is not the case, then I am very confused because morphisms in a realizability topos are not functions (for example by taking the exact completion of the category of the assemblies of a partial combinatory algebra) and so one cannot talk about injectivity or surjectivity.
Or is the existence of the injection implied by some other means, i.e. the injection does not correspond to a specific morphism in the topos by rather an object or a class of morphisms and objects with specific properties.
 A: To directly answer your question: Andrej meant "monomorphism".
Since the objects of a topos don't typically consist of (raw, unstructured) sets, the usual notions of injectivity and surjectivity don't apply. But for convenience, people still talk about "injections" and "surjections" in those contexts (and mean monomorphisms and epimorphisms, respectively). This is also common when dealing with abelian categories.
The story doesn't end here. Malice is right with their comment. The internal language of a topos allows you to formulate statements about objects of the topos in a naive, element-based way. The Kripke–Joyal semantics translates such formulas to external ones. It turns out that the translation of the internal statement "the map $f$ is injective" is precisely "the morphism $f$ is a monomorphism".
You can learn about the internal language in the sections VI.5, VI.6, and VI.7 of Mac Lane and Moerdijk's excellent textbook Sheaves in Geometry and Logic. I also found lecture notes by Thomas Streicher very nice and very useful. Of course there's also an nLab entry. If you prefer slides, then you can have a look at these slides of mine which accompany expository notes. (Please don't hesitate to contact me should you have any questions.) The translation of injectivity to being a monomorphism is shown in detail in Example 2.3 on page 8, however in the slightly different setting of a sheaf topos instead of a realizability topos.
I think that the internal language of a topos is a fascinating topic, since it allows you to "explore alternate mathematical universes". But you probably don't need it in order to understand Andrej's nice article. In case you want to refresh your knowledge on realizability, Andrej has very nice notes about it.
