¿Cuál es la semántica categórica del subtipo?

A partir de Curry-Howard-Lambek, ha habido una buena trinidad de teorías de tipos, lógicas y categorías. Tengo curiosidad por saber qué semántica categórica obtienes al agregar subtipos (coercitivos) a una teoría de tipos; parece que esto no se ha explorado mucho, si es que lo ha hecho.

En general, agregar un subtipo coercitivo a una teoría de tipos no arruina sus propiedades meta-teóricas, como una fuerte normalización, ¡creo que su semántica categórica debería ser algo de interés real!

Semánticamente, una coerción es solo un morfismo c : A → B , que se agrega a la interpretación de términos en los puntos apropiados. El problema básico que esto crea es el tema de la coherencia : ¿está garantizado que un término tendrá un significado único, dado que el mismo término puede tener coerciones ocultas en muchos lugares posibles del programa?$c : A \leq B$$c : A \to B$

Uno de los primeros tratamientos de este tema fue el artículo de 1980 de John Reynolds, Uso de la teoría de categorías para diseñar conversiones implícitas y operadores genéricos , que muestra cómo puede dar una semántica categórica a un sistema de coerción y usarlo para garantizar que sea coherente.

Si está interesado en el subtipo coercitivo para teorías de tipo rico (por ejemplo, dependiente), entonces Zhaohui Luo es el tipo ideal.