[Agda] Telescope syntax

[Guillaume Brunerie]

On 2014-11-27 12:15 GMT+01:00 Jesper Cockx <Jesper at sikanda.be> wrote:
> Hm, I guess so. It just seems nicer to have "foo : Group -> Group" in a
> library instead of "foo : Group -> Set" and having to look whether the
> library also exports a group structure for it. A nicer way to write it would
> be something like this:
>
>   foo : Group -> Group
>   foo G = ...
>     where
>       instance GS : GroupStr (foo G)
>       GS = ...

That makes much more sense indeed.
Although I’m not sure how often that would be used, for instance for
the cartesian product I don’t think you want a "cartesian product of
groups" function, I’d rather prove that if G and H have group
structures, then so do G × H, but also that if A and B have ring
structures, then so do A × B, if X and Y are pointed, then so is X ×
Y, and so on (all of that for × the cartesian product of types).
But maybe it could be nice in some cases.

> On Thu, Nov 27, 2014 at 12:01 PM, Guillaume Brunerie
> <guillaume.brunerie at gmail.com> wrote:
>>
>> 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")
>
>