Conclusion

Abstract

Cut elimination in categories is better adapted to a purely categorial context than to a context that approaches logic. With free adjunctions in the (ac) formulation of the rectangular || notion, and with free comonads formulated analogously, we obtained an exact match between the defining equalities of these notions and equalities necessary and sufficient for cut elimination in the form of Cut Disintegration. In the case of special adjunctions motivated by logic, of which we have considered what is presumably the most basic one—the adjunction of categories with binary product—matters are not so straightforward. In the (ac) formulation of the rectangular || notion for this adjunction, cut elimination fails, while in other formulations it obtains, but at the cost of having equalities unnecessary for cut elimination.