Definition of embedding

[mikeshulman]

@martinescardo has pointed out that the proof of 4.6.3 essentially uses the equivalence of embeddings with (-1)-truncated maps (i.e. those whose fibers are hprops), which is not mentioned until section 7.6, and that that equivalence may be conceptually helpful. We could add that equivalence to section 4.6 as a Lemma 4.6.2½ (assuming #601).

It might also be good to add a bit of explanation of why the definition of embedding given is the correct generalization of injectivity to non-sets, both with and without reference to 4.6.2½.

[JasonGross]

For ease of reference, the relevant discussion thread is here.