Apakah semantik kategorikal dari subtyping?

Mulai dari Curry-Howard-Lambek, telah ada trinitas bagus dari teori tipe, logika, dan kategori. Saya ingin tahu apa yang Anda dapatkan semantik kategoris ketika Anda menambahkan (paksaan) subtipe ke teori jenis - sepertinya ini belum banyak dieksplorasi, jika sama sekali.

Secara umum, menambahkan subtyping koersif ke teori tipe tidak merusak sifat meta-teoretisnya seperti normalisasi yang kuat, jadi semantik kategorisnya seharusnya menjadi sesuatu yang menarik, menurut saya!

Secara semantik, paksaan hanyalah morfisme c : A → B , yang ditambahkan pada interpretasi istilah pada titik yang tepat. Masalah dasar yang diciptakan ini adalah masalah koherensi : apakah Anda dijamin bahwa suatu istilah akan memiliki makna yang unik, mengingat bahwa istilah yang sama berpotensi memiliki paksaan yang disembunyikan di banyak tempat yang memungkinkan dalam program ini?$c : A \leq B$$c : A \to B$

Salah satu perawatan pertama dari masalah ini adalah makalah John Reynolds 1980, Menggunakan Teori Kategori untuk Merancang Konversi Tersirat dan Operator Generik , yang menunjukkan bagaimana Anda dapat memberikan semantik kategoris ke sistem paksaan dan menggunakannya untuk memastikan koheren.

Jika Anda tertarik pada subtyping koersif untuk teori tipe kaya (misalnya, dependen), maka Zhaohui Luo adalah orang yang tepat.