<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 27, 2014 at 10:16 AM, 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"><p dir="ltr">
Le 26 nov. 2014 16:08, "Jesper Cockx" <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> a écrit :<span></span></p><span><p dir="ltr">> - 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.</p>
</span><p dir="ltr">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.</p></blockquote></div>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<br><br></div><div class="gmail_extra"><span style="font-family:monospace"> private<br> fooCarrier : Type -> Type<br></span></div><div class="gmail_extra"><span style="font-family:monospace"> fooCarrier G = ...<br><br></span></div><div class="gmail_extra"><span style="font-family:monospace"> instance<br></span></div><div class="gmail_extra"><span style="font-family:monospace"> fooGroupStr : (G : Group) -> GroupStr (fooCarrier G)</span><br></div><div class="gmail_extra"><font face="monospace"> fooGroupStr G = ...<br><br></font></div><div class="gmail_extra"><font face="monospace"> foo : Group -> Group<br></font></div><div class="gmail_extra"><font face="monospace"> foo G = fooCarrier G<br><br></font></div><div class="gmail_extra"><font face="monospace"><span style="font-family:arial,helvetica,sans-serif">And then Agda woul</span>d<font face="arial,helvetica,sans-serif"> get the group structure for "fooCarrier G" by instance resolution</font>.<br></font></div></div>