Cartesian Linearly Distributive Categories: Revisited

Abstract

Linearly distributive categories (LDC) were introduced by Cockett and Seely to provide alternative categorical semantics for multiplicative linear logic. In contrast to Barr's $*$-autonomous categories, LDCs take multiplicative conjunction and disjunction as primitive notions. Thus, a LDC is a category with two monoidal products that interact via linear distributors. A cartesian linearly distributive category (CLDC) is a LDC whose two monoidal products coincide with categorical products and coproducts. Initially, it was believed that CLDCs and distributive categories would coincide, but this was later found not to be the case. Consequently, the study of CLDCs was not pursued further at the time. With recent developments for and applications of LDCs, there has been renewed interest in CLDCs. This paper revisits CLDCs, demonstrating strong structural properties they all satisfy and investigating two key classes of examples: posetal distributive categories and semi-additive categories. Additionally, a previously assumed class of CLDCs, the Kleisli categories of exception monads of distributive categories, is re-examined and it is showed that they are not, in fact, CLDCs.