Are all binoidal categories (in the literature) actually strict?

Question

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.

Answer 1

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.

P.S.: Who is the mathematician displayed in your avatar/icon?