Divisibility properties of cells in a polycategory or multicategory have a deep connection to the rules of sequent calculi for multiplicative linear logic, as first evidenced by Cockett and Seely: the left and right introduction rules for each connective correspond either to composition with a divisible cell, or the use of its divisibility property.
Hermida relied on the same notions to devise an abstract proof of strictifiability for monoidal categories, a classic theorem of category theory. The obvious generalisation of this theorem to higher-dimensional variants, such as braided monoidal categories, fails, and weaker versions are mostly still open problems.
An analysis of the failure of Hermida's proof to generalise indicates that the modelling of units with divisible cells that have a degenerate (0-ary) boundary may be responsible. We show that it is possible to recover units from the existence of certain divisible cells of lower dimension, even when degenerate boundaries are disallowed. This leads to a weaker semi-strictification theorem, which, however, we hope to extend to arbitrary dimensions.
While the polycategorical units so obtained are equivalent to the usual ones at the level of the induced monoidal category structure, they behave very differently at the level of sequent calculus: most notably, their polarity as connectives changes. We pose some questions on the logical and computational aspects of our notion of unit, in the light, also, of the increase in the complexity of proof equivalence brought by the usual notion.