The dual of a locally cartesian closed category.

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?.

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

Created on June 3, 2022 at 14:36:52. See the history of this page for a list of all contributions to it.