Qual é a semântica categórica da subtipagem?

A partir de Curry-Howard-Lambek, houve uma boa trindade de teorias de tipos, lógicas e categorias. Estou curioso sobre a semântica categórica que você obtém ao adicionar subtipos (coercitivos) a uma teoria de tipos - parece que isso não foi muito explorado, se é que realmente foi.

Em geral, adicionar subtipagem coercitiva a uma teoria de tipos não arruina suas propriedades metateóricas, como forte normalização, portanto sua semântica categórica deve ser algo de interesse real, eu acho!

Semântica, uma coerção é apenas um morfismo , que é adicionado à interpretação dos termos nos pontos apropriados. O problema básico que isso cria é a questão da coerência : você tem a garantia de que um termo terá um significado único, uma vez que o mesmo termo pode potencialmente ter coerções ocultas em muitos locais possíveis no programa?$c : A \leq B$$c : A \to B$

Um dos primeiros tratamentos desta edição foi o artigo de John Reynolds, de 1980, Usando a teoria da categoria para projetar conversões implícitas e operadores genéricos , que mostra como você pode fornecer uma semântica categórica a um sistema de coerções e usá-lo para garantir que seja coerente.

Se você está interessado em subtipagem coercitiva para teorias de tipos ricos (por exemplo, dependentes), então Zhaohui Luo é o principal candidato .