aboutsummaryrefslogtreecommitdiff
path: root/Data/Mat/Util.agda
AgeCommit message (Expand)Author
2026-03-26Add cocartesian structure to category of matricesJacques Comeaux
2026-03-19Add category of matrices over an arbitary rigJacques Comeaux