[Agda] heterogeneous lists with universes

[J.Burton at brighton.ac.uk]

Sorry, double colons lost in the email. That should be:
[...]
> I want lists of them like so:
> 
> (MkL 'A'   MkL 'B'   []) : (L 'A' ::: L 'B' ::: Nil)

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

> 
> Or if I redefine   to apply MkL itself:
> 
> ('A'   'B'   []) : (L 'A' ::: L 'B' ::: Nil)
> 

('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)
> 
> -----------------------------
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda