Categorical models of subtyping


Greta Coraglia, LUCI Lab, University of Milan. 30 novembre 2023 10:00 TLR limd
Abstract:

We start from categorical semantics of dependent types and propose structural rules involving a new notion of subtyping. We begin by recalling a few classical models, which traditionally have been heavily set-based: this is the case for categories with families, categories with attributes, and natural models. In particular, all of them can be traced back to certain discrete fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, and use the newly found structure on the fibers to interpret a form of subtyping. Interestingly, the emerging notion turns out to be closely related to that of coercive subtyping. This is joint work with J. Emmenegger.