[Agda] Telescope syntax

[Guillaume Brunerie]

On 2014-11-27 11:54 GMT+01:00 Jesper Cockx <Jesper at sikanda.be> wrote:
>
>
> On Thu, Nov 27, 2014 at 10:16 AM, Guillaume Brunerie
> <guillaume.brunerie at gmail.com> wrote:
>>
>> Le 26 nov. 2014 16:08, "Jesper Cockx" <Jesper at sikanda.be> a écrit :
>>
>> > - There is a way to make sense of having Type and Group as the return
>> > type of a function: "f : ... -> Type" just stands for "f : ... -> Set _",
>> > and "g : ... -> Group0" stands for "g : ... -> Set", but using g also brings
>> > a term of type "GroupStr (g ...)" into scope for instance resolution. Then
>> > you could make (A : Set) a synonym for {i : Level} (A : Set i) instead of (A
>> > : Set0), so that functions that look non-level-polymorphic can actually be
>> > used at any level.
>>
>> That makes sense for postulates for instance, but not for function
>> definitions, if you want to define a function of type Group -> Group, then
>> you have to provide the group structure on the result and it might be
>> nontrivial.
>
> Well, if you don't want to provide the group structure on the result, you
> should write Group -> Set (or Group -> Type) instead. I would imagine you
> write something like
>
>     private
>       fooCarrier : Type -> Type
>       fooCarrier G = ...
>
>       instance
>         fooGroupStr : (G : Group) -> GroupStr (fooCarrier G)
>         fooGroupStr G = ...
>
>     foo : Group -> Group
>     foo G = fooCarrier G
>
> And then Agda would get the group structure for "fooCarrier G" by instance
> resolution.

Ok, but then I don’t see the point of defining foo at all. Everytime
you want to use [foo G] you can just use [fooCarrier G] instead, no?
(if you remove "private")