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

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.

• The HoTT book defines dependent equality over a path $p : A = B$ as $a = \mathsf{transp}_p b$. It then proves that transporting either side results in isomorphic types.
– Trebor
Feb 10, 2022 at 6:07
• More specifically, you prove something like ++-unit : (xs : Vec A n) → Σ[ p ∈ n + 0 ≡ n ] subst (Vec A) p (xs ++ []) ≡ xs in Agda. Feb 10, 2022 at 7:57
• I doubt there's a single correct answer. I'd be tempted to use an analogue of Data.Fin.cast, but this is merely a temptation. Feb 10, 2022 at 13:59

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