Reference for "external logic" and comparison with internal I'm currently studying Sheaves in Geometry and logic. I have learned about the Mitchell-Bénabou language, Kripke-Joyal/Sheaf semantics, etc, but I wanted to understand what is meant by "external logic". Since this book is my first contact with the subject, the problem might be that I have a restricted understanding of logic in a topos. As far as I understand, when talking "externally" one talks about properties of the topos, while internal means formulated in some internal language. Example: external AC = every epi is split, internal AC = the corresponding statement in the internal language is valid, and the two are not necessarily equivalent, and external operations = those on the lattice of subojects, internal = the arrows induced by Yoneda, etc.
However, I have heard in a video (which is not about this topic) that when a topos is well-pointed the internal and external logic coincide.
How something like this can be formulated as a theorem? MacLane and Moerdijk prove that AC holds iff IAC holds when a topos is well-pointed, but that is a specific case. Also, well-pointedness means $Hom(1, -)$ is faithful, does this functor play a role in this?  Is there a notion of external validty? Any reference is appreciated, I couldn't find it anything explaining what "external" means in nlab.
 A: A very thorough paper discussing this topic can be found here.
To summarise the paper, a statement in the language of category theory is a first-order statement about a category which can quantify over objects and, given two objects $A, B$, over the arrows from $A$ to $B$, where the atomic propositions are always of the form $f = g$, and both $f$ and $g$ are arrows with the same domain and codomain. It is not permitted in this language to discuss equality of objects, nor can we discuss equality of arrows unless they syntactically have the same domain and codomain.
An example of such a statement would be $\forall A \exists f : A \to B \forall g : A \to B (f = g)$. This is the statement that $B$ is a terminal object.
Fix a terminal object $1$. The notation $x :\in A$ is shorthand for $x : 1 \to A$. Given $f : A \to B$ and $x :\in A$, the term $f(x) :\in B$ is shorthand for $f \circ x$.
The following statement expresses one part of the property of well-pointedness:
$$\forall A, B \forall f, g : A \to B, (\forall x :\in A, f(x) = g(x)) \to f = g$$
Note the above part of well-pointedness, if interpreted as a statement in normal set theory, is just the statement of function extensionality.
If we are talking about a category with enough structure, such as a topos, we can take a statement $\phi$ in the language of category theory and construct a new statement $X \Vdash \phi$ in the language of category theory. This translation is known as the “stack semantics”. If we restrict $\phi$ to only contain quantifiers over arrows and not over objects, we can interpret $\Vdash$ using the Kripke-Joyal semantics or any number of other methods and get an equivalent statement. The stack semantics is a generalisation of this.
We say a statement $\phi$ holds in a category $C$ externally if $\phi$, interpreted in the obvious way, is true about $C$. So for instance, $\forall A, B \forall f, g : A \to B, (\forall x :\in A, f(x) = g(x)) \to f = g$ is true externally in $C$ if and only if $1$ is a generator in $C$.
But we can also discuss what it means for $\phi$ to be true internally in $C$. This is exactly saying that $1 \Vdash \phi$ is true externally in $C$. In particular, $\forall A, B \forall f, g : A \to B, (\forall x :\in A, f(x) = g(x)) \to f = g$ is always true in $C$.
We have the following two results:

The following are equivalent: (a) for every statement $\phi$ which doesn’t involve quantifies over objects (but can take parameters in $C$), $\phi \iff 1 \Vdash \phi$ holds in $C$, (b) $C$ is (constructively) well-pointed


The following are equivalent: (a) for every statement $\phi$ with parameters in $C$, $\phi \iff 1 \Vdash \phi$ holds in $C$, (2) $C$ is (constructively) well-pointed and satisfies the axiom scheme of collection.

The axiom of choice is a good example of this phenomenon. The external axiom can be stated as $\phi :\equiv \ulcorner$For all epis $f : A \to B$, there is some $g : B \to A$ such that $f \circ g = 1_B \urcorner$. The internalisation $1 \Vdash \phi$ is equivalent to the statement that for all $f : A \to B$, the right adjoint to pullback $\Pi_f : C / A \to C / B$ preserves epis. If $C$ is well-pointed, the two statements are equivalent.
