[Agda] Telescope syntax

[Guillaume Brunerie]

On 2014-11-28 23:59 GMT+01:00 Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 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?

I guess so, but I thought implicit coercions were unwanted in Agda.
That telescope synonym syntax looks less problematic than implicit coercions.