<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jul 11, 2014 at 3:27 AM, Roman Cheplyaka <span dir="ltr"><<a href="mailto:roma@ro-che.info" target="_blank">roma@ro-che.info</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":yk" class="" style="overflow:hidden">The result of any function is always determined by that function's parameters.<br>


<br>
Injectivity means that the *parameters* are determined by the result.<br>
<br>
So I think Jan's definition is correct.</div></blockquote></div><br></div><div class="gmail_extra">What's correct could still be confusing. Now that you brought it up, I no longer know what "RHS" in OP means! It could be (1) the result. Or (2) the right of the vertical bar.<br>

<br></div><div class="gmail_extra">For easy reference, here are the statements in question:<br><br>* "Standard injective type family (all parameters uniquely determined by the RHS)"<br><br>* "Type family injective only in some parameters (ie. only some parameters uniquely determined by the RHS):"<br>

</div><div class="gmail_extra"><br></div><div class="gmail_extra">So when you say "arguments always determine result", one has to pause and think about what that means in the presence of multiple arguments as we have here. Because that doesn't hold when only some arguments are applied.<br>

<br>Also, note the usage of the expression "uniquely determined" in OP. When a single-argument function is injective, we say that the argument 'uniquely determines' (as opposed to just determine) the result. But note how it appears flipped in OP!<br>

</div><div class="gmail_extra"><br></div><div class="gmail_extra">Finally, let's look at how the verb 'determine' is used. When defining a type family case-by-case, one works from arguments to the result determined by the arguments. But saying "Injectivity means that the *parameters* are determined by the result" raises the specter of the inverse function. Suddenly, the arrow of work gets flipped in reverse. Doesn't that only contribute to cognitive noise?<br>

<br></div><div class="gmail_extra">Imprecise language not only trips up experts, it also sets up insurmountable barriers for outsiders. We can do much better here.<br></div><div class="gmail_extra"><br clear="all"><div>-- Kim-Ee</div>


</div></div>