\) One characteristic which sets category theory apart from other theories is that for any concept there exists a dual. This makes category theory an obvious choice when setting out on an investigation of a dual concept. In this post we take a look at the less well-known dual of implication which we call coimplication, but is also known as subtraction or exclusion.

Implication corresponds to the right adjoint of the cartesian product. That is, a cartesian category \(\) models implication if the functor \(A (-) : \) has a right adjoint, which we denote \(A B\) for objects \(A\) and \(B\). By the functor \(A (-) : \) having a right adjoint we mean that there is a natural bijection \( : \). This gives rise to the necessary tools for working with implication like currying, which is given by the bijection itself, and evalution \( : (A B) A B\). As an example using these morphisms along with the associator, \(: (A B) C A (B C)\), and the symmetry, \(: A B B A\), of the cartesian product we can prove \((;( );^{-1};( );;) : (A B) (B C) (A C)\). A category with products, a terminal object, and the right adjoint to the product functor is called a cartesian closed category (CCC), and the right adjoint to the product is often called the interal hom, because it can be seen as a bifunctor: \((-) (-) : ^{} \) which is an internalization of the homspace functor.

Now coimplication corresponds to the left adjoint of the coproduct functor. This is dual to that of implication. Thus, we have a bijection \( : \). We also have the coevaluator \( : B (A - B) + A\). The left adjoint to the coproduct functor is called the co-internal hom, and a category with coproducts, an initial object, and a co-internal hom is called a cocartesian coclosed category (coCCC).

The question this post gives an answer to is “does it make sense to have a category that is both cartesian closed and cocartesian co-closed?” The answer happens to be negative and is due to Tristan Crolard. The main result that we will need is due to André Joyal. We will show that any category which is both cartesian closed and cocartesian coclosed is degenerative in the sense that it is a preorder, that is, for any two objects \(A\) and \(B\) the homspace \(\) has at most one element. We call a category that is both a CCC and a coCCC a bi-cartesian closed categories (biCCC).

First, we need some basic results.
In any CCC \(\), if \(\) is an initial object in \(\) and \(\) is non-empty, then \(A A \). This follows easily from the universial mapping property for products. ▌

In any CCC \( C \), if \(\) is an initial object in \(\), then so is \(A\) for any object \(A\) of \(\). We know that the universal morphism for the initial object is unique, and hence, the homspace \(\) for any object \(B\) of \(\). Then using the right adjoint to the product functor we know that \( \), and hence, there is only one arrow between \(A\) and \(B\). ▌

In any CCC \(\), if \(\) is a terminal object in \(\), then for any object \(A\), \(A A A \). This follows easily from the universial mapping property for products. ▌

Observe the following. A biCCC is a CCC whose dual is also a CCC. Follows from a straightforward use of duality. ▌ Thus, the three basic results we gave apply to any biCCC.

We have now arrived at the main result by Joyal. In any CCC \(\), if \(\) is an initial object in \(\) and \(\) is non-empty, then \(A\) is an initial object in \(\). Suppose \(\) is a CCC such that \(\) is an initial object in \(\), and \(A\) is an arbitrary object in \(\). Furthermore, suppose \(\) is non-empty. By the first basic lemma above we know that \(A A \), and by the second \(A \) is initial, thus \(A\) is initial. ▌

Notice that the proof of the previous lemma hinges on the fact that the universal morphism is unique. If we took the initial object to be weak instead, then the previous result would not hold.

Finally, we have the main result of this post due to Crolard. If \(\) is a biCCC, then for any two object \(A\) and \(B\) of \(\), \(\) has at most one element.
Suppose \(\) is a biCCC, and \(A\) and \(B\) are objects of \(\). We know from above that \(B B\). Thus, we know that \( \). Using the internal hom adjunction we know the following:
\( \)
Taking the dual of this chain of isomorphisms yields:
\( \)
Therefore, by Joyal’s theorem above \(\) has at most one element. ▌

Again, the previous result hinges on Joyal’s result, but can be prevented by using weak initial objects.

So, what are the repercussions of all of this? We do not have a categorical proof theory for languages consisting of implication and coimplication. For example, the logics: subtractive logic, L, and dualized intutionistic logic. This is not desirable.

Are there anyways around this? Well, taking weak initial objects is one way. Interestingly enough, the structural rules are causing havoic here. If we take instead of cartesian closed categories and cocartesian coclosed categories we use monoidal closed and monoidal coclosed categories we do not have any issues. The internal hom then would be a right adjoint to the tensor product, and the cointernal hom would be the left adjoint of par. So an option is to work with linear logic instead. In fact, Lambek used the cointernal hom in his work on categorical grammars. Another option is to split the atom and keep the cartesian closed part separate from the co-cartesian closed part. This is the direction I am working on right now. I plan to talk more about this in a future post.