For the last months I've been trying to become familiar with the so-called "internal language of a category". However, I'm still not confident enough when, for instance, I find a subobject (of a given object) which is defined through a formula of the internal laguage of the category I'm considering.
In detail, if $\mathcal{C}$ is a pretopos, $A$ is an object of $\mathcal{C}$ and $\phi$ is a formula in the internal language of $\mathcal{C}$, I'm not fully able to understand the following two things:
$1)$ Which is the actual subobject $B$ of $A$ represented by the expression $\{x \in A:\phi(x)\}$. Meaning, how I can recover $B$ in terms of "categorical operations" in $\mathcal{C}$.
$2)$ How I can work with $\{x \in A:\phi(x) \}$. That is, for instance, how I can verify through a completely syntactical procedure that $\{x \in A:\phi(x) \}$ is the object I was looking for.
Of course, I'm not asking you to answer points $(1)$ and $(2)$, as they are too generic. I would prefer if you suggested me a self-contained chapter of a book or some lecture notes where this subject is fully explained. In my opinion, I would especially need a collection of basic examples and exercises regarding its use.
Thanks in advance.
Best Answer
The answer is, to some extent, there's nothing to do. If you start with a theory, then you just have a bunch of syntactical formulas and subobjects aren't involved until you provide an interpretation. Once you do, a formula $\varphi(x)$ where $x$ is of sort $A$ will simply be interpreted as a subobject of the interpretation of the sort $A$. This is a direct generalization of the set-theoretic case.
If you start with a pretopos, then the internal language of that pretopos will simply have a predicate symbol for each subobject. Of course, we'll have an interpretation that will interpret each such predicate symbol as the subobject it corresponds to. This is more or less the counit of this adjunction. This procedure may lead to a theory that has a proper class of predicate symbols and axioms, and I believe you just have to stretch your notion of theory to accept that.
Now to be clear, it is important to separate a subobject from a monomorphism. A subobject is an equivalence class of monomorphism. Having a subobject doesn't provide you with a particular object. You may need the Axiom of Global Choice to pick representatives if no other structure is available. (Maybe there's a way to get away with less in general, perhaps using Scott's trick.)
To prove things, you just prove things like normal in the theory. For the theory generated from the given pretopos, you'll have an axiom asserting every formula that you can formulate in the theory with predicate symbols corresponding to subobjects which is true under interpretation. In other words, for the theory generated from the given pretopos, a formula is provable if and only if its interpretation is true in the given pretopos.