We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

翻译：我们刻画了线性逻辑乘加片段（MALL）中的类型同构，从而扩展了Balat与Di Cosmo关于乘性片段的结果，将其应用于具有有限积的*-自伴范畴。这导出了一个涉及分配律与消去律的更为丰富的等式理论。通过采用Hughes与Van Glabbeek引入的证明网语法，我们得到了无单位元情形下的结论。利用序列演算，结合对消去规则及规则交换性的研究，我们将结果推广至包含所有单位元的完整MALL系统。