How to state and prove the associativity of append of sized vectors with homogeneous equality?

Question

Append (denoted ++) for sized vectors is obviously associative, i.e. a ++ (b ++ c) = (a ++ b) ++ c for a : Vec A n, b : Vec A m, c : Vec A o, assuming = is the intensional equality type former.

Now, if we define = as the heterogeneous equality, the statement and the proof will be straightforward, but heterogeneous equality is incompatible with univalence. With homogeneous equality, the expression a ++ (b ++ c) = (a ++ b) ++ c is no longer well typed because the LHS has type Vec A (n + (m + o)) and the RHS has type Vec A ((n + m) + o). These two types are only equal up to intensional equality. How can I, in this case, state the theorem and prove it?

In the standard library of Agda, this is only proved in a with-K module using heterogeneous equality. In cubical Agda library, there's a beautiful statement (like PathP (λ i -> +-assoc i) (a ++ (b ++ c)) ((a ++ b) ++ c)), but PathP is not available w/o cubical features. I'm unsure about other systems.

Answer 1

The equality has to be a "dependent equality" over the associativity of natural numbers n + (m + o) = (n + m) + o.

Some libraries for univalent mathematics have a primitive notion of "dependent equality type"; in plain dependent type theory it can be defined inductively with "dependent reflexivity" as its only generator, while in cubical type theories it is a basic notion. Other libraries identify it with a particular homogeneous equality type obtained by transporting the LHS across the nat-associativity equality. There are several libraries for univalent mathematics in Agda, and I don't know which of them you're using or what its approach to this definition may be.

Regardless, once you state the theorem in one of these ways, you should be able to prove it in essentially the same way that you prove associativity of unsized lists: destructing each vector in turn will at the same time destruct their lengths.