严格关联和单位∞-范畴的语法

我们提出了严格关联和单位∞-范畴的第一个定义。我们的提案以一种类型理论的形式呈现，其中的术语描述了此类结构的操作，而其定义等价关系强制执行所需的严格性条件。关键技术是理论中定义等价的新计算规则，我们称之为插入，按照一种普遍属性进行定义。在定义的术语上，该操作将替代的相干性之一的一个参数“插入”到相干性本身中，适当地修改粘贴图和结果类型，同时简化语法。我们从这种约简关系生成一个方程理论，并详细研究其性质，表明它产生了一个用于相等性的决策过程。作为一种类型理论，我们的模型非常适合生成和验证高阶范畴语句的有效证明。我们通过OCaml实现进行了说明，并给出了几个例子，包括对聚合的一种简短编码，一种在球体同伦群中起重要作用的5维同伦。