May's strictification conjecture for symmetric bimonoidal functors

A bipermutative category has additive and multiplicative symmetric permutative structures, with the multiplicative structure distributing over the additive one. A symmetric bimonoidal functor between bipermutative categories has compatible additive and multiplicative symmetric monoidal functor structures; it is strict when both structures preserve their tensor products and units strictly. May's conjecture. There is a functor on the bipermutative-category level that replaces symmetric bimonoidal functors by strict symmetric bimonoidal functors, in a sense analogous to May's strictification result for permutative categories. The conjecture is motivated by the multiplicative infinite loop space machine, which sends bipermutative categories to E_-ring spaces and spectra. The paper proves a weaker form beginning with multiplicatively strong symmetric bimonoidal functors, so the full strictification statement remains unresolved here.