7
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – Trebor
    Commented Feb 10, 2022 at 6:07
  • $\begingroup$ More specifically, you prove something like ++-unit : (xs : Vec A n) → Σ[ p ∈ n + 0 ≡ n ] subst (Vec A) p (xs ++ []) ≡ xs in Agda. $\endgroup$
    – L.-T. Chen
    Commented Feb 10, 2022 at 7:57
  • $\begingroup$ 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. $\endgroup$
    – James Wood
    Commented Feb 10, 2022 at 13:59

1 Answer 1

5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.