Given an arbitrary topos $\mathscr{T}$ and objects $X, Y$ of $\mathscr{T}$, are the interpretations of the following terms equal to $\top : \mathrm{Hom}(1, \Omega)$?
$\forall p, q : \Omega, (p \rightarrow q) \rightarrow (q \rightarrow p) \rightarrow p = q$.
$\forall f, g : {}^X Y, (\forall x : X, f(x) = g(x)) \rightarrow f = g$.
$\forall S_1, S_2 : P(X), S_1 \subseteq S_2 \rightarrow S_2 \subseteq S_1 \rightarrow S_1 = S_2$.
My attempt at 2, for example, would be: suppose we use a test object $U$, and we have $f, g : \mathrm{Hom}(U \times X, Y)$. The interpretation of the term in parentheses would suggest for any morphism $\phi : \mathrm{Hom}(V, U)$ and term $x : \mathrm{Hom}(V, X)$, then $f \circ (\phi, x) = g \circ (\phi, x)$. (More precisely, the pullback of $f$ to $\mathrm{Hom}(V \times X, Y)$ would be $f \circ (\phi \circ \pi_1, \pi_2)$, and then evaluation at $x$ corresponds to composing on the right with $(\mathrm{id}_V, x)$; so the result is $f \circ (\phi \circ \pi_1, \pi_2) \circ (\mathrm{id}_V, x) = f \circ (\phi, x)$, and similarly for $g$.) But then, by simply choosing $V := U \times X$, $\phi := \pi_1$, and $x := \pi_2$, we get $(\phi, x) = \mathrm{id}_{U \times X}$ so $f = g$.
And for 1, suppose we use a test object $U$, and we have $p, q : \mathrm{Sub}(U)$. Then $p \rightarrow q$ would be interpreted as $p$ factors through $q$, and $q \rightarrow p$ would be interpreted as $q$ factors through $p$. Therefore, $p \simeq q$, and by the definition of equality in $\mathrm{Sub}(U)$ this implies $p = q$. And 3 I think would be similar, except that $S_1, S_2 : \mathrm{Sub}(U \times X)$.
So, does this make any sense, or is it complete nonsense? I haven't actually seen a detailed treatment of the internal language, so I've been attempting to reconstruct what it might look like. My interpretation seems to largely make sense to me though I tend to get bogged down in the details if I try to formalize it generally - but also as far as I know, my interpretation might be completely off-base compared to the "official" one, and maybe even the question doesn't make sense.
As an optional follow-on question: is there a version of the internal language of a topos which allows for "proof terms" as in the Curry-Howard correspondence and if so, does it satisfy proof irrelevance: $\forall p : \Omega, \forall \alpha, \beta : p, \alpha = \beta$? What about definite description: is there a way to interpret something similar to $(\exists! x:X, \phi) \to \{ x:X | \phi \}$ in a topos where $\phi$ is a term of type $\Omega$ with a free variable $x : X$?
(Basically, I'm going through the classical axioms which aren't automatic in Coq's logic - though there are things there like the Type(n) hierarchy which have no interpretation in an arbitrary topos. Obviously, excluded middle and axiom of choice are not valid even in general algebraic-geometric sites. And "indefinite description" $(\exists x:X, \phi) \to \{ x:X | \phi \}$ isn't accepted even by most classical mathematicians as a valid way of giving a "definition", even if it's a consistent axiom.)
