Does the forgetful functor from the category of models of a cartesian theory preserve and create limits?

61 Views Asked by At

It is well-known that a monadic functor preserves and creates limits, which in particular shows that any algebraic category, or equivalently, any category of models of an algebraic theory, has limits, and the forgetful functor creates them.

I'm wondering whether the same holds for cartesian theories as well. Since cartesian theories corresponds exactly to some sort of partial algebras, I'm expecting this to hold. Also, as an example, in the case of the cartesian theory of categories this indeed holds. The theory of categories $\mathbb T$ is itself cartesian; and for any finitely complete category $\mathcal C$, $\mathbb T$ models in $\mathcal C$ are just internal categories in $\mathcal C$, and we denoted this category as $\mathbf{cat}(\mathcal C) = \mathrm{Mod}_\mathbb T(\mathcal C)$. Now it is well-known that the forgetful functor $$ \mathbf{cat}(\mathcal C) \to \mathcal C^2 $$ preserves and creates limits (the codomain of the forgetful functor is $\mathcal C^2$ because the cartesian theory of categories has 2 sorts, viz. objects and morphisms).

I couldn't find any reference on this. It would be really helpful if you know any reference that contains such (either positive or negative) results; I guess this should be well-established.