Comment by types_vs_sets

Inclusions are a form of isomorphism. In the more common developments of elementary arithmetic, Q is constructed from Z, and in particular the subset of integral rational numbers are technically a different ring from Z. The conversion Z \to Q in particular is an isomorphism from Z to that subset.

Type conversions in every day programming languages though sometimes not only fail to be surjective, they can also fail to be injective, for example int32 -> float32.

type-conversions and "implicit isomorphisms" differ because the former does not need to be invertible, but they agree in that they are implicit maps, that are often performed without thought by the user. So I think that the type-conversions analogy is pretty good in that it captures the idea that implicit conversions, when composed in different ways from A to B, can arrive at various values, even if each stage along the way the choices seemed natural.