[Agda] Heterogeneous Vectors

[Simon Foster]

Hi,

I'm trying to come up with a flexible implementation of a  
heterogeneous vector, but I'm encountering some problems with universe  
levels. At the moment I am using the following representation:

data HVec {a} : (n : ℕ) → (As : Vec (Set a) n) → Set (suc a) where
   hnil  : HVec zero []
   hcons : ∀ {A : Set a} {k} {As} → A → HVec k As → HVec (suc  
k) (A ∷ As)

This works quite well, except when I want to use it in an inductive  
datatype (such as a typed n-ary expressions), because this leads to a  
data-type whose universe index increases depending on the data-type  
depth. My question is, is there another way of representing  
heterogeneous vectors which doesn't require the type to have a higher  
set index than its encapsulated types? I can achieve a similar effect  
using functions, e.g.

HVec : ∀ {a} → (n : ℕ) → (As : Vec (Set a) n) → Set a
HVec n As = λ (i : Fin n) → lookup i As

But such a representation is very cumbersome to use. Is there a better  
way using an inductive datatype?

Thanks,

-Si.