nLab locally cartesian (infinity,1)-category

Definition

An $(\infty, 1)$-category $C$ is locally cartesian if each of its slice $(\infty, 1)$-categories $C/x$ is a cartesian monoidal $(\infty, 1)$-category, meaning that $C/x$ has all finite products. Another way to say this is that $C$ has all $(\infty, 1)$-pullbacks.

Properties

In any locally cartesian $(\infty, 1)$-category, the base change $(\infty, 1)$-functor has a left adjoint $(\infty, 1)$-functor called the dependent sum.

The internal logic of a locally cartesian $(\infty, 1)$-category is expected to be a dependent type theory with identity types and dependent sum types.

 Examples

• Every finitely complete $(\infty, 1)$-category is a locally cartesian $(\infty, 1)$-category with a terminal object.

• Every locally cartesian closed $(\infty, 1)$-category is a locally cartesian $(\infty, 1)$-category in which the base change $(\infty, 1)$-functor has a right adjoint $(\infty, 1)$-functor called the dependent product.

Related entries

• locally cartesian category

• locally cartesian closed (infinity,1)-category