<div dir="ltr"><div><div><div><div><div><div>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:<br><br></div><font face="monospace"> foo : Group -> Group<br></font></div><font face="monospace"> foo G = ...<br></font></div><font face="monospace"> where</font><font face="monospace"><br></font></div></div><font face="monospace"> instance GS : GroupStr (foo G)<br></font></div><font face="monospace"> GS = ... <br></font></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 27, 2014 at 12:01 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 2014-11-27 11:54 GMT+01:00 Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
><br>
><br>
> On Thu, Nov 27, 2014 at 10:16 AM, Guillaume Brunerie<br>
> <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> wrote:<br>
>><br>
>> Le 26 nov. 2014 16:08, "Jesper Cockx" <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> a écrit :<br>
>><br>
>> > - There is a way to make sense of having Type and Group as the return<br>
>> > type of a function: "f : ... -> Type" just stands for "f : ... -> Set _",<br>
>> > and "g : ... -> Group0" stands for "g : ... -> Set", but using g also brings<br>
>> > a term of type "GroupStr (g ...)" into scope for instance resolution. Then<br>
>> > you could make (A : Set) a synonym for {i : Level} (A : Set i) instead of (A<br>
>> > : Set0), so that functions that look non-level-polymorphic can actually be<br>
>> > used at any level.<br>
>><br>
>> That makes sense for postulates for instance, but not for function<br>
>> definitions, if you want to define a function of type Group -> Group, then<br>
>> you have to provide the group structure on the result and it might be<br>
>> nontrivial.<br>
><br>
> Well, if you don't want to provide the group structure on the result, you<br>
> should write Group -> Set (or Group -> Type) instead. I would imagine you<br>
> write something like<br>
><br>
> private<br>
> fooCarrier : Type -> Type<br>
> fooCarrier G = ...<br>
><br>
> instance<br>
> fooGroupStr : (G : Group) -> GroupStr (fooCarrier G)<br>
> fooGroupStr G = ...<br>
><br>
> foo : Group -> Group<br>
> foo G = fooCarrier G<br>
><br>
> And then Agda would get the group structure for "fooCarrier G" by instance<br>
> resolution.<br>
<br>
</div></div>Ok, but then I don’t see the point of defining foo at all. Everytime<br>
you want to use [foo G] you can just use [fooCarrier G] instead, no?<br>
(if you remove "private")<br>
</blockquote></div><br></div>