Add HasEquivs instance for MatrixCat

[Alizter]

In theories/Algebra/Rings/Matrix.v we have a definition of the category of matrices whose objects are natural numbers and morhpisms are matrices between those dimensions.

We should add a HasEquivs instance for MatrixCat. It should consist of the following:

• The type of equivalences will be invertible matrices. That is the subset of matrices which are invertible as ring elements. Theory about invertible ring elements can be found in theories/Algebra/Rings/Ring.v. A sigma type should be enough.
• The type of "is equivalence" predicates will be if a given matrix is invertible.
• The other fields of HasEquivs can then be constructed in a straightforward manner using projections and constructors.

[ndcroos]

Hi, I am still busy working on the other issues, but I'd like to work on this after these.