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证明助手中实现了形式化。