Full embeddings are embeddings

[TashiWalde]

In #155, Benno introduced the notion of a full embedding of types (aka. fully faithful functors) .
This is a map f : X --> Y which induces equivalences hom X x y -> hom Y (f x) (f y) for all x,y : X.

As the name suggests, these maps are embeddings; at least when X and Y are Rezk types.

The proof roughly goes as follows:

• we know that the map Iso X x y -> hom X x y is an embedding, and similarly for Y (f x) (f y). (This is basically is-prop-is-iso-arrow)
• using the same argument as in 1-category theory, one uses the fully faithfulness to deduce, for each g : hom X x y a logical equivalence between is-iso g and is-iso (f g)
• this logical equivalence shows that the assumed equivalence hom X x y -> hom Y (f x) (f y) restricts to an equivalence Iso X x y -> Iso Y (f x) (f y) along the respective embeddings
• using the Rezk axiom, this yields that x = y -> (f x) = (f y) is an equivalence, thus proving that f is an embedding.

This might be a good self-contained project for a motivated would-be contributor.