The trick of that article is noting that Rúnar translates "S is a subtype of T" to "S => T", e.g. subtyping implies coercion. This is the first part of subtypin

The trick of that article is noting that Rúnar translates "S is a subtype of T" to "S => T", e.g. subtyping implies coercion. This is the first part of subtyping. The second part is that we must have that definitions of Q[S] for any Q must follow naturally from definitions of Q[T]. So let's say that Apple is a subtype of Fruit. That means that there exists a natural coercion function f : Apple => Fruit. It also means that if we have a predicate Delicious that we define for both Fruit and Apple then the answer Delicious[Apple] must be exactly Delicious[Fruit].comap(f). If they don't align then your coercion function is somehow wrong and not implementing subtyping properly.