Naive injectivity implies isEmbedding even if only B is a set

[MatthiasHu]

This PR removes an unnecessary assumption from injEmbedding in Cubical.Functions.Embedding. The naive definition of injectivity, ∀{w x} → f w ≡ f x → w ≡ x, is already sufficient for f to be an embedding if B is a set, we don't need that A is a set.

I also deleted retractableIntoSet→isEmbedding, because it shows the same thing under the stronger assumption that f has a retract.

[MatthiasHu]

Wait a second, every function that admits a retract is an embedding, right? So retractableIntoSet→isEmbedding had an unnecessary isSet assumption too...

[MatthiasHu]

No, I was wrong: for example, Unit -> S^1 admits a retract but is not an embedding.