nLab locally cartesian category

Definitions

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.

The internal logic of a locally cartesian category is expected to be a dependent type theory with dependent sum types, identity types, and a set truncation axiom.

Related entries

• locally cartesian closed category

• locally regular category

• locally cartesian (infinity,1)-category