Add laws for InjectK typeclass

[andyscott]

InjectK has (tentatively) been converted to a typeclass and deserves the full treatment by introducing laws.

See #1642

[andyscott]

I'd assign myself to this, but I can't! So feel free to assign me.