nLab cocartesian coclosed category

Contents

Contents

Idea

The notion of a cocartesian coclosed category is dual to that of a cartesian closed category.

Definition

A cocartesian coclosed category is a locally cocartesian coclosed category CC with an initial object. Equivalently, it is a category CC with finite coproducts and coexponential objects.

Properties

Any category which is both cartesian closed and cocartesian coclosed is a thin category, though it may not be the terminal category (e.g., any Boolean algebra is such a category).

Proof

Let a category be given which is both cartesian closed and cocartesian coclosed. Cartesian closure tells us that the product of any object with the initial object 00 will be itself initial (as left adjoints preserve colimits). Furthermore, given any morphism from an object AA to 00, we can pair this with the identity morphism on AA to obtain a morphism from AA into A×0A \times 0 with a left inverse given by projection, thus identifying AA as a retract of an initial object, and therefore as an initial object itself. It follows immediately that any two parallel morphisms to 00 are equal; equivalently, by the dual reasoning, any two parallel morphisms out of 11 are equal. But this means any two parallel morphisms in general are equal, as maps from XX to YY can be identified with maps from 11 to Y XY^X; accordingly, the category must be a thin category.

Examples

The Kleisli category of a continuation monad K R=R R ()K_R = R^{R^{(-)}} on a cartesian closed category with coproduct C\mathbf{C} is cocartesian coclosed. In fact ()×R AA+()(-) \times R^A \dashv A + (-), which we can prove using the cartesian closure of C\mathbf{C}:

Kl(K R)(B×R A,C)C(B×R A,R R C)C(B×R A×R C,R) \mathbf{Kl}(K_R)(B \times R^A, C)\cong \mathbf{C}(B \times R^A, R^{R^C}) \cong \mathbf{C}(B \times R^A \times R^C, R) \cong
C(B×R A+C,R)C(B,R R A+C)Kl(K R)(B,A+C) \mathbf{C}(B \times R^{A + C}, R)\cong \mathbf{C}(B, R^{R^{A+C}}) \cong \mathbf{Kl}(K_R)(B, A+C)

See also

Last revised on November 17, 2022 at 17:17:35. See the history of this page for a list of all contributions to it.