(1) Yes. The particular dependent type theory one wants to use has UIP (Uniqueness of Identity Proofs), one universe of all propositions (in the homotopy-type-theory sense, i.e. subsingletons) satisfying propositional extensionality, pushouts (a kind of higher inductive type), and propositional truncations. This is a sort of truncated version of homotopy type theory.
(2) The type theory described above is one state of the art. Alternatively, one can use higher-order logic as described, for instance, in Sketches of an Elephant. I tend to prefer dependent type theory, since dependent types occur naturally in mathematics; but the semantics and metatheory are more difficult in that case (and filling in some of their details is a problem of current research).
(3) Agda, Coq, Idris can all manage this type theory easily, when suitably augmented by axioms (for UIP, propositional extensionality, etc.). The main wrinkle is that they all have a tower of universes, which an arbitrary elementary topos may not; but you can just ignore the larger universes. You can also reason in higher-order logic inside such a proof assistant by simply not making use of the dependent types.
Not having read Goldblatt, I am not exactly sure what he's getting at.
However, there is a concept which he might be addressing.
A lot of applications of internal logic go something like this:
We are given some sort of property $P$ about objects and morphisms in a topos. We then try to translate this property into some property $Q$ such that if $P$ holds in the external logic, then $Q$ holds in the internal logic.
We then prove in constructive logic that $Q \to R$, so we know that $Q \to R$ must hold in the internal logic by soundness.
Finally, we show that if $R$ holds in the internal logic, then $S$ holds in the external logic.
This gives us a complete proof that $P \to S$ in the external logic.
For example, take the lemma in the answer that you cited.
Let $\mathcal{F}$ be an $\mathcal{O}_X$-module locally of finite type.
Then $\mathcal{F}$ is locally free iff its rank is constant.
Here, $X$ is a reduced scheme.
$P$ is the statement "$\mathcal{F}$ is an $\mathcal{O}_X$-module locally of finite type, and $X$ is a reduced scheme". The corresponding statement in the internal logic is $Q = $"$\mathcal{F}$ is a finitely generated $\mathcal{O}_X$-vector space, and $X$ is a field". Note that since we are working in constructive logic, it's critical to pick the right definition of "field", but we'll gloss over that little detail for now.
We then switch to "internal logic mode", put on our intuitionist hats, and prove in constructive logic the statement $Q \to R$, where $R$ is the statement "$\mathcal{F}$ is a free vector space if and only if there is some smallest $n \in \mathbb{N}$ such that $\mathcal{F}$ is generated by $n$ elements as a vector space".
Therefore, we know that $R$ holds in the internal logic. The fact that $R$ holds in the internal logic allows us to conclude statement $S$, which is "$\mathcal{F}$ is locally free iff its rank is constant".
More abstractly, we come up with a "global model" of the first-order sentence $Q$, which we then determine is also a global model of the first-order sentence $R$. We then interpret this in the external logic to get free theorems.
However, consider that models can also exist locally. In other words, we may have $\Vdash \exists M (M \models R)$ without there actually being a model of $R$ in the topos. This is different than coming up with a structure $M$ and then proving $\Vdash M \models R$. Note that this requires a form of the internal logic which can quantify over objects.
The interpretation of $\Vdash \exists M (M \models R)$ in the topos $E$ is that there is some epi $V \to 1$ and some structure $M$ in the topos $E / V$ such that in the internal logic of $E / V$, we have $\Vdash M \models R$.
So in other words, if we have a topos $E$ which believes that there is a model of $R$, we can find a nontrivial slice of $E$ for which there actually is a model of $R$.
This means that if we can prove the existence of a model of a formula in a nontrivial topos, we can come up with some other nontrivial topos where there actually is such a model.
Best Answer
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 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.