The Stacks project

I suppose what you really want in this definition is whatever is needed for MacLane's coherence. It might be worth mentioning that the other minimal coherence conditions: $(1\otimes X)\otimes Y\to X\otimes Y$ equals $(1\otimes X)\otimes Y\to 1\otimes (X\otimes Y)\to X\otimes Y$, $(X\otimes Y)\otimes 1\to X\otimes Y$ equals $(X\otimes Y)\otimes 1\to X\otimes (Y\otimes 1)\to X\otimes Y$, left unitor $1\otimes 1\to 1$ equals right unitor $1\otimes 1\to 1$, $(1\otimes X)\otimes 1\to X\otimes 1\to X$ equals $(1\otimes X)\otimes 1\to 1\otimes X\to X$, and so on are consequence of the definition. I think the first three are not immediate, this proof is written in ncatlab, apparently it's due to Kelly https://ncatlab.org/nlab/show/monoidal+category. The others follow from naturality of unitors and associator, and one of them is the pentagon identity. In the case of symmetric monoidal categories you also want $1\otimes X\to X$ equals $1\otimes X\to X\otimes 1\to X$ . I believe a similar proof as the Kelly one works here using the hexagon:

$$\matrix{ X \otimes (1\otimes 1)) & \to & (1\otimes 1)\otimes (X) \cr \downarrow && \downarrow \cr 1\otimes X & \to & X \otimes 1 }$$

conmutes by naturality of conmutator

Up to associativity (as in MacLane Coherence) $X\otimes 1\otimes 1\to 1\otimes 1\otimes X$ equals $X\otimes 1\otimes 1\to 1\otimes X\otimes 1\to 1\otimes 1\otimes X$ (this is the Hexagon).

By naturality of the unitor $$\matrix{ 1 \otimes X\otimes 1 & \to & 1\otimes 1\otimes X \cr \downarrow && \downarrow \cr X\otimes 1 & \to & 1 \otimes X }$$

conmutes

As the arrows are isomorphisms this implies $X\otimes 1\otimes 1\to 1\otimes X\otimes 1\to X\otimes 1$ coincides with $X\otimes 1\otimes 1\to X\otimes 1$. As $(.) \otimes 1$ is an equivalence conclude that $X\otimes 1\to 1\otimes X\to X$ coincides with $X\otimes 1\to 1$.

These three conditions for monoidal categories and this extra condition for symmetric monoidal category I guess are straghtforward verifications in applications, so it's also possible to just add it to the definition instead.

OK, I don't want to change the definitions if that is not necessary (and it sound like it isn't). We'll add the additional properties (in the Stacks project) if we use them. If that has happened silently, then someone will point it out and we'll add it here.

I think this is used silently often. Before this definition: "en equivalent definition would be an object 1 and an isomorphism $1:1\otimes 1\to 1$" seems to be use that left unitor= right unitor.

tag 0FFQ, I believe the omitted proof that the maps are inverse of each other uses the two coherences for monoid categories. The omitted proof is that $Z'\to Z'\otimes X\otimes Y\to Z\otimes Y\otimes X\otimes Y\to Z\otimes Y$ equals $Z'\to Z\otimes Y$. The first two arrows equal (1) $Z'\to Z\otimes Y\to Z\otimes Y\otimes X\otimes Y$ by naturality, and (2) $Z\otimes Y\to Z\otimes Y\otimes X\otimes Y\to Z\otimes Y$ equals the identity by the definition of dual. The issue is that being a bit careful with the defining arrows one sees that the arrow $Z\otimes Y\to Z\otimes Y\otimes X\otimes Y$ in (1) is really: $Z\otimes Y\to (Z\otimes Y)\otimes 1\to (Z\otimes Y)\otimes (X\otimes Y)$ while the arrow in (2) is $Z\otimes Y\to Z\otimes (Y\otimes 1)\to Z\otimes (Y\otimes (X\otimes Y))$, so here you need the coherence $Z\otimes Y\to (Z\otimes Y)\otimes 1$ equal $Z\otimes Y\to Z\otimes (Y\otimes 1)\to (Z\otimes Y)\otimes 1$

The omitted proof of tag 0FN8 I believe uses the coherence I mentioned for symmetric categories.

OK, thanks for these comments! I agree that the original exposition (which will soon be updated) was a bit thin. I made some edits proving the equivalence of the two notions of units and then given some arguments proving enough so that MacLane's paper provides the coherence. I ran through the cases $(C, \phi)$, $(C, \phi, \mathbf{1})$, and $(C, \phi, \psi, \mathbf{1})$ in order which I think clarifies things. At the moment an exposition of MacLane's arguments is omitted. See this, this, and this.