非相干相干
Incoherent coherences
摘要：
本文探索了一个具有良好类型和良好作用域的语法的通用框架，并使用了类似于传统抽象代数的签名公理方法。在语法上定义操作所需的样板代码被识别和抽象掉了。一些频繁的样板证明也被推广。
英文摘要：
This article explores a generic framework of well-typed and well-scoped syntaxes, with a signature-axiom approach resembling traditional abstract algebra. The boilerplate code needed in defining operations on syntaxes is identified and abstracted away. Some of the frequent boilerplate proofs are also generalized.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
