[Agda] Telescope syntax

Nils Anders Danielsson nad at cse.gu.se
Fri Nov 28 23:59:33 CET 2014


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


More information about the Agda mailing list