[Agda] Associativity and Heterogeneous Equality

[Marco Vassena]

Given an heterogeneous list data-type:

data HList : List Set -> Set₁ where
  [] : HList []
  _∷_ : ∀ {xs x} -> x -> (ts : HList xs) -> HList (x ∷ xs)

I have defined the append function:
_+++_ : ∀ {xs ys} -> HList xs -> HList ys -> HList (xs ++ ys)
[] +++ bs = bs
(t ∷ as) +++ bs = t ∷ (as +++ bs)

Now I want to prove that _+++_ is associative: a +++ b +++ c = (a +++ b) +++ c.

I could not state this lemma using propositional equality, because _+++_
appends the list of types using _++_ : 
a +++ b +++ c :: HList (xs ++ ys ++ zs)
(a +++ b) +++ c :: HList ((xs ++ ys) ++ zs) 

the two indexes are not considered equal, leading to different types, preventing the use of propositional equality.
In order to solve this I should use associativity of _++_ in the signature itself, but I could not find any
way to do that.

I tried then to use heterogeneous equality.

assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList zs) -> a +++ b +++ c ≅ (a +++ b) +++ c
assoc-+++ [] b c = refl
assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c = H.cong (_∷_ x) (assoc-+++ a b c)  -- (xs +++ ys) != xs (needs associativity)

The term (assoc-+++ a b c) is ill-typed because of the associativity of _++_ .
At this point I have tried to use firstly associativity of _++_, but this failed with an error about the generated with function being ill-typed.

Is there a way to prove associativity of _+++_ ?

I have attached a file with this problem.

All the best,
Marco

-------------- next part --------------
A non-text attachment was scrubbed...
Name: HAssociativity.agda
Type: application/octet-stream
Size: 1759 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150607/e2d455e1/HAssociativity.obj
-------------- next part --------------