View source for GoI for MELL: the *-autonomous structure

== Weak distributivity ==
Similarly we get weak distributivity thanks to the operators:
: <math>\delta_1 = pppp^*q^* + ppqp^*q^*q^* + pqq^*q^*q^* + qpp^*p^*p^* + qqp q^*p^*p^* + qqq q^*p^*</math> and
: <math>\delta_2 = ppp^*p^*q^* + pqpq^*p^*q^* + pqqq^*q^* + qppp^*p^* + qpqp^*q^*p^* + qqq^*q^*p^*</math>.

Given three types <math>A</math>, <math>B</math> and <math>C</math> then one can show that:
: <math>\delta_1</math> has type <math>((A\limp B)\tens C)\limp A\limp (B\tens C)</math> and
: <math>\delta_2</math> has type <math>(A\tens(B\limp C))\limp (A\limp B)\limp C</math>.