In a category with biproducts, morphisms between finite biproducts are naturally encoded in terms of arrays of morphisms between the direct summands of the objects. The natural operations on morphisms (addition, composition) correspond to the usual matrix calculus operations on these arrays.
For the special case that Vect this reproduces the standard matrix calculus of linear algebra.
In matrix calculus one therefore writes
With this notation one has the following rules for computation:
As can be seen in the above formulas, particularly for matrix multiplication, this is a context is which the Einstein summation convention can be used, with a distinction drawn between upper and lower indices. Then repeated indices (in formulas with general applicability) will always appear once upper and once lower, summed over. However, this convention can apply only to the morphisms, not to the objects.
If the category is in addition a dagger category with an obvious compatibility condition between the dagger operation and the biproduct structure, then the usual rules of computation for matrices over complex numbers have analogs in .
Here the distinction between upper and lower indices cannot be maintained, although it is still true that repeated indices will be summed in formulas with general applicability.
Formalization in terms of dependent linear type theory is in