Rocq 中图重写的粘合剂范畴论

Rocq 中图重写的粘合剂范畴论

Adhesive category theory for graph rewriting in Rocq

https://arxiv.org/abs/2509.17392

摘要
我们使用层级构建器（Hierarchy Builder，HB）设计了一个关于粘合范畴的Rocq库。该库围绕两个层级结构构建：第一个是范畴的层级，底层为通常的范畴，顶层为粘合范畴，中间包含粘合范畴的若干较弱变体；第二个是态射的层级（特别是同构、单态射和正则单态射）。这些层级的每一层都配备了多个接口，用于定义实例。

我们涵盖了诸如拉回（pullbacks）和等化子（equalizers）等基本范畴论概念，以及粘合范畴特有的结果。利用该库，我们形式化了范畴图重写理论中的两个核心定理：Church-Rosser定理和并发定理。我们提供了多个实例，包括类型范畴、有限类型范畴、简单图范畴以及预层范畴。我们详细说明了所采用的实现选择，并报告了在此形式化工作中对HB的使用情况。

关键词：粘合范畴，范畴图重写，图变换，Rocq，层级结构

1 引言
范畴图重写（categorical graph rewriting），或称图变换（graph transformation）[13, 30]，是一个用于在图上定义重写规则的框架，它结合了双推出（double-pushout, DPO）操作语义，并利用范畴来抽象掉具体图模型之间的差异。该框架在计算机科学中有诸多应用，例如基于模型的软件工程 [18]；在数学物理中，例如弦图（string diagrams）的重写 [6]；以及在（生物）化学系统的建模中，其中重写规则用于描述粒子或分子之间的相互作用 [3, 11]。

在这一领域中，人们经常使用粘合范畴（adhesive categories）[15, 23]；这类范畴包含所有预层范畴（presheaf categories），因此涵盖了许多多重图（multigraphs）的范畴。然而，也存在一些重要的图范畴并非粘合范畴。这促使人们引入更弱的概念，以覆盖这些情形，同时仍能保证DPO语义的良好性质。例如，简单图（simple graphs）的范畴仅为rm-拟粘合范畴（rm-quasiadhesive）[15, 20]，而项图（term graphs）的范畴则是rm-粘合范畴（rm-adhesive，早期文献中也称为拟粘合范畴（quasiadhesive））[10]。

这些范畴类别的定义涉及拉回（pullbacks）、推出（pushouts）和单态射（monomorphisms）等标准概念；然而，证明这些定义之间存在的各种蕴含关系有时相当困难。因此，对它们的形式化可被视为检验通用范畴论库开发能力的一个有趣测试案例。

与通常的形式化工作一样，一项具有挑战性的任务在于如何组织定义，使得引理能够以最一般的形式陈述和使用，同时实例又能以最高效的方式定义。为此，我们选择使用层级构建器（Hierarchy Builder, HB）[9]。HB提供了一种高级语言来定义结构层级，并支持多重继承等高级特性。HB会检查这些高级描述的一致性，并将其自动翻译为适当的Rocq记录（records）、典范结构（canonical structures）和强制转换（coercion）声明 [14]，从而在无需用户额外干预的情况下获得简洁的记号和可靠的推理机制。

我们当前的形式化工作包括：(i) 一个通用范畴论库；(ii) 粘合范畴、rm-粘合范畴和rm-拟粘合范畴的定义；(iii) 两个重要定理，它们为这些结构提供了若干等价刻画；(iv) 范畴图重写中的两个关键定理；以及 (v) 典型实例（类型、集等价类（setoids）、有限类型、简单图、预层范畴和切片范畴（slice categories））。

该抽象库是无公理的（axiom-free），我们详细说明了某些具体实例所需引入的公理。
本项开发工作已在 Gitlab¹ 上公开，其中的 README 文件将本文中的定理与代码的相关部分进行了对应链接。

结构安排：第2节详细介绍了我们所实现的所需基础范畴论²，以及如何使用HB组织这些内容。我们工作的一个特点是，不仅定义了范畴的层级结构，还定义了态射的层级结构（包括同构、单态射、满态射及其正则（regular）和分裂（split）变体）。这一点至关重要，因为这些概念无处不在，我们需要良好的推理机制以高效地使用它们。我们回顾了所设定的记号、如何处理捆绑（bundled）与非捆绑（unbundled）定义，以及如何利用范畴对偶性。

第3节转向图变换所涉及的特定范畴。我们回顾了关键定义与定理；解释了如何以模块化的方式将这些概念扩展到前述标准层级中，同时遵循HB的“遗忘式继承”（forgetful inheritance）策略；并概述了我们为（rm-（拟）粘合）范畴形式化的主要定理。

第4节简要介绍了范畴图重写，并阐述了我们已形式化的两个定理。

第5节讨论了具体实例的形式化。

最后，我们在第6节总结了研究成果，第7节讨论了相关工作，第8节展望了未来的研究方向。

2 通用范畴论
2.1 态射上的相等性

在类型论中形式化范畴时，第一个问题是：“如何比较态射？”

一种简单的方法是使用命题相等（propositional equality），并依赖诸如函数外延性（functional extensionality）和证明无关性（proof irrelevance）（例如用于比较自然变换）等公理，以及某些形式的选择公理和谓词外延性（例如用于将函子按函子等价关系取商³）。

为了在保留命题相等的同时减少所需公理的数量，可以考虑使用泛等类型论（univalent type theory）并形式化泛等范畴（univalent categories）[2, 29, 39]。然而，许多范畴并非泛等的（例如任何包含两个不同但同构对象的范畴），我们仍需在早期就引入函数外延性以支持若干构造，而要定义（h）集（(h)sets）与函数的范畴，还需泛等公理。

为完全避免使用公理，我们可以转而形式化 E-范畴（E-categories）[21, 37]，其中每个 hom 集都配备一个用户自定义的等价关系，而态射之间的等式仅在这些等价关系下成立。正如文献 [19, 40] 所做的那样，我们在本工作中也采用这种方式，并利用 Rocq 对集等价类重写（setoid rewriting）[31] 的支持。其主要优势在于，我们能保持库中所有抽象部分无公理（axiom-free），将潜在的公理使用推迟到具体实例中。我们将在第 6.2.2 节进一步讨论这一选择。

2.2 范畴与态射的层级结构

我们从 HB 仓库示例中的范畴定义出发（已适配为 E-范畴，后文中我们简称为“范畴”）。该定义分为三个步骤：
• 拟范畴（quivers）：对象与 hom 集；
• 预范畴（precategories）：拟范畴加上单位箭头与复合操作；
• 范畴（categories）：预范畴再加上单位律与结合律的等式。

虽然我们的开发工作严格来说并不需要如此细致的范畴定义，但这是一个展示我们如何使用层级结构的良好范例：我们定义相互继承的结构（例如，每个范畴都是一个拟范畴），并将操作与引理定义在能够陈述或证明它们的最低（即最一般）层级上。例如，终对象（terminal object）的概念可在任意拟范畴中定义；同构（isomorphism）的概念以及“终对象在唯一同构意义下唯一”这一事实需要预范畴；而“两个同构的复合仍是同构”这一性质仅在范畴中成立。

除了范畴的层级结构外，我们还定义了一个态射的层级结构：除了单态射（monomorphisms）、满态射（epimorphisms）和同构之外，我们还需要正则单态射（regular monomorphisms）与分裂单态射（split monomorphisms）及其对偶概念：正则满态射与分裂满态射。（正则单态射是指某对平行态射的等化子；分裂单态射是指存在一个回缩（retraction）的态射。）在本文其余部分，我们按文献惯例将“epimorphism”和“monomorphism”分别简写为“epi”和“mono”。

这两个层级结构如图 1 所示。当我们转向粘合范畴论时，将进一步扩展这些层级结构，因此拥有适当的工具支持至关重要：我们此处将范畴特化为粘合范畴的用例，只是形式化大型结构层级时常见活动的一个实例。

更具体地说，我们需要能够：

1. 在所有继承自某结构的结构（即层级中位于其上方的所有结构）中，自由使用该结构可用的任何定义、记号或引理；

2. 在不破坏现有代码的前提下新增结构，甚至可在层级中间插入新结构；

3. 以增量方式并通过多种手段提供实例。

在 Rocq 中，实现此类层级结构主要有两种方式：类型类（typeclasses）[32, 40] 和典范结构（canonical structures）[25]。类型类初始设置通常更简单，但在大型层级中较为脆弱且可能效率低下 [4, 第 12 节]。典范结构已在 mathcomp [26] 中大规模使用，被证明稳健高效，但需要对合一算法有专家级理解。一些开发者混合使用了典范结构与类型类 [28]。HB 提供了一个抽象层，代表终端用户使用典范结构实现打包类（packed classes）[14]。我们选择尝试其功能，并在此报告其当前的局限性。

打包类中的推理由单一索引驱动。在我们的范畴层级中，索引是对象的类型；在态射层级中，索引是态射本身。例如，若我们请求对象类型为 Type 的典范范畴，将得到类型与函数构成的范畴；若请求对象为两个给定范畴之间的函子的典范范畴，则会得到函子与自然变换构成的范畴。类似地，对于态射，若我们请求底层前向态射为恒等态射的典范同构，将得到恒等同构；若我们希望将一个复合态射提升为满态射，推理机制会尝试将其两个组成部分分别提升为满态射。

打包类最重要的概念是 mixin：一种依赖于索引及该索引上其他 mixin 的数据类型。例如：
• 拟范畴的 mixin 仅依赖对象索引类型，由每对对象对应的集等价类（即带等价关系的类型）组成；
• 预范畴的 mixin 依赖拟范畴的 mixin，包含单位箭头与复合操作；
• 范畴的 mixin 依赖预范畴的 mixin，包含单位律与结合律满足预期等式的证明；
• 态射的 mixin 定义态射的个别性质，因此彼此之间从不相互依赖，仅依赖其索引（即一个态射）；
• 单态射的 mixin 包含该态射是单态射的证明——这是一个 Prop 中的性质；
• 正则单态射的 mixin 包含它作为等化子所对应的那对平行态射及其相应证明；类似地，分裂单态射的 mixin 包含其右逆及其相应证明。在这两种情况下，这些附加信息必须位于 Type 中，因为它们具有计算相关性，常用于构造 Type 中的其他值；然而，由于我们使用集等价类和 E-范畴，可以在比较态射时安全地忽略这些信息。

HB 中的结构被定义为 mixin 的集合，继承通过包含关系定义：若结构 A 包含结构 B 的所有 mixin，则 A 继承自 B。这一点极为重要，因为它意味着 HB 仅实现 遗忘式继承（forgetful inheritance） [9]。这一策略具有稳健性的优势，但也对我们组织代码的方式带来若干影响。

在我们的开发中，结构总是恰好定义一个额外的 mixin（加上其所继承结构的 mixin）。我们已在上文提及其中一些 mixin。注意，按这些定义，一个正则单态射包含两个 mixin：正则单态射的 mixin 和单态射的 mixin，尽管前者蕴含后者。若为追求极简而省略后者，则从正则单态射到单态射的继承将不再是遗忘式的。出于同样原因，一个同构包含七个 mixin（参见图 1）。

为应对这些冗余，我们使用 HB 提供的 构建器（builders） 机制：我们证明并声明，单态射的 mixin 可由正则单态射的 mixin 推导得出，因此只需提供后者即可构建具体实例。（详见第 2.5 节。）我们对其他标准蕴含关系（例如，分裂单态射蕴含正则单态射）也采取类似处理，但这仍不足够。例如，众所周知，一个既是正则单态射又是满态射的态射是同构；对偶地，每个既是正则满态射又是单态射的态射也是同构。因此，除了按继承关系所暗示的“同时证明分裂满态射与分裂单态射”之外，我们至少还有另外两种构造同构的方式。为此，我们使用 工厂（factories）——这些是不直接出现在结构中的 mixin，但可用于构建其他 mixin。对于上述例子，我们声明一个空工厂，依赖正则单态射与满态射的两个 mixin，并定义构建器，从这些数据出发构造所有其他 mixin（对偶情况亦然）。

2.3 记号

在形式化数学中，清晰简洁且支持重载的记号至关重要 [16]。结合隐式参数与 Rocq 的记号系统，HB 所采用的典范结构与（可逆）强制转换（coercions）的组合，使得我们能够获得接近教科书记号的符号系统。

例如，我们仅用 A → B 表示范畴中从 A 到 B 的箭头类型。由于范畴以其对象类型为索引，A 与 B 的类型会典范地确定该范畴。若它们是跨度（spans），则箭头表示跨度态射；若它们是函子，则箭头表示自然变换，等等。类似地，我们统一使用符号 idmap 表示单位态射，(◦) 表示复合，(≡) 表示态射相等，(≃) 表示同构，无论具体范畴为何。对于需要记号强制指定范畴（从而指定对象类型）的情形，我们也设置了以范畴为索引的变体（例如 A →_C B）。

范畴论中一个常见模式是：存在唯一满足某性质的态射，其中“唯一性”是在态射等价意义下的。如同 Wiegley 的库 [40] 所做的那样，我们使用单一记号 (Σ!) 及若干工具来处理此类陈述。我们将此记号定义在 Type 中，因为其见证（witness）通常具有计算相关性（例如，在拉回中，我们需要完全访问中介箭头，以便用它构造新的态射）。

2.4 捆绑（Bundling）

使用 HB 定义的结构是捆绑的（bundled）。例如，一个范畴是一个单一的包（package），其中包含对象类型、hom 集类型、单位态射等。当我们需要对结构进行量化时，这种方式非常方便，并能产生简洁易读的证明上下文：例如，我们可以用一个单一变量 i : A ≃ B 表示一个同构，而无需分别引入一个底层态射变量和一个额外的假设来说明该态射确实是一个同构。

然而，在某些情况下我们也需要非捆绑的（unbundled）结构。例如考虑如下命题：“沿同构的拉回仍是同构”。作为输入的同构可以是完全捆绑的，但输出的同构则不能是捆绑的：该引理的目的正是将一个普通态射提升为同构；因此我们需要一个谓词“是同构”（being an isomorphism）的名称。在态射层级结构中，这种现象在证明过程中十分常见——我们常常在局部上下文中拥有某些态射，并需要逐步将其提升为正则单态射、分裂单态射等。为此，我们使用别名（aliases）或 HB 提供的打包机制（packing mechanism）。在这两种情况下，我们都使用了一些特定的样板代码（boilerplate code），这些代码未来应发展为一种通用的提升策略（promotion tactic）。

这种捆绑与非捆绑定义之间的张力，也出现在我们当前层级结构之外的概念中。例如考虑拉回（pullbacks），我们可以采用多种定义方式，每种都有其各自的优缺点：

1. 成为一个拉回可以被表述为对构成一个方图的四个态射所满足的一种性质：

这种完全非捆绑的定义非常适合陈述和证明标准事实，例如拉回方图的粘贴引理（pasting lemma）、单态射在拉回下的稳定性，或关于同构可在拉回方图的角点之间移动的引理：

在第一个引理中， isMono 是我们用于“是单态射”的非捆绑谓词。）

2. 然而，上述定义在定义具有所有拉回的范畴时并不方便。事实上，在这种情况下，更可取的做法是拥有一个（捆绑的）跨度类型，该跨度能将给定的余跨度（cospan）补全为一个拉回：

1. 当需要证明拉回在唯一同构意义下唯一时，最佳定义是最具范畴论思想的那个：拉回是“将给定余跨度补全为交换方图的跨度范畴中的终对象”。我们证明了这一刻画：它要求我们定义子范畴和跨度范畴，但随后的唯一性作为终对象唯一性的特例自动成立。

最终，我们同时保留了一个完全非捆绑的定义（陈述一个态射方图是一个拉回）和一个部分捆绑的定义（陈述一个余跨度具有一个拉回），并设置了适当的引理以在这两种定义之间来回转换。我们对库中所有其他概念也采取类似处理方式。特别地，前述关于单态射沿拉回保持稳定的引理被表述如下，其中 A→C 是我们对从 A 到 C 的单态射类型的记号。

2.5 一个具体示例：正则单态射

为了给出 HB 如何组织结构的一个具体示例，以下是我们如何在库中定义正则单态射的方式。

首先，回顾一下：一对平行态射 f 和 g 的等化子（equalizer）是最一般的态射 e，使得 f ∘ e = g ∘ e，如下图所示。

正则单态射（regular mono）于是就是一个对某对态射而言是等化子的态射，我们可以证明每个正则单态射确实是一个单态射：

首先，我们定义一个新的 mixin；接着，我们定义一个新结构 RegMono，它由这个新 mixin 与结构 Mono 的所有 mixin（实际上仅有一个）共同组成；最后，我们将前述引理注册为一个从新 mixin 到 Mono 的 mixin 的构建器。该构建器使得我们只需提供预期的性质即可定义正则单态射，而结构 RegMono 的冗余定义确保了从正则单态射到单态射的遗忘式继承。

从此刻起，我们可以同时使用类型 RegMono A B（表示从 A 到 B 的正则单态射）和非捆绑谓词 isRegMono f来刻画此类态射。

2.6 对偶性

范畴论中的另一个重要概念是对偶性：每个抽象概念或引理都有其对偶概念——例如满态射/单态射、等化子/余等化子、始对象/终对象及其唯一性、推出/拉回及其粘贴引理等。与其他工作 [2, 19, 28, 35, 40] 类似，我们尽可能充分利用对偶性，以避免代码重复。核心工具是结构 S（无论是拟范畴、预范畴、范畴，或是各类态射之一）的对偶结构的定义：通过对一般结构 S 应用某个引理于其对偶结构，我们便可得到对偶命题。

尽管在纸上这很容易实现，但在我们的实际工作中仍需克服若干困难：

1. Cᵒᵖ 的同构类型仅等价于 C 的同构类型（即使考虑参数反转，甚至在证明无关性下：若 A ≃_C B 是一个包含三个字段的记录：

{i: A ⇝ C B; j: B ⇝ C A; _: i ∘ j ≡ id ∧ j ∘ i ≡ id}

则 B ≃_Cᵒᵖ A 是如下记录：

{i: A ⇝ C B; j: B ⇝ C A; _: j ∘ i ≡ id ∧ i ∘ j ≡ id}

请注意，两个合取项已被交换，因此我们最多能通过命题外延性证明这两种类型在命题意义上相等。

这意味着我们有时需要显式地将一种同构转换为另一种。

1. 我们希望为了可读性和用户体验而采用重复的定义：拉回（pullback）的定义和推出（pushout）的定义都不应涉及 Cᵒᵖ。然而，术语 @Pushout C 和 @Pullback Cᵒᵖ 应在定义上相等，以利用对偶性。这一要求阻止了我们在这些定义中使用专用的记录类型，这正是我们在上述 Pullback 定义中使用通用 sigma 类型的原因。

2. 范畴 C 和 Cᵒᵖ 共享相同类型的对象，因此我们需要消歧义，以便规范结构推断能够找到正确的实例。为此，我们使用别名：我们定义一个恒等函数 catop: Type → Type，将其绑定到记号 Sᵒᵖ，并用于标注我们希望推断其对偶结构的对象类型。对于态射，我们使用相同的技术，使用以下恒等函数：

   
   

（在第二个证明中，iso_op 就是上述作用于同构的强制转换操作。）
从长远来看，我们希望开发对沿范畴等价传递结果的支持，这将有助于避免当前在对偶性方面存在的一些迂回做法和局限性。

1. 黏着范畴论
   现在我们已经建立了所需的范畴论基本概念，接下来将简要解释黏着范畴论的核心思想，然后介绍我们对该理论的形式化工作——重点在于如何以模块化的方式描述该理论，其基础是上一节所述的通用范畴论库。

3.1 范·坎彭方块与黏着态射

我们首先定义推出方块的三个性质以及两类新的态射。提供这些定义是为了让大家了解我们需要操作的概念；在下文中，它们可被视为黑箱。

定义 3.1（范·坎彭方块 [23]）。一个推出满足：

• 稳定的（stable），当且仅当对于每个具有如下图示箭头的交换立方体，其中底面是推出方块，侧面是拉回方块，则顶面也是推出方块；

• 精确的（exact），当且仅当对于每个具有如下图示箭头的交换立方体，其中底面是推出方块，左侧面和背面是拉回方块，顶面是推出方块，前侧面和右侧面是拉回方块；

• 范·坎彭的（Van Kampen），当且仅当它既是稳定的又是精确的。

  
  

  范·坎彭方块的两个关键性质是：它们保持单态射（monos），并且它们本身也是拉回方块 [23]。

  定义 3.2（黏着态射 [15]）。一个态射是：

  黏着态射是预黏着的（通过沿恒等态射作拉回）；预黏着态射是正则单态射；而同构总是黏着的。

  因此，我们将这两类态射转化为 HB 结构。我们可以轻松地将它们添加到我们现有层级结构中位于正则单态射之上的位置，其中黏着态射位于预黏着态射之上。然而，对于同构态射该如何处理尚不明确（见图2）。事实上，若在同构之下声明黏着态射，将要求我们更新同构的定义，使其包含黏着与预黏着态射的混入（mixins）。虽然以这种方式重构代码是可能的，但并不令人满意：由于黏着态射相当特殊，我们希望仍能将先前关于满态射和单态射的层级结构作为库来使用，而将黏着态射作为一个可选模块进行插件式引入。因此，我们只剩下两种选择：

• • 预黏着的（pre-adhesive），当且仅当它沿任意态射都存在推出，且这些推出既是稳定的又是拉回；

  • 黏着的（adhesive），当且仅当它沿所有态射的拉回都是预黏着的。

  1. 将同构声明为黏着态射的实例：这使我们能够在预期出现黏着态射的地方使用同构，但破坏了 HB 的遗忘继承策略。事实上，有了这样的实例声明后，HB 有两种方式为一个同构配备“比如正则单态射”的混入：要么通过直接包含，要么通过利用其是黏着态射（从而是预黏着态射，从而是正则单态射）的证明。由于这两种路径没有特别理由必须相等，这可能导致问题情境——即在一个路径下成立的语句无法在提及另一路径的上下文中使用。因此，HB 拒绝此类定义。

  2. 添加一个新的同构结构（Iso'），同时继承自原始同构结构和黏着态射结构。采用这种方式，我们遵守了遗忘继承原则，但有时需要显式地将同构从核心库提升到扩展后的同构结构。这可以通过空工厂（empty factory）轻松实现，但仍会引入一些开销，并且每当我们需要在同构之下引入新的态射类别时，都不得不引入新的副本。

目前我们选择了第二种方法，希望未来能设计出更令人满意的解决方案来处理这种后验形式的继承。

3.2 子对象

我们还将需要“子对象”（subobject）的概念，它是集合论包含关系在范畴论中的推广。给定一个范畴 C 中的对象 X，子对象是一个单态射 m: A ↪ X。子对象构成一个范畴，其中从 m: A ↪ X 到 n: B ↪ X 的态射是满足 n ∘ f = m 的态射 f: A → B。当 C 具有拉回时，该范畴具有所有积，称为“二元交”。余积（并不总是存在）称为“二元并”。若底层单态射是正则的，则称该子对象为“正则的”。

3.3 黏着范畴的层级结构

我们现在可以介绍我们已形式化的三种黏着范畴变体。每次我们都提供教科书定义——以及任何可能的替代刻画，并解释我们所做的选择。

3.3.1 Rm-准黏着范畴。我们从 rm-准黏着范畴开始，这是该层级中最弱的结构。

定义 3.3（rm-准黏着范畴 [15]）。一个范畴是 rm-准黏着的，当且仅当：

• 它具有所有拉回；

• 它沿正则单态射具有推出；

• 沿正则单态射的推出是稳定的；

• 沿正则单态射的推出也是拉回。

由于“具有所有拉回”——即每个余锥都有拉回——是一个常见要求，我们首先为这类范畴定义了一个结构 CatPb；类似地，我们为那些沿正则单态射具有推出的范畴定义了一个结构 CatRmPo——这意味着每个其中一个态射是正则单态射的锥都有推出。

我们将定义中的最后两个要求转化为一个新的混入（mixin），以定义结构 RmQAdhesive。在这里——比小范畴、预范畴和范畴的情形稍复杂一些——我们可以看到在 HB 中如何通过组合较弱结构的独立部分来构建更强的结构。

至此，我们的层级结构包含以下依赖关系：

在 rm-准黏着范畴的理论中，我们证明了正则单态射在复合下保持不变，因此构成一个子范畴；推出保持正则单态射；并且正则子对象确实具有二元并（这些结果并非平凡，参见 [15, 23]）。

3.3.2 Rm-黏着范畴。Rm-黏着范畴（最初在 [23] 中被称为准黏着范畴）是黏着范畴论层级结构中的下一级。

定义 3.4（Rm-黏着范畴 [15], [23]）。一个范畴是 rm-黏着的，当且仅当：

• 它具有所有拉回；

• 它沿正则单态射具有推出；

• 沿正则单态射的推出是范·坎彭的。

注意，前两个性质与 rm-准黏着范畴相同；但第三个性质乍看之下似乎无关。然而，我们有：

定理 3.5（[15, 定理 3.3]）。在一个具有所有拉回的范畴 C 中，以下三者等价：

1. C 是 rm-黏着的；

2. 正则单态射是黏着的，且正则子对象在二元并下封闭；

3. C 是 rm-准黏着的，且正则子对象在二元并下封闭。

由于存在三种等价刻画，我们可以选择其中最方便的一种作为原生定义。虽然第一点是教科书中的定义，但上述定理的第三点表明，rm-黏着范畴实际上就是 rm-准黏着范畴。因此，为了优化模块化，我们采用第三点作为原生定义：RmAdhesive 仅在 RmQAdhesive 的基础上额外添加“正则子对象在二元并下封闭”这一性质。

用 HB 的术语来说，这意味着上述第 3 点的第二部分成为一个混入（mixin），而第 1 点和第 2 点则成为依赖于具有拉回的范畴（即 CatPb）的工厂（factory）。蕴含关系 1 ⇒ 3 和 2 ⇒ 3 已被证明并声明为构建器（builder）。这意味着 HB 会将它们用作指令，说明如何根据任一工厂提供的数据，在层级结构中构造出直至 RmAdhesive 所需的混入。这使得用户可以方便地以三种不同方式创建实例。

相反，蕴含关系 3 ⇒ 1 和 3 ⇒ 2 可被视为 rm-黏着范畴理论的一部分。我们以标准 Rocq 引理的形式陈述并证明这些蕴含关系；只要我们拥有一个 rm-黏着范畴的实例，就可以应用它们：

• 沿正则单态射的推出是精确的，因此也是范·坎彭的（这是蕴含关系 3 ⇒ 1 的剩余部分）；

• 正则单态射是黏着的（这是蕴含关系 3 ⇒ 2 的剩余部分，实际上它是 rm-准黏着范畴的一个定理）。

3.3.3 黏着范畴。我们最终进入黏着范畴，它在我们的层级结构中构成最丰富的结构：

定义 3.6（黏着范畴 [15]）。一个范畴是黏着的，当且仅当：

• 它具有所有拉回；

• 它沿单态射具有推出；

• 沿单态射的推出是范·坎彭的。

定理 3.7（[15, 定理 3.2] 和 [23, 命题 6.2]）。在一个具有所有拉回的范畴 C 中，以下陈述等价：

1. C 是黏着的；

2. 所有单态射都是黏着的；

3. C 沿单态射具有推出，这些推出既是稳定的又是拉回；

4. C 是 rm-黏着的，且所有单态射都是正则的；

5. C 是 rm-准黏着的，且所有单态射都是正则的。

（第五点在上述参考文献中未提及；它由定理 3.5 的第三项推导而来：在 rm-准黏着范畴中，正则子对象的并存在且为单态射，因此此处即为正则单态射。）我们从该定理可见，黏着范畴是 rm-黏着的，且它们沿所有单态射都具有推出。后一要求相当普遍，因此我们将其制成结构 CatMPo，位于 CatRmPo 之上。然后我们将黏着范畴定义为具有沿所有单态射的推出、且所有单态射均为正则的 rm-黏着范畴。我们所获得的层级结构如图 3 所示。我们提供四个工厂来构造黏着范畴，分别对应上述定理中的第 1、2、3 和 5 项（第 4 项被第 5 项取代）。

与 rm-黏着范畴类似，我们提供定理 3.7 的其余部分作为关于黏着范畴的标准 Rocq 引理。

请注意，由于遗忘继承机制，结构 CatMPo 中提供了两个函数用于计算沿单态射和沿正则单态射的推出。虽然后者可从前者推导得出，但并非必须如此，且这两个函数可能对同一输入返回不同值（尽管这些值仍通过推出的唯一性同构）。

为了减轻显式处理模同构的工作负担，我们谨慎地编写我们的混入和语句，使其量化所有可能的推出（或在不同上下文中其他类型的值）。例如，定理 3.7 的第三项在形式化时被建模为一个函数，该函数为每个单态射与态射构成的锥提供某个推出，并附加“所有沿单态射的推出都是稳定的且是拉回”的性质——而不仅仅是该函数所提供的那些推出。

4 图重写理论

黏着范畴及其变体使我们能够一次性建立有关图重写系统的定理，从而抽象出图的具体选择（简单图、有向图、带标签图、有限图、带类型图等）。为了检验我们的库是否成熟到足以形式化该领域的前沿成果，我们形式化了两个重要定理 [23, 定理 7.7 和 7.10]。因篇幅所限，我们在此不提供其精确陈述，仅说明其总体性质以及我们形式化它们所需的少量代码行数。

4.1 DPO 图重写的基本概念

在双推出（DPO）图重写中，重写规则（也称为“产生式”）由一个锥组成，其中两个目标对象分别为输入和输出，源对象为中间状态。这样的产生式如图 4 所示。中间对象的直观含义是：它包含图中除上下文外被该产生式保留的部分，即既不被删除也不被添加的部分。

我们关注线性产生式，其中锥的两个态射均为正则单态射。

重写规则的一个应用称为“推导”。给定一个产生式 I ← K → O 和一个对象 X 以及态射 I → X，一个推导是一个如下形状的图，其中两个方块均为推出。

直观上，态射 I→X表明了产生式的左侧如何以及在何处与输入图（X）匹配，Z是将该产生式应用于 X后得到的结果，而态射 O→Z则表明产生式的右侧出现在该图中。

4.2 局部 Church-Rosser 定理

第一个定理（[23, 定理 7.7]）给出了项重写系统中局部 Church-Rosser 性质 [34] 的一种刻画。它关联了两个性质：并行无关性（parallel independence）和顺序无关性（sequential independence）。前者是关于从同一图出发的两个推导的性质，表明其中任一推导都不会删除另一个产生式所作用的部分；后者也是关于两个推导的性质，其中第二个产生式作用于第一个推导的输出，表明第二个产生式既不需要、也不会删除第一个产生式向图中添加的内容。该定理断言这两个性质是等价的。由于并行无关性具有对称性，它等价于两种顺序下的顺序无关性。这一点尤其有助于在图语法中定义推导的等价关系，以及为每个等价类定义规范推导（canonical derivations）[22]。[23] 中的证明是针对 rm-黏着范畴撰写的，但它同样适用于 rm-准黏着范畴。该定理及其证明在纸上占 2 页，涉及最多 11 个对象的图表。得益于我们的库，我们的形式化仅用了 80 行陈述和 78 行证明。

4.3 并发定理并发定理

（[23, 定理 7.10]）确定了在何种条件下、以及如何将两个产生式组合成一个新的产生式，使得该新产生式所诱导的推导与依次应用原两个产生式所得的推导相同。这种可能性在建模工具中非常有用，例如可将一组小规则合并为一个更大的规则，从而在基于模型的软件工程中将复杂的重构操作 [18] 表示为单一的原子操作。与上述情况类似，[23] 中针对 rm-黏着范畴给出的证明同样适用于 rm-准黏着范畴。该定理及其证明在纸上占 2.5 页，涉及最多 19 个对象的图表。我们用 107 行代码完成了其形式化陈述，证明部分则用了 105 行。

5 实例
现在我们讨论已形式化的关键实例：类型（types）、集等价类（setoids）、有限类型（finite types）、简单图（simple graphs）、切片范畴（slice categories）和函子范畴（functor categories）。在每种情况下，我们都讨论了所需（如果有的话）的类型论公理。

5.1 类型与函数
我们已证明：以 Type 为对象类型、以外延函数（extensional functions）为态射的范畴 Types 是一个黏着范畴。这在类型论中对应于集合论中以集合为对象、以函数为态射的集合范畴。我们使用定理 3.7 的第三项来构造这一黏着范畴。证明它具有所有拉回是容易的，但构造并分析推出则更为困难。

为了构造商类型并定义推出的余投射，我们采用了 Arthur Azevedo de Amorim [12] 编写的一个文件。该实现依赖于以下标准公理⁵：

• 谓词外延性（Predicate extensionality），即：若两个谓词逐点等价，则它们相等。

  predicate_extensionality:
  ∀ A (P Q: A → Prop), (∀ a, P a ↔ Q a) → P = Q.

• 构造性确定描述（Constructive definite description），这是一种选择形式，表明：若存在唯一一个对象满足某个在 Prop 中的谓词，则我们可以从中提取出一个 Type 类型的见证。

  constructive_definite_description :
  ∀ A (P: A → Prop), (∃! x, P x) → {x | P x}

应当注意的是，我们正在构建所有的推出，而证明一个范畴是黏着的仅需沿单态射（在集合的情形下即为单射函数）的推出。若 f 是单射，则关系 R 会简化：等价类要么是单元素集 {a}（对任意 a ∈ A 且不在 f 的像中），要么恰好包含 B 的一个元素。这意味着每个等价类都有一个典范元素。然而，为 A 中元素计算其典范元素需要计算它们在 f 下的逆像，而我们尚未找到使用更弱公理系统实现这一点的方法。

谓词外延性蕴含证明无关性，而我们需要证明无关性以在此范畴中获得拉回（用于中介箭头的唯一性）。此外，我们使用构造性确定描述来证明沿单态射的推出是稳定的且是拉回。反之，我们已证明：在证明无关性前提下，黏着范畴要求所有单态射都是正则的，在 Types 中等价于构造性确定描述。

5.2 集等价类与外延函数
在类型论中避免外延性公理的一种标准技术是用“集等价类”（setoids）替代类型：集等价类是由一个类型和一个用户自定义的等价关系组成的结构。集等价类之间的态射是底层类型之间的函数，且这些函数将等价元素映射为等价元素。我们证明了相应的范畴 Setoids 是黏着的，其中两个态射被定义为等价，当且仅当它们作为函数是逐点等价的。

为该范畴配备拉回和推出是容易的——这一次完全不需要任何公理，因为我们在定义对象时可以自由选择如何比较元素。证明推出是稳定的，以及沿正则单态射的推出是拉回，稍微困难一些，但即便如此，我们也不需要任何公理。因此，Setoids 是 rm-准黏着的。

为了进一步证明它是 rm-黏着的（或黏着的），根据定理 3.5（或定理 3.7），只需证明正则子对象在并运算下封闭（或所有单态射都是正则的）。我们已证明以下等价关系：

• Setoids 中正则子对象在并下封闭，当且仅当析取可以提升为直和（sum）：

  ∀ P Q : Prop, P ∨ Q → P + Q

• Setoids 中所有单态射都是正则的，当且仅当构造性不定描述（Constructive Indefinite Description, CID）成立：

  ∀ A (P : A → Prop), (∃ x, P x) → {x | P x}

后一性质是一个标准公理；它比构造性确定描述（Constructive Definite Description, CDD）更强，因为它不要求见证的唯一性；而前一性质也可由它推出（取 A = 2 即可）。

因此，虽然我们在范畴 Types 中从一开始就不得不使用谓词外延性和 CDD，但在范畴 Setoids 中我们可以逐步添加公理：

• rm-准黏着性无需任何公理；

• rm-黏着性需要“析取可提升为直和”；

• 黏着性则需要 CID。

特别地，由于 Church-Rosser 定理和并发定理在 rm-准黏着范畴中成立，我们在 Setoids 中无需任何公理即可获得这两个定理。

5.3 有限类型与函数

当我们限制到有限类型时，可以无需任何公理就得到一个黏着范畴 finTypes。我们使用 mathcomp 库 [26] 中的有限类型和函数对其进行形式化，该库完全契合我们的需求。

为了实现代码的复用，我们使用从 finTypes 到 Setoids 的函子，该函子将一个有限集映射到其自身，并配备命题相等关系作为等价关系。由于该函子是全且忠实的（full and faithful），它能反映推出和拉回；此外，它还保持（正则）单态射、推出和拉回。因此，我们可以利用该函子将 Setoids 的性质（如 (rm-(准))黏着性）导入到 finTypes 中。

由于我们希望该实例不依赖任何公理，我们仅通过上述方式证明了 finTypes 的 rm-准黏着性，并单独证明了在 finTypes 中所有单态射都是正则的。

对于范畴 Types，我们无法采用这种方法：要证明相应的函子保持推出（即使仅限于沿正则单态射的推出），似乎必须使用 CID（构造性不定描述）。然而，CID 对于 Types 成为黏着范畴并非必需，因此这种做法会是次优的。

我们还证明了：在假设谓词外延性和 CID 的前提下，范畴 Types 与 Setoids 是等价的。已知这一组公理组合可推出 Type 中的排中律；但我们尚不清楚是否必须依赖这些公理才能证明这两个范畴的等价性。

5.4 有向简单图

一个有向简单图是由一组顶点配备一个二元边关系构成的集合。（为简化起见，我们允许自环。）通过考虑图同态（即保持边关系的函数），我们得到范畴 SGraphs：给定图 (V₁, E₁) 和图 (V₂, E₂)，态射 f : V₁ → V₂ 必须满足：∀x, y ∈ V₁, x E₁ y ⇒ (f x) E₂ (f y)。

请注意，Setoids 并不是“边构成等价关系”的简单图的子范畴：图同态是逐点严格比较的，而集等价类态射则是逐点比较并模去目标端的等价关系。

SGraphs 是 rm-准黏着的 [5]；我们在 Rocq 中通过重用 Types 是黏着的这一事实，并验证所生成的各种函数均保持边关系，来证明这一点。

然而，SGraphs 不是 rm-黏着的，因为推出运算会丢失两个顶点之间边的重数信息。图5给出了一个具体的反例：沿一个单态射的推出不是一个拉回。

5.5 函子与预层范畴

给定范畴 C 和 D，从 C 到 D 的函子范畴及自然变换具有所有拉回，前提是 D 具有所有拉回；并且当 D 是黏着范畴时，该函子范畴也是黏着的。对于切片范畴，证明的主要部分是将拉回、单态射等性质从自然变换传递到其分量，反之亦然。若一个自然变换的所有分量具有某个性质，则该自然变换也具有该性质，这通常很直接；但反过来往往更复杂。

例如，如果我们有一个自然变换的拉回，我们不能直接使用其在某个分量上的泛性质。但我们可利用拉回的唯一性以及典范拉回是按分量构造的事实——但这要求我们首先拥有一个典范拉回。因此，许多此类证明都要求 D 是一个具有所有拉回的范畴。

类似的问题也出现在单态射上：我们无法直接证明：若一个自然变换是单态射，则它的所有分量都是单态射。在这种情况下，与拉回不同，不存在一个范畴“具有所有单态射”的概念。不过，我们可以利用这样一个事实：一个自然变换是单态射等价于它具有平凡核对（任何单态射沿自身的拉回是一个恒等同构构成的锥），然后借用拉回的证明方法。这是来自 [7, 推论 2.15.3] 的证明。对于正则单态射，这可能也成立，但需要类似的极限联系。证明这一点将使我们能够声明：只要 D 是 rm-(准)黏着的，则函子范畴也是 rm-(准)黏着的。我们将此留待未来工作。

结合本实例与 Types（或 Setoids）实例，我们推导出：对于任意范畴 C，预层范畴 (Cᵒᵖ → Types)（或 (Cᵒᵖ → Setoids)）是黏着的。这包括了有向多重图范畴 MGraphs [5]，只需将 C 实例化为具有两个对象和它们之间两条平行箭头的范畴即可。类似地，对于有限预层 (Cᵒᵖ → finTypes)，从而也包括有限有向多重图，无需使用任何公理。

5.6 切片/上范畴

给定一个范畴 C 中的对象 X，我们可以定义切片范畴 C/X。它的对象是形如 f: A → X 的态射；从 f: A → X 到 g: B → X 的态射是一个 C 中的态射 h: A → B，使得 f = g ∘ h。（X 的子对象实际上构成 C/X 的一个子范畴。）

对于范畴层级结构中任意结构的一个实例 C，以及任意 X ∈ C，切片 C/X 是与 C 相同结构的一个实例，即：若 C 是 rm-黏着的，则切片也是 rm-黏着的，等等。证明主要由一系列引理组成，用于在切片范畴与原范畴之间传递拉回、推出、单态射和正则单态射等性质。

这种构造是额外具体模型的有用来源。例如，范畴 Types/X 是 X 上的（内涵性）多重集范畴；而对于选定的图范畴，X 的切片范畴是“以 X 为类型”的图范畴，即：X 的每个节点定义一种类型，其边定义允许存在的边，因此该切片范畴中的对象是满足类型约束的图，而图之间的态射则是保持类型的态射 [13]。因此，范畴图变换的一般理论可立即提升到这些更丰富且实际有用的设置中。

6 讨论

6.1 代码

该库总共包含约 10,000 行代码。其中约 5100 行用于预备知识和通用范畴部分（集等价类、范畴、推出、同构、函子等），2400 行用于黏着范畴理论（范·坎彭方块、黏着态射、子对象、rm-准黏着范畴等），400 行用于 Church-Rosser 和并发定理，2100 行用于各种实例。开发过程是无公理的，除了证明类型与集等价类范畴是黏着范畴的部分（见第 5.1 和 5.2 节）。

6.2 集等价类与 -范畴

如第 2.1 节所述，我们形式化的是 -范畴而非普通范畴：homset 是集等价类。范畴的概念可平滑地推广到 -范畴：只需做到以下几点：

• 将所有态射之间的命题相等（=）替换为集等价类相等（≡）；

• 要求所有 homset 之间的函数保持这些等价关系（例如，复合运算或函子在态射上的作用）；

• 每当定义一个范畴时，需适当定义态射上的等价关系，例如：通过分量比较自然变换（忽略自然性证明）、通过底层态射比较切片态射、在 Types 中逐点比较函数等。 （后一点通常能简化证明，因为等式往往退化为所期望的性质。）

这一设计选择使我们避免了必须使用公理来构建显式商结构：除第 2.1 节中函子与函子等价的情形外，还涉及正则单态射及其他类态射——虽然“成为正则”的要求带有计算内容且应属于 Type（以便在此基础上构造推出等），但我们希望在比较正则态射时忽略这些计算内容。在所提议的设置下，这一点可以以无公理的方式直接实现。

为此付出的代价是我们必须系统性地证明概念在态射等价下保持不变。为此，我们使用 Rocq 的集等价类重写工具 [31]。例如，我们陈述、证明并使用如下引理：

Instance isPullbackE {C: Cat} {A B C D: C}:CMorphisms.Proper (eqv⇒ eqv⇒ eqv⇒ eqv⇒ iffT)(@isPullback C A B C D).

它表明“是一个拉回方块”这一性质在态射等价（eqv）下是封闭的。由于“是一个拉回”带有计算内容，它是 Type 中的一个性质，因此我们使用 CMorphisms.Proper 和 iffT，而非更常用的 Proper 和 iff（用于 Prop 中的关系）。然而，Rocq 对 Type 中集等价类重写的支撑不如对 Prop 中的那么稳健，这有时需要一些令人不快的手动调整——若 rewrite 策略未能自动使用上述实例时。

6.3 关于 Hierarchy Builder 可用性的报告

HB 在当前工作中被证明非常方便，我们的整体评价相当积极。它使我们能够清晰高效地建立层级结构，而无需手动调整典范结构或类型类推断。以下是我们列出的一些进一步改进的建议。

全称多态性（Universe polymorphism）。HB 目前尚不支持全称多态性，因此我们必须复制集等价类结构，以避免在定义 Setoids 范畴时出现全称不一致问题：小型集等价类作为该范畴的对象，大型集等价类则用于 -范畴的 homset。由于 Rocq 已经支持全称多态记录，我们未发现任何重大障碍，并希望 HB 开发者能在不久的将来解除这一限制。

动态层级结构（Dynamic hierarchies）。在我们的态射层级结构（图 2）中有一个显著现象：当向上遍历范畴层级时，某些类会发生坍缩。例如，在一个黏着范畴中，每个单态射都是黏着的（因而也是正则的）。HB 目前不支持此类层级结构的动态行为。我们使用具有适当依赖关系的引理，在条件满足时轻松提升态射；但此类提升必须明确写出，将其自动化将十分有趣。

后验继承（Inheritance a posteriori）。我们的主要关切是当前无法后验添加向下继承关系，正如第 3.1 节末尾所解释的那样。在保持推理健壮性的前提下解决此问题颇具挑战性，但在模块化方式下设计和组合大型库时可能必不可少。

7 相关工作

在各类证明助手中有大量范畴论的形式化工作 [1, 2, 17, 19, 29, 33, 35, 36, 38–40]。其中仅有极少数库定义了正则单态射 [19, 35, 39]。据我们所知，唯一对黏着范畴进行形式化的是 Lean 的 mathlib 库 [35]，其中包含了教科书定义、沿单态射的推出仍为单态射且是拉回的事实，以及 Types 和函子范畴的实例。

与该库相比，我们发展了更多概念（如 rm-准黏着范畴和 rm-黏着范畴），提供了这些范畴的替代刻画（定理 3.5 和 3.7），证明了局部 Church-Rosser 定理和并发定理，并提供了更多实例（有限类型、集等价类、简单图、切片范畴等）。另一个重要区别在于：与 [19, 40] 类似，我们使用 -范畴以避免依赖公理；而 Lean 的 mathlib 依赖于命题外延性和一种强形式的选择公理，因此采用经典逻辑——包括 Type 中的排中律。特别是，他们可以自由地构造商结构，并使用严格范畴（参见第 2.1 节）。

8 未来工作

我们希望能开发出支持在复合运算结合律下进行重写的工具（在我们的开发中，我们在显式的重写序列里提到了结合律 439 次）。虽然设计一个策略（tactic）来在复合结合律及其他若干范畴论基本定律下证明态射等式是容易的，但陈述这些等式本身却十分繁琐。因此，我们希望实现一种匹配算法，能够自动识别在结合律意义下的出现位置，并自动执行相应的传递性步骤——类似于 [8] 中的方法，但适用于范畴复合这类异构运算。

我们的库包含大量关于同构的引理：许多概念仅在同构意义下定义，通常可以引入、移除或移动同构（例如第 2.4 节中的引理 isPullback_iso_A）。然而，与纸质证明中通常隐式处理同构相比，目前对这些引理的使用仍会带来额外的复杂性。一个典型例子见 [20, 第 321–322 页]：“[…] 因此 B≃B′。特别地，我们可以从图中去掉所有撇号。” 我们希望自动化这一任务，并开发一个策略，用于删除给定的同构，仅保留其源对象或目标对象。

例如，在如下目标中：

其中 i 和 A 已被删除，而 f 和 g 的类型已修改，使用了确保性质 P 在同构下保持的适当引理。（这是一个典型情况：在单值范畴中工作要容易得多——同构退化为命题等式，并且总是可以被消除。）

同样地，我们需要开发沿范畴等价传递结果的方法。例如，有向多重图的范畴既可定义为预层范畴（参见第 5 节），也可更具体地通过用户自定义的图类型及其间态射类型来定义。通过沿范畴等价传递我们的黏着性证明，我们将免费获得这些终端用户变体也是黏着的这一事实。如第 2.6 节所述，在某些情况下，此类工具将有助于对偶性：有时我们无法从定义上获得对偶性，而只能达到范畴等价的程度。这里的挑战在于以一种合理的方式传递计算内容。

最后，若能拥有一种工具，以图形方式显示当前正在处理的图表，将使证明过程更容易——即使仅处于只读模式，也与 Ambroise Lafont [24] 的工作不同，后者的更宏大目标是实现图形化证明。

原文链接：https://arxiv.org/pdf/2509.17392