  If premise combination is not commutative, then residuation can go in two ways. In addition to the residuation condition giving the behaviour of \(\rightarrow\), we may wish to define a new arrow \(\leftarrow\) as follows: