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:


1. 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$?
2. 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>).



Reference request about “internal language of categories”
Here are some resources:


1. Carsten Butz.[*Regular categories and regular logic*](https://www.brics.dk/LS/98/2/), notes, 1998.
2. P. Freyd and A. Scedrov. *Categories, Allegories.* North–Holland, Amsterdam 1990.
3. S. Mac Lane and I. Moerdijk. *Sheaves in Geometry and Logic.* Springer–Verlag, New York 1992.
4. B. Jacobs, [*Categorical Logic and Type Theory*](http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html), Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.


The first one covers the fragment of logic with $\top$, $\land$, $\exists$ and $=$. The second one has first-order categorical logic, and the third one higher-order logic. Jacobs's book is very thick and intimidating, I am mentioning it because it contains rules for $\lbrace x : A \mid \phi(x)\rbrace$, which you're asking about.


