Incoherent coherences

01/19/2022

∙

by   Xu Huang, et al.

∙

0

∙

share

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.