[Agda] Telescope syntax

[Nils Anders Danielsson]

On 2014-11-27 12:07, Andreas Abel wrote:
> It seems like you want first-class Sigma/record types with exactly one
> visible component (all others hidden/instance) and further some way to
> abbreviate it.  In this case, one could just write e.g.
>
>    telescope Group = (G : Set) {{IG : IsGroup G}}
>    telescope Type  = {i : Level} (_ : Set i)
>
> since there is exactly one visible component.

Guillaume, would implicit coercions (of some kind) solve your problem?

-- 
/NAD