Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories

TL;DR

This paper develops a category-theoretic framework for non-wellfounded syntax with variable binding, providing criteria for infinite term generation and a monadic substitution operation, formalized in Coq.

Contribution

It introduces a novel categorical construction for non-wellfounded syntax with binders, including criteria for infinite terms and a formalized substitution mechanism.

Findings

Criteria for generating infinite terms via {}-continuity.

Construction of a monadic substitution operation.

Formalization of the framework in Coq using UniMath.

Abstract

We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say {\Sigma}. First, we provide sufficient criteria for {\Sigma} to generate a language of possibly infinite terms, through {\omega}-continuity. Second, we construct a monadic substitution operation for the language generated by {\Sigma}. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution. The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.