Uniform preorders are a class of combinatory representations of Set-indexed preorders that generalize Pieter Hofstra's basic relational objects. An indexed preorder is representable by a uniform preorder if and only if it has as generic predicate. We study the $\exists$-completion of indexed preorders on the level of uniform preorders, and identify a combinatory condition (called 'relational completeness') which characterizes those uniform preorders with finite meets whose $\exists$-completions are triposes. The class of triposes obtained this way contains relative realizability triposes, for which we derive a characterization as a fibrational analogue of the characterization of realizability toposes given in earlier work. Besides relative partial combinatory algebras, the class of relationally complete uniform preorders contains filtered ordered partial combinatory algebras, and it is unclear if there are any others.
翻译:统一前序是一类集合指标前序的组合表示,它推广了Pieter Hofstra的基本关系对象。一个指标前序可由统一前序表示当且仅当它具有泛谓词。我们在统一前序的层次上研究指标前序的$\exists$-完备化,并识别出一个组合条件(称为“关系完备性”),该条件刻画了那些具有有限交且其$\exists$-完备化为三丛的统一前序。通过这种方式获得的三丛类包含相对可实现性三丛,我们对此给出了一个纤维化类比,该类比源自早期工作中对可实现性拓扑斯特征的刻画。除相对部分组合代数外,关系完备统一前序类还包含滤过有序部分组合代数,目前尚不清楚是否存在其他此类结构。