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.
++-unit : (xs : Vec A n) → Σ[ p ∈ n + 0 ≡ n ] subst (Vec A) p (xs ++ []) ≡ xs
in Agda. $\endgroup$Data.Fin.cast
, but this is merely a temptation. $\endgroup$