Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context -- and for each type a set of terms of said type. 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 Grothendieck fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types. We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type $A'$ is a subtype of $A$ if there is a unique coercion from $A'$ to $A$. Whenever we need a term of type $A$, then, it suffices to have a term of type $A'$, which we can `plug-in' into $A$. For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.

翻译：长期以来，大多数依赖类型的范畴模型都强烈基于集合论：上下文构成一个范畴，对于每个上下文，我们有一个该上下文中类型的集合——而对于每个类型，有一个该类型项的集合。这正是带族范畴、带属性范畴和自然模型的情况；特别地，它们都可以追溯到某些离散的Grothendieck纤维化。我们将这一直觉推广到一般的、不必离散的纤维化情形，使得在给定上下文上，我们不仅有一个集合，而且有一个类型的范畴。我们认为，这种附加的结构可归因于一种子类型概念，该概念与强制子类型共享许多特征，因为它是将子类型视为一种缩写机制的思想产物：我们说给定类型$A'$是$A$的子类型，如果存在从$A'$到$A$的唯一强制映射。那么，每当我们需要一个类型$A$的项时，只需拥有一个类型$A'$的项，就可以将其“插入”到$A$中。对于这种版本的子类型，我们提供了规则、一致性条件和显式模型，并将其与Z. Luo等人提出的强制子类型进行比较和对比。最后，我们提出如何使用本文介绍的工具来找到关联子类型与特定类型构造子的适当规则。