EmbeddingLike coe

Stream: mathlib4

[Felix Weilacher]

Is it intentional that providing a type F with an instance of EmbeddingLike F A B does not provide a coercion from F to Embedding A B?

(Instead, you get a coercion to functions and a proof that they are injective)

Is it for diamond reasons?

[Edward van de Meent]

i think that this might be because in most cases, the API for (f : A -> B) (hinj : Injective f) is (possibly a lot) better? i hardly ever have come across uses of Embedding, to be honest...

[Yury G. Kudryashov]

No diamond reasons, just a hole in the API. We have these functions for many other similar classes.