[Agda] Associativity of vector concatenation

[Dan Licata]

nice example! 

> The idea is very similar to using heterogeneous equality, as you will
> see.

More precisely, I think that heterogeneous equality (a:A) == (b:B) is equivalent to either 
(writing PathOver F p a b for your a ≡[ p ] b to make the type family explicit,
and writing == for the homogeneous identity type)

(p : A == B) -> PathOver (\X -> X) p a b

or 

(p : A == B) * PathOver (\X -> X) p a b

depending on what the rules for the (a:A) == (b:B) type are
(there was a thread a few years ago about whether this should imply A==B or require A==B, but I can’t find it right now).  

-Dan