关系预层的实现 (Realization of relational presheaves)

Relational presheaves generalize traditional presheaves by going to the category of sets and relations (as opposed to sets and functions) and by allowing functors which are lax. This added generality is useful because it intuitively allows one to encode situations where we have representables without boundaries or with multiple boundaries at once. In particular, the relational generalization of precubical sets has natural application to modeling concurrency. In this article, we study categories of relational presheaves, and construct realization functors for those. We begin by observing that they form the category of set-based models of a cartesian theory, which implies in particular that they are locally finitely presentable categories. By using general results from categorical logic, we then show that the realization of such presheaves in a cocomplete category is a model of the theory in the opposite category, which allows characterizing situations in which we have a realization functor. Finally, we explain that our work has applications in the semantics of concurrency theory. The realization namely allows one to compare syntactic constructions on relational presheaves and geometric ones. Thanks to it, we are able to provide a syntactic counterpart of the blowup operation, which was recently introduced by Haucourt on directed geometric semantics, as way of turning a directed space into a manifold.

翻译：关系预层通过转向集合与关系的范畴（而非集合与函数的范畴），并允许使用松弛函子，推广了传统预层的概念。这种额外的泛化性具有实用性，因为它直观地允许编码那些具有无边界或多边界可表示对象的情形。特别地，预立方集合的关系泛化在并发建模中具有自然应用。本文中，我们研究关系预层的范畴，并为其构造实现函子。我们首先观察到它们构成一个笛卡尔理论的基于集合的模型范畴，这尤其意味着它们是局部有限可表现范畴。通过运用范畴逻辑的一般结果，我们随后证明此类预层在一个余完备范畴中的实现是该理论在相反范畴中的模型，这允许刻画存在实现函子的情形。最后，我们阐明本工作可应用于并发理论的语义学。具体而言，实现使得人们能够比较关系预层上的句法构造与几何构造。借此，我们能够为blowup操作提供一个句法对应物——该操作由Haucourt最近在定向几何语义学中引入，作为一种将定向空间转化为流形的方法。