[Agda] Telescope syntax

[Jesper Cockx]

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 = ...

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")
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141127/17ecf7e4/attachment.html