I've been thinking of a way of presenting a "bootstrapping" of topos theory using the internal language as much as possible. What I'm thinking of is that the basic terms of the internal language would be chosen to be the ones where the interpretation is easiest to construct from the basic definition of a topos as a category with finite limits and power objects:
- $1$, $\times$, ordered pair terms, $\pi_1$, $\pi_2$, etc.
- $P$ taking a type and returning another type
- $\Omega := P(1)$
- $=$ (or $=_X$ if we want to disambiguate the type of the arguments) with output of type $\Omega$
- $\in$ (or $\in_X$ with left argument of type $X$, right argument of type $P(X)$, and output of type $\Omega$).
- $\{ x : X \mid \phi \}$ of type $P(X)$ where $\phi$ is intended to be a term, with $x$ possibly a free variable, of type $\Omega$
- Similarly, $\{\{ x : X \mid \phi \}\}$ which gives a type.
- $\wedge$
And then, to construct other terms of the internal language in terms of these:
- $\top := \{ x:1 \mid x = x \} = \{ x:1 \mid x = x \}$
- $p \rightarrow q := (p \wedge q = p)$
- $\forall x : X, \phi := (\{ x : X \mid \phi \} = \{ x : X \mid \top \})$
- $\bot := \forall p : \Omega, p$
- $p \vee q := (\forall r : \Omega, (p \rightarrow r) \rightarrow (q \rightarrow r) \rightarrow r)$
- $\exists x : X, \phi := (\forall q : \Omega, (\forall x : X, \phi \rightarrow q) \rightarrow q)$
- $\exists! x : X, \phi := (\exists x_0 : X, \{ x : X \mid \phi \} = \{ x : X \mid x_0 = x \})$
- $Y^X := \{\{ f : P(X \times Y) \mid \forall x:X, \exists! y:Y, (x, y) \in f \}\}$
- $\lambda (x:X) . \tau := \{ p : X \times Y \mid \exists x:X, p = (x, \tau) \}$
- $X \sqcup Y := \{\{ S : P(X) \times P(Y) \mid (\exists x:X, S = (\{ x \}, \emptyset)) \vee (\exists y:Y, S = (\emptyset, \{ y \}) \}\}$
- $X / R := \{\{ S : P(X) \mid \exists x_0:X, S = \{ x:X \mid (x_0, x) \in R \} \}\}$
- Coequalizers of $f, g : X \to Y$ would be constructed as the quotient of $Y$ by the intersection of all equivalence relations containing $(f(x), g(x))$ for all $x : X$
- Given a morphism $f : X \to Y$, its image as a subobject of $Y$ would be defined as $\{\{ y:Y \mid \forall S:P(X), (\forall x:X, f(x) \in S) \rightarrow y \in S \}\}$
And so on.
So, I'm wondering whether something like this will work, and if so, if there's a reference which already takes this approach. (I guess one thing that's missing above is "application" of a term of type $Y^X$ to a term of type $X$, where you might need to define $f(x)$ to be the unique $y:Y$ such that $(x, y) \in f$. I have to admit that this "the unique object such that" construction is one where I'm not sure how it's usually represented in the internal language if at all - and if so, does it introduce an "entanglement" between proof theoretic terms and typing judgments where you have to prove $\exists! x:X, \phi$ is true in some context before you can conclude $\upsilon (x:X), \phi$ is of type $X$? Though I guess typing judgments for saying whether some term is of type $\{\{ x:X \mid \phi \}\}$ could also be another such entanglement already.)