nLab locally cocartesian coclosed category

Idea

The dual of a locally cartesian closed category.

Definition

A locally cocartesian coclosed category is a category $C$ whose coslice categories $x/C$ are all cocartesian coclosed categories. Equivalently, it is a category $C$ with all coexponentiable morphisms?.

Properties

A locally cocartesian coclosed category should be the categorical semantics of codependent type theory.

See also

• coexponential object

• coslice category

• cocartesian coclosed category

• codependent type theory

• coinductive type

• cotopos

• locally cartesian closed category