# What is the categorical semantics of subtyping?

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?