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发展的异质替换系统概念的温和推广；此类系统封装了实现替换所需的核心递归模式。相关结果已在Coq证明助手中通过单值数学的UniMath库完成形式化验证。