How can I prove that the category of internal categories has pullbacks?

Question

I have to prove that if $\mathbb{C}$ is a category with pullbacks, then the category of internal categories in $\mathbb{C}$, namely $\mathsf{Cat}(\mathbb{C})$, has pullbacks too. I wanted to find an elegant solution but I couldn't. Any help would be appreciated.

Answer 1

Let us denote by $C=(C_0,C_1)$ an object in the category of internal categories; $C_0$ is the objects object and $C_1$ is the morphisms object. It is natural to define the pullback of two morphisms $f = (f_0,f_1):C \to E$, $g=(g_0,g_1):D \to E$ as $P = (P_0,P_1)$, where $P_0 = C_0 \times_{E_0} D_0$ and $P_1 = C_1 \times_{E_1} D_1$ (the first along $f_0,g_0$, and the second along $f_1,g_1$). The natural morphisms $P \rightrightarrows C,D$ are given by the corresponding natural morphisms of $P_0$ and $P_1$. The pullback square commutes because its two component pullback squares do and composition in the category of internal categories is defined componentwise.

Also if $X \rightrightarrows C,D$ is another candidate making the pullback square commute, the two component commuting squares yield unique morphisms (in $\mathbb{C}$) $X_0 \to P_0$ and $X_1 \to P_1$. These form a unique morphism $X \to P$ making the pullback diagram commutative.

Answer 2

One possible solution is ysing the fact that the category of internal categories in $\mathbb C$ is equivalent to the category of pullback preserving functors from the finite-limit theory of categories to $\mathbb C$.

From this equivalence one can conclude observing that this categories of functors is closed under pullbacks: to prove this one can use the fact that for any category $\mathbb T$ the functor category $[\mathbb T,\mathbb C]$ is closed for pullbacks, since $\mathbb C$ is pullback-closed, and then prove that a functor that is the pullback of pullback preserving functors in $[\mathbb T,\mathbb C]$ is pullback preserving. This proves that the category of pullback-preserving functors is closed for pullback, hence so does the equivalent category $\text{Cat}(\mathbb C)$.