Makes me think of another mnemonic for subtyping: S <: T when id : S -> T is well-typed.
"Our language comes with a subtyping relation T <: S that tells when it is safe to use elements of T in a context that expects elements of S."
@lyxia It's always safe to use elements of one type in contexts that expect elements of another one… except when it's not…
Seriously, though, #Coq's :> offers to save a few keystrokes, by not specifying the field of the structure, at the expense of harder debugging, when the types aren't quite coercible…
Sure I can get the aesthetics of identifying an algebraic structure with it's carrier, as is commonly done in informal math, but still, it's a fragile mechanism, IMO.
This is talking about the theory of subtyping though, not Coq coercions.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !