This morning’s crop of arxiv updates included a new version of Joachim Kock’s Elementary remarks on units in monoidal categories. Somehow I hadn’t noticed the earlier version; it’s a beautiful result, and it implies the lemma of mine that I mentioned in Paré’s observation.
The essential idea is that the unit of a monoidal category can be considered independently of the associativity. The usual way to define the unit is to ask for an object I together with natural isomorphisms
λA: I⊗A → A
ρA: A⊗I → A
such that the “triangle” diagram
Of course this definition doesn’t make sense without the associator α. What Kock does (he calls it a Saavedra unit) is just to ask for an object I equipped with an isomorphism
u: I⊗I → I
such that the functors I⊗- and –⊗I are full and faithful. This definition doesn’t require an associator, but if you have one then you can define natural isomorphisms λ and ρ that satisfy the triangle condition. It’s very simple: to define λA, for example, consider the composite
Since I⊗- is full and faithful, there is a unique (invertible) map λA: I⊗A → A for which I⊗λA is equal to this composite. The right-unit isomorphism ρ can be similarly defined, and the triangle axiom verified.
In particular, if you have arbitrary natural isomorphisms λ and ρ, you can take u to be either λI or ρI, and use Kock’s construction to find coherent unit isomorphisms, so as I said it subsumes my lemma.
Kock goes on to show how to define monoidal functors in terms of the Saavedra unit. For the definition of lax monoidal functor, I think he makes it a little bit more complicated than it needs to be. You can define a lax monoidal functor to be a functor F equipped with the usual data (a natural transformation mA,B: FA⊗FB → F(A⊗B) and a map mI: I → FI) subject to the usual associativity axiom, together with Kock’s condition that the diagram
must commute, and the additional requirement that, for every object A, the composites
should be invertible.
Of course, one benefit of the Saavedra unit approach is that it eliminates a coherence condition. The obvious question for anyone interested in higher categories is whether the idea can be extended to higher dimensions, where the savings would presumably be more substantial. Indeed Kock has done some work in this direction: see his paper Weak identity arrows in higher categories.
I haven’t read this one thoroughly, but it doesn’t seem to address one of the obvious questions, namely can one do something similar for monoidal bicategories? Update: it seems that there is something along these lines in Weak units and homotopy 3-types, with more promised in a forthcoming paper entitled Coherence for weak units.