nLab bicartesian closed category

See also


Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory

A bicartesian closed category is a cartesian closed category with finite coproducts. In the case where this is furthermore a preorder or poset, it is called a Heyting prealgebra or Heyting algebra, respectively. They provide the semantics and proof theory of intuitionistic propositional logic.

Note that a bicartesian closed category is bicartesian (that is, it is both cartesian and cocartesian), and furthermore it is cartesian closed, but it is usually not cocartesian closed (as the only such category is the trivial terminal category), nor co-(cartesian closed) (i.e., the dual of a cartesian closed category; aka, cocartesian coclosed). Thus the terminology could be confusing, but since the only categories which are both cartesian closed and co-(cartesian closed) are preorders, there is not much danger.

Also note that a bicartesian closed category is automatically a distributive category. This follows since the functors XA×XX\mapsto A\times X have right adjoints (by closedness), so they preserve colimits.

A bicartesian closed category is one kind of 2-rig.

See also

Last revised on May 14, 2022 at 06:35:41. See the history of this page for a list of all contributions to it.