A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on

TL;DR

This paper develops a unified, syntax-free framework for modeling substitution across presheaves, nominal sets, and related structures, using closed monoidal structures to generalize and connect various approaches.

Contribution

It introduces a general method to derive closed monoidal structures from monoidal actions, unifying and extending substitution tensors for presheaves and nominal sets.

Findings

Recovered known substitution tensors for presheaf categories

Developed novel substitution tensors for nominal and renaming sets

Established new correspondences between different categorical models of syntax

Abstract

Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as lambda-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, modeling substitution in the spirit of Fiore et al.'s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action of a monoidal category on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories, but also yields novel notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In doing so, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of novel correspondences between them.