Re: bilax_monoidal_functors