The maximality of Cartesian categories (Q2707078)

This article considers the equations between arrows that are assumed in the definition of a Cartesian category, that is a category with binary products and a terminal object. It is shown that extending these equations with any new equation obtained from the language of free Cartesian categories will collapse the Cartesian category into a preorder. Hence the title ``maximality of Cartesian categories''.NEWLINENEWLINENEWLINEThe proof utilizes a coherence theorem addressing uniqueness in normal form in the free Cartesian category on a set of objects \({\mathcal O}\). The authors conclude the article with a discussion of the implication of these results for logic.