Re: bilax_monoidal_functors?