[wyager]

> The injectivity assumption isn't unjustified

Strongly disagree.

(+2) 3 == (+1) 4 implies neither (+2) == (+1) nor 3 == 4. So Fst goes out the window.

(even 5) == (even 7) does not imply 5 == 7.

>type constructors are injective.

But type functions aren't, and that's what we want.

I agree that it's misleading to have type functions look like type constructors syntactically.

[catnaroek]

The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.