On Thu, Jul 10, 2014 at 9:37 PM, Jan Stolarek <jan.stolarek@p.lodz.pl> wrote:

1. Standard injective type family (all parameters uniquely determined by the RHS):
injective type family F a b c | a b c

<snip>

2. Type family injective only in some parameters (ie. only some parameters uniquely determined by the RHS):
injective type family G a b c | a b

English is not my mother tongue. Perhaps you mean: 'the image under the type function is uniquely determined by the parameters on the right of the vertical bar'?

As they stand, the sentences confuse which determines what.

Such confusion has a way of squirreling into official documentation.

-- Kim-Ee