斜幺半范畴的相继式演算

Szlachányi的斜幺半范畴是幺半范畴的一个有充分动机的变体，其中单位元和结合子不要求是自然同构，而仅仅是特定方向的天然变换。我们提出了一种用于斜幺半范畴的相继式演算，建立在其中一位作者近期提出的Tamari序（斜半群范畴）相继式演算公式之上。在该演算中，前件由一个stoup（一个可选公式）后跟一个上下文组成，连接词的行为与标准幺半相继式演算中类似，只是左规则只能在stoup位置应用。我们证明该演算关于自由斜幺半范畴中映射的存在性是可靠且完备的，并且一旦对推导施加适当等价关系，它还能刻画映射的相等性。然后我们识别出一个聚焦推导子系统，并确立它恰好包含每个等价类的一个规范代表。该 coherence 定理直接导向判定自由斜幺半范畴中映射相等性以及无重复枚举任意同态集的简单过程。最后，本着Lambek工作的精神，我们描述了这一证明论分析与Bourke和Lack近期将斜幺半范畴刻画为左可表示斜多范畴之间的紧密联系。我们已在依赖类型编程语言Agda中形式化了这一发展。