[Agda] Associativity and Heterogeneous Equality

[Sergei Meshveliani]

On Sun, 2015-06-07 at 16:33 +0200, Marco Vassena wrote:
> 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.
> [..]

This is because the types are different. 
We can consider defining a pair of mutually inverse bijections

  hList-assocMap1 : HList (xs ++ (ys ++ zs)) -> 
                    HList ((xs ++ ys) ++ zs) 

  hList-assocMap2 : HList ((xs ++ ys) ++ zs)) -> 
                    HList (xs ++ (ys ++ zs)) 

and applying   xs \equiv (hList-assocMap1 ys)  
instead of     xs \equiv ys.

Regards,

------
Sergei