++) 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.