[Agda] Associativity of vector concatenation

[Martin Escardo]

On 28/10/16 15:59, Dan Licata wrote:
>> The idea is very similar to using heterogeneous equality, as you will
>> see.
>
> More precisely, I think that heterogeneous equality (a:A) == (b:B) is equivalent to either
> (writing PathOver F p a b for your a ≡[ p ] b to make the type family explicit,
> and writing == for the homogeneous identity type)
>
> (p : A == B) -> PathOver (\X -> X) p a b
>
> or
>
> (p : A == B) * PathOver (\X -> X) p a b
>
> depending on what the rules for the (a:A) == (b:B) type are
> (there was a thread a few years ago about whether this should imply A==B or require A==B, but I can’t find it right now).

I'd also like to understand this, and also the claim that the 
elimination principle for heterogeneous equality implies K.

Martin