Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type theory -- it seems like this has not been explored very much, if at all.
In general, adding coercive subtyping to a type theory does not ruin its meta-theoretic properties such as strong normalization, so its categorical semantics should be something of actual interest, I think!
Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the program?
One of the first treatments of this issue was John Reynolds' 1980 paper, Using Category Theory to Design Implicit Conversions and Generic Operators, which shows how you can give a categorical semantics to a system of coercions and use it to ensure that it is coherent.
If you're interested in coercive subtyping for rich (e.g., dependent) type theories, then Zhaohui Luo is the go-to guy.
