  It is proved that equalities between arrows assumed for cartesian categories
are maximal in the sense that extending them with any new equality in the
language of free cartesian categories collapses a cartesian category into a
preorder. An analogous result holds for categories with binary products, which
may lack a terminal object. The proof is based on a coherence result for
cartesian categories, which is related to model-theoretical methods of
normalization.
