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.

翻译：我们描述了一种涉及变量绑定及其单子替换操作的非良基语法的泛型构造。这种语法及其替换的构造是在范畴论框架下进行的，特别地，通过使用幺半范畴及其间的强函子来实现。一个语言由多类绑定签名（记作Σ）指定。首先，我们通过ω-连续性为Σ生成可能包含无限项的语言提供了充分条件。其次，我们为Σ生成的语言构造了一个单子替换操作。这一构造的基石是对Matthes和Uustalu提出的异质替换系统概念的温和推广；此类系统封装了实现替换所需的必要余递归方案。相关结果已通过单值数学UniMath库在Coq证明助手中形式化。