[Agda] Universe-Heterogeneous tree

[effectfully]

gallais, nice idea to use pattern synonyms machinery as a preprocessor.

Philipp Hausmann, `AST' and `el' emulate induction-recursion. Cool.
But it should be

el {ls A=> ls₁} (T , U) = Σ (el T) λ t → el (U t)

probably. And you also need to define `ast' of course.

> I'm also wondering if it's possible to use Level arguments in the AST
> language, but
> that seems quite tricky.

I don't think so. It's not possible in Agda to define

Setω-error : Σ Level λ α -> Set (suc α)
Setω-error = ?

for any sensible definition of `Σ' (I don't think this restriction is
natural, and not only I [1]).

[1] https://lists.chalmers.se/pipermail/agda/2013/005516.html