[Agda] heterogeneous lists with universes

[J.Burton at brighton.ac.uk]

Hi, I want to make a heterogeneously-typed list whose type corresponds
to its data, i.e. whose value is fully captured by its type. So if I
have type wrapping a Char like this:

data L : (c : Char) -> Set where
  MkL : (c : Char) -> L c 

I want lists of them like so:

(MkL 'A' ∷ MkL 'B' ∷ []) : (L 'A' ::: L 'B' ::: Nil)

Or if I redefine ∷ to apply MkL itself:

('A' ∷ 'B' ∷ []) : (L 'A' ::: L 'B' ::: Nil)

I tried various ways to achieve this with universes and the example of
heterogeneous lists in the section on relational algebra in Oury et
al. "The Power of Pi". I think this is a red herring since those lists
carry types around as values rather than revealing them in type
signatures...

The broken code below might help explain what I'm trying to do.
Any suggestions as to how this is done?

Many thanks,

Jim

-----------------------------

data L : (c : Char) -> Set where
  MkL : (c : Char) -> L c 

{- I'll add to the types in U later -}
data U : Set where
  label    : Char -> U

el : U -> Set
el (label c) = L c

infixr 5 _:::_ _::_

data TCons : Set1 where
  Nil : TCons
  _:::_ : (t : Set) -> TCons -> TCons

data TSet (ts : TCons) : Set where
  []   : TSet Nil
  _::_ : {u : U}(el u) -> TSet ts -> TSet ((el u) ::: ts)

-----------------------------