Background
Basic concepts
equivalences in/of $(\infty,1)$-categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
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.
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.
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.
Created on March 8, 2024 at 05:14:23. See the history of this page for a list of all contributions to it.