[Agda] Associativity of vector concatenation

[Roman]

I stopped using heterogeneous equality in Agda a while ago and never
missed it. First I used "heteroindexed equality":

data [_]_≅_ {ι α} {I : Set ι} {i} (A : I -> Set α) (x : A i) : ∀ {j}
-> A j -> Set where
  refl : [ A ] x ≅ x

It's nice, but you need a data type for handling `A : I -> Set α`, a
data type for handling `B : ∀ i -> A i -> Set β`, a data type for...
So instead I now use "telescopic equality", which for `Z : X → Set`
looks like this:

[_]_≅_ : ∀ {X : Set} {x y} → (Z : X → Set) → Z x → Z y → Set
[_]_≅_ {x = x} {y} Z a b = (x , a) ≡ (y , b)

And this generalizes pretty nicely: just one propositional equality
that cover all the cases.

With such equalities the proof of associativity of _++_ for vectors is
basically indistinguishable from the one that deals with lists:

gap : ∀ {A : Set} {C E : A → Set} {a b} {c : C a} {d : C b} {k : A -> A}
    → (f : ∀ {a} -> C a -> E (k a)) -> [ C ] c ≅ d → [ E ] f c ≅ f d
gap f refl = refl

++-assoc : ∀ {X l m n} (xs : Vec X l) (ys : Vec X m) (zs : Vec X n)
         → [ Vec X ] (xs ++ (ys ++ zs)) ≅ ((xs ++ ys) ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = gap (_ ∷_) (++-assoc xs ys zs)

A full snippet: http://lpaste.net/309877