<div dir="ltr"><div><div><div><div><div><div>Hm, I guess so. It just seems nicer to have &quot;foo : Group -&gt; Group&quot; in a library instead of &quot;foo : Group -&gt; Set&quot; 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 -&gt; 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">&lt;<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>&gt;</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 &lt;<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>&gt; wrote:<br>
&gt;<br>
&gt;<br>
&gt; On Thu, Nov 27, 2014 at 10:16 AM, Guillaume Brunerie<br>
&gt; &lt;<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; Le 26 nov. 2014 16:08, &quot;Jesper Cockx&quot; &lt;<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>&gt; a écrit :<br>
&gt;&gt;<br>
&gt;&gt; &gt; - There is a way to make sense of having Type and Group as the return<br>
&gt;&gt; &gt; type of a function: &quot;f : ... -&gt; Type&quot; just stands for &quot;f : ... -&gt; Set _&quot;,<br>
&gt;&gt; &gt; and &quot;g : ... -&gt; Group0&quot; stands for &quot;g : ... -&gt; Set&quot;, but using g also brings<br>
&gt;&gt; &gt; a term of type &quot;GroupStr (g ...)&quot; into scope for instance resolution. Then<br>
&gt;&gt; &gt; you could make (A : Set) a synonym for {i : Level} (A : Set i) instead of (A<br>
&gt;&gt; &gt; : Set0), so that functions that look non-level-polymorphic can actually be<br>
&gt;&gt; &gt; used at any level.<br>
&gt;&gt;<br>
&gt;&gt; That makes sense for postulates for instance, but not for function<br>
&gt;&gt; definitions, if you want to define a function of type Group -&gt; Group, then<br>
&gt;&gt; you have to provide the group structure on the result and it might be<br>
&gt;&gt; nontrivial.<br>
&gt;<br>
&gt; Well, if you don&#39;t want to provide the group structure on the result, you<br>
&gt; should write Group -&gt; Set (or Group -&gt; Type) instead. I would imagine you<br>
&gt; write something like<br>
&gt;<br>
&gt;     private<br>
&gt;       fooCarrier : Type -&gt; Type<br>
&gt;       fooCarrier G = ...<br>
&gt;<br>
&gt;       instance<br>
&gt;         fooGroupStr : (G : Group) -&gt; GroupStr (fooCarrier G)<br>
&gt;         fooGroupStr G = ...<br>
&gt;<br>
&gt;     foo : Group -&gt; Group<br>
&gt;     foo G = fooCarrier G<br>
&gt;<br>
&gt; And then Agda would get the group structure for &quot;fooCarrier G&quot; by instance<br>
&gt; 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 &quot;private&quot;)<br>
</blockquote></div><br></div>