Matrix

A $m\times n$ matrix with values in a type $A$ is a function $[m]\times[n]\to A$.

As Polynomial Functors

A $m\times n$ matrix of types can be represented as a Linear Polynomial Functor

• $[n]\leftarrow X\xrightarrow{mathrm{id}{ifx..lse\par i}}X\to[m]$

Typesetting

There are a couple of latex environments for typesetting matricies; the main two are pmatrix and bmatrix.