Realization of relational presheaves

TL;DR

This paper develops a categorical framework for relational presheaves, extending traditional presheaves to relations and lax functors, with applications in modeling concurrency and relating syntactic and geometric semantics.

Contribution

It constructs realization functors for relational presheaves, characterizes their models categorically, and applies these results to concurrency semantics and geometric transformations.

Findings

Relational presheaves form models of a cartesian theory.

Realization in a cocomplete category yields models of the opposite theory.

Application to semantics of concurrency and geometric blowup operations.

Abstract

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.