I've tried to become familiar with the so-called "internal language of a category" for the last months. 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 that I'm considering.

In detail, if $C$ is a pretopos, $A$ is an object of $C$ and $\phi$ is a formula in the internal language of $C$, I'm not completely able to understand the following two things:

Which is the actual subobject $B$ of $A$, represented by the expression $\{ x\in A:\phi(x)\}$? Meaning, how can I recover $B$ in terms of "categorical operations" in $C$?

How can I work with $\{ x\in A:\phi(x)\}$? That is, for instance, how can I verify through a completely syntactical procedure that $\{ x\in A:\phi(x)\}$ is the object that I was looking for?

Of course, I'm not asking you to answer points (1) and (2), as they are too generic. I would rather you to suggest me a self-contained chapter of a book or some lecture notes where this subject is fully explained. In my opinion, what I in particular need is a collection of basic examples and exercises regarding its usage.

Thanks in advance.

P.S. I asked the same question in Math Stack Exchange (https://math.stackexchange.com/questions/3262479/reference-request-about-internal-language-of-categories).

Sheaves in Geometry and Logic, from page 296 on. $\endgroup$ – fosco Jun 15 '19 at 20:42