Define matrices as functions about coq-hott

[Alizter]

@jdchristensen After thinking about this for a bit I actually don't think I know how to prove function extensionality for a finite domain. Even for the empty type, I don't know how to show two functions from the empty type are equal without assuming funext.

It would seem then if we wanted matrices to compute like this, then we will have to introduce funext everytime we prove something with an equality.

[jdchristensen]

It might still work out well, replacing = by == for statements about vectors and matrices. But it would be pretty radical, so I'm not sure if we want to go there. But so many operations on vectors are naturally expressed componentwise, and would then compute definitionally. map would just become postcomposition, and iterated map would definitionally commute with composition of functions. I guess a summary is that some = would have to be replaced by == (or use funext), while many others would be replaced by definitional equality.

I checked how the Coq standard library does it, and it uses the inductive family approach to defining vectors, which still has the property that nth doesn't definitionally commute with map.

The current approach isn't that bad, just requiring frequent use of rewrite entry_Build_Vector.