The tensor product is given by a composite $\mathcal M/m \times \mathcal M/m \to \mathcal M^2/(m, m) \to \mathcal M/(m \otimes m) \to \mathcal M/m$, where the last functor is the one you mention. However, it's not possible to express this in terms of the arrow category, because we need to only consider morphisms with certain codomains (e.g. $m$).

@cxandru: could you clarify what you mean by the left base change? What are the domain and codomain of the functor?

What do you mean by "the type of the function might have to be "lifted" in order to match the type of the value it is applied to"? The Church numeral representation is an encoding for the untyped lambda calculus, so there are no types. Do you actually mean to refer to the polymorphic lambda calculus?

Commutative distributive laws are considered in Wolff's Commutative distributive laws, though they do not consider monoidal distributive laws.

Thanks! (I notice that you haven't accepted answers on many of your other questions: perhaps you had intended to accept them, but didn't realise about the checkmark. If so, it could be helpful to look through your past questions and accept the answers you intended to :) )

You can't upvote it, but you should be able to click the checkmark symbol to mark it as an accepted answer. (On other people's answers, you have both options, which are independent, but if you answer your own question, you only have the option to accept.)