Durante los últimos meses he intentado familiarizarme con el llamado "lenguaje interno de una categoría". Sin embargo, todavía no me siento lo suficientemente seguro cuando, por ejemplo, encuentro un subobjeto (de un objeto dado) que se define mediante una fórmula del lenguaje interno de la categoría que estoy considerando.
En concreto, si $C$ es un pretopos, $A$ es un objeto de $C$ y $\phi$ es una fórmula en el lenguaje interno de $C$ No soy capaz de entender del todo las dos cosas siguientes:
-
Que es el subobjeto real $B$ de $A$ representado por la expresión $\{ x\in A:\phi(x)\}$ ? Es decir, cómo puedo recuperar $B$ en términos de "operaciones categóricas" en $C$ ?
-
¿Cómo puedo trabajar con $\{ x\in A:\phi(x)\}$ ? Es decir, por ejemplo, cómo puedo verificar mediante un procedimiento completamente sintáctico que $\{ x\in A:\phi(x)\}$ ¿es el objeto que estaba buscando?
Por supuesto, no le pido que responda a los puntos (1) y (2), ya que son demasiado genéricos. Preferiría que me sugirieras un capítulo autocontenido de un libro o unos apuntes de clase donde se explique completamente este tema. En mi opinión, lo que necesito en particular es una colección de ejemplos y ejercicios básicos sobre su uso.
Gracias de antemano.
P.D. Hice la misma pregunta en Math Stack Exchange ( https://math.stackexchange.com/questions/3262479/reference-request-about-internal-language-of-categories ).