initial segment coercions

Stream: general

[Violeta Hernández]

There are currently a lot of coercions in the initial segment API. There's a coercion from principal segments to initial segments, a coercion from initial segments to relation embeddings, and a coercion from principal segments to relation embeddings.

[Violeta Hernández]

These don't sit quite right with me - I don't think we use casts in this way elsewhere in mathlib. We don't even have more obvious coercions, like order isomorphisms to relation isomorphisms.

[Violeta Hernández]

And we don't tend to have compositions of coercions as coercions, do we?

[Violeta Hernández]

Should I refactor these out in favor of explicit functions?