$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Remark Let $\operatorname{\mathcal{C}}$ be a nonunital monoidal category. Suppose we are given objects $\mathbf{1}, \mathbf{1}' \in \operatorname{\mathcal{C}}$ together with isomorphisms

\[ \upsilon : \mathbf{1} \otimes \mathbf{1} \simeq \mathbf{1} \quad \quad \upsilon ': \mathbf{1}' \otimes \mathbf{1}' \simeq \mathbf{1}'. \]

To carry out the proof of Proposition, it is sufficient to assume that the functors

\[ \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\quad \quad X \mapsto \mathbf{1} \otimes X \]
\[ \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\quad \quad X \mapsto X \otimes \mathbf{1}' \]

are fully faithful: the first assumption is sufficient to construct the left unit constraints of Construction, and the second is used at the end of the proof. This can be regarded as a categorical analogue of the observation that if a nonunital monoid admits a left unit $e$ and a right unit $e'$, then we must have $e = e'$.