A category $C$ is **locally cartesian** if each of its slice categories $C/x$ is a cartesian monoidal category, meaning that $C/x$ has all finite products. Another way to say this is that $C$ has all finite fibred products or equivalently that $C$ has all pullbacks.

A **finitely complete category** is precisely a locally cartesian category that has a terminal object.

Last revised on July 18, 2022 at 05:26:53. See the history of this page for a list of all contributions to it.