[Agda] Associativity of vector concatenation

[Martin Escardo]

Often people mention the formulation and proof of associativity of
vector concatenation as something tricky.

The problem, of course, is that for vectors xs, ys, and zs, the
concatenations

    xs ++ (ys ++ zs)    of length l + (m + n)

and

    (xs ++ ys) ++ zs    of length (l + m) + n

belong to the different (but isomorphic) types

    Vec X  (l + (m + n)) and Vec X ((l + m) + n).

One approach considers heterogeneous equality, which is a notion of
equality that allows to compare elements of different types. A
limitation of this equality is that its elimination rule implies the K
axiom (any two proofs of equality are equal), which is incompatible
with univalent type theory as in the HoTT Book or as in Cubical Type
Theory, which are type theories some people wish to either use or at
least be compatible with.

Not only can we be compatible with univalent type theory, but also
we can learn from it (even without using univalence or other features that
don't belong to Martin-Loef Type Theory as represented by Agda).

I would like to advertise this here, as the ideas are of general use,
even if one is not interested in HoTT, and hopefully intuitive and
natural too.

Given a type X and a type family F:X->Set, suppose we have x,y:X,
p:x≡y and a : F x and b : F y. Even though x and y are equal, the
types F x and F y are not the same (they are equal under univalence,
but we don't want to use this). So can't compare a and b for equality.

But we can define a notion of equality between the types F x and F y,
dependent on p:x≡y,

    a ≡[ p ] b,

by

    a ≡[ refl ] b   =   a ≡ b.

In particular, we get

_≡[_]_ : ∀ {X} {m n} → Vec X m → m ≡ n → Vec X n → Set
xs ≡[ refl ] ys = xs ≡ ys

Then vector associativity becomes

++-assoc : ∀ {X : Set} l m n (xs : Vec X l) (ys : Vec X m) (zs : Vec X n)
        → xs ++ (ys ++ zs)  ≡[ +-assoc l m n ]  (xs ++ ys) ++ zs

where

+-assoc : ∀ l m n → l + (m + n) ≡ (l + m) + n.

Its proof is the same as that of associativity of list concatenation
(where the problem discussed in this message doesn't arise), but
taking care of the extra subscript p for dependent equality, in a way
that doesn't become disruptive or require new ideas, as shown here:

http://www.cs.bham.ac.uk/~mhe/agda/VecConcatAssoc.html

The idea is very similar to using heterogeneous equality, as you will
see.

Anyway, I wanted to advertise this idea coming from univalent type
theory, and try to convince you of its simplicity and naturality and
usefulness.

Martin