# Kerodon

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

Remark 2.1.2.22. 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 2.1.2.9, 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 2.1.2.17, 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'$.