Category of matrices valued in a frame (source code)

= Category of matrices valued in a frame
{title2=$\mathbf{Mat}(L)$}

For a <frame> $L$, an $L$-valued matrix $f:A\rightsquigarrow B$ is a function $A\times B\to L$. Composition is matrix multiplication with join as addition and meet as multiplication.