There is a very good description of binoidal categories on the nlab.

Briefly, a binoidal category consists of a category $C$ and, for each $A\in Ob(C)$ a pair of functors $A\rtimes -$ and $- \ltimes A$ whose action on objects agrees in the following sense: $A\ltimes B=A\rtimes B$; we write this object $A\otimes B$. Note that the $\otimes$ notation applies only to objects; the closest equivalent for morphisms has two possibilities, which may not be equal. Given $f:A\to B$ and $g:C\to D$, the composites $A\otimes C\to B\otimes D$

$$f\ltimes D \circ A \rtimes g$$ and $$B \rtimes g \circ f \ltimes C$$

need not be equal.

Question 1: is it a consequence of the above definition of binoidal categories that $$f\ltimes(A\otimes B) = (f\ltimes A)\ltimes B$$ and $$(A\otimes B)\rtimes f = A\rtimes (B\rtimes f)$$

I suspect not: any monoidal category is a binoidal category via $-\otimes\text{id}_A$ and $\text{id}_A\otimes -$, and in a non-strict monoidal category the two morphisms "equated" above might not even have the same domain and codomain. Or perhaps I have made a mistake?

If so, this means that the equation above (and the corresponding rule for $\rtimes$) must be added as an additional part of the definition of a binoidal category. I have not found this mentioned in the literature. One is then led to a "weak" version where the equation is replaced with a natural isomorphism as below

Question 2: is it a consequence of the above definition of binoidal categories that $$\left(-\ltimes(A\otimes B)\right) \simeq \left((-\ltimes B)\circ(-\ltimes A)\right)$$ and $$\left((A\otimes B)\rtimes -\right) \simeq \left((A\rtimes -)\circ(B\rtimes -)\right)$$

Finally,

Question 3: if the answer to either (1) or (2) is "no", what is the name for a binoidal category in which the equation of (1) holds, and what is the name for a binoidal category in which the equation of (2) holds?

By analogy to monoidal categories, it would seem that the answer to (3) involves the use of the adjectives "strict" and "non-strict"; this is where the title of my question comes from.

Side note: I'm not sure that any of the above is necessarily implied by the associator of a premonoidal category; in the non-strict case that is a natural isomorphism relating the "left product" with the "right product" as shown below, rather than relating one of them to itself.

$$\left((B\rtimes -)\circ(-\ltimes A)\right) \simeq \left((-\ltimes A)\circ(B\rtimes -)\right)$$

**Edit 2-Apr**: what was previously the sole question is now "Question 1"; I have added "Question 2" and "Question 3", which were implicit in the original posting, but which I should have made explicit. Question 3 is the real goal, but might be ill-posed or trivial based on the answers to 1+2.

binoidalcategories proper should obey your axiom in general. $\endgroup$