[Agda] Telescope syntax

[Jesper Cockx]

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