Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations, $\lambda$2-fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.
翻译:Jacobs为纤维类提出了定义(弱、强、强、分)通用物体;根据他对(分)通用物体的定义,Jacobs开发了一个重要的纤维结构元件,用于绝对逻辑和计算机科学,包括更高顺序纤维、多形态纤维、美元/lambda 2纤维、三角形和其他。我们观察到,根据给定定义,分裂的通用物体不必特别成为通用对象,多元形态纤维、三角形等的定义足够严格,足以排除一些基本例子:例如,由可变性部分组合代数引发的纤维型前置结构,不是这种意义上的三角体。我们提出新的术语调整,强调在性质上最常见的通用物体的形式,即研究内部类别、三角形和多形态学的注解性定义性。此外,我们提议了一种由更高类别理论的近期发展动态所启发的新的周期性通用物体类别,以及可变性能的纤维化原型,将普通的原型的原型的原型变成一个任意性理论。