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.

For easy reference, here are the statements in question:

* "Standard injective type family (all parameters uniquely determined by the RHS)"

* "Type family injective only in some parameters (ie. only some parameters uniquely determined by the RHS):"

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.

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!

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?

Imprecise language not only trips up experts, it also sets up insurmountable barriers for outsiders. We can do much better here.