[Agda] Telescope syntax

[Guillaume Brunerie]

On 2014-11-29 2:41 GMT+01:00 Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> 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.

Actually I don’t think it would work, for at least two reasons:

I guess that what we would do with implicit coercions is the
following: define [Type] and [Group0] as records, with the only
explicit projection being a coercion to [Set i] (or [Set]), and then
when we have an argument [(G : Group0)], [G] is really a Sigma type,
but we can still write [g : G] because the coercion will silently turn
it into a type.
The problems are:
- There is no way to define [Type] as a record, because it’s too big
and records have to live in some universe
- If we have [f : (G : Group0) -> Set] and an instance of a group
structure on [Int], then we want to be able to talk about [f Int]
(with instance search figuring out why [Int] is a group), but that
wouldn’t work here (unless maybe we have also an implicit coercion
from Set to Group0 taking an instance argument, but that sounds really
fishy)