💻 computer science

Univalent Enriched Categories and the Enriched Rezk Completion

本文通过证明单价富集范畴之间的本质上满且完全忠实函子是等价函畴、证明每个富集范畴都存在 Rezk 完成，以及应用该完成构造单价富集 Kleisli 范畴，对单价富集范畴进行了研究。

原作者： Niels van der Weide

发布于 2026-06-10

📖 1 分钟阅读☕ 轻松阅读

原作者： Niels van der Weide

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一位正在设计城市的建筑师。在标准数学中，你可能会建造一座城市，其中两座看起来完全相同的建筑（同构的）会被视为不同的实体，除非你显式地将它们粘合在一起。但在（本论文所使用的）**单价基础（Univalent Foundations）**的世界里，规则不同：如果两座建筑看起来一样且功能一样，它们就是同一个。不存在任何“隐藏的区别”。

这篇题为《单价富集范畴与富集 Rezk 完成》（Univalent Enriched Categories and the Enriched Rezk Completion）的论文，旨在将这种“长得像即为相同”的规则应用于一种非常特定且复杂的城市规划方式——富集范畴（Enriched Categories）。

以下是该论文旅程的拆解，使用了日常类比：

1. 什么是“富集范畴”？

可以将一个标准范畴想象成一张城市地图，其中的“街道”（态射）只是连接建筑（对象）的简单线条。你知道可以从建筑 A 到达建筑 B，但这条街本身只是一条线。

富集范畴则像是一个街道具有额外纹理的城市。也许从 A 到 B 的街道不仅仅是一条线；它可能是一条“橡胶做的路”，或者是一条“有速度限制的高速公路”，或者是一条“存在于特定顺序中的路径”。

论文的目标： 作者想要建造这些具有纹理的城市（富集范序），但要确保它们遵循严格的“长得像即为相同”的规则（单价性）。

2. 问题：“虚假”的等价

在这些具有纹理的城市世界中，你有时会构建出一张看起来完美但实际上有缺陷的地图。

场景： 想象你有一张城市地图，其中每个建筑都有一个双胞胎，且它们之间的街道也完美匹配。然而，这张地图却将这对双胞胎视为不同的人。
问题所在： 在标准数学中，你可能需要一个“魔杖”（选择公理）来修复这一点，并说：“好吧，让我们假装他们是同一个。”
论文的解决方案： 作者证明了，如果你从一个已经遵循“长得像即为相同”规则（单价富集范畴）的城市开始，你不需要魔杖。如果一张地图是“满忠实”的（它完美地保留了所有街道纹理）并且是“本质上满射”的（它覆盖了所有的建筑），那么这张地图自动就是一个完美的等价关系。这是一张“金票”，证明了这两个城市是完全相同的。

3. “Rezk 完成”：城市翻新工程

有时，你可能会从一个并不遵循“长得像即为相同”规则的混乱城市开始。这个城市拥有看起来完全相同但被视为不同的重复建筑。

隐喻： 想象一个有两个咖啡馆的城市，“乔的咖啡馆”和“乔伊的咖啡馆”，它们实际上是同一家企业，但在名单上是分开列出的。这会导致混乱。
解决方法（Rezk 完成）： 论文提供了一种被称为 Rek Completion 的构造。你可以把它看作是一项大规模的城市翻新工程。你获取这个混乱的城市，识别出所有重复的建筑，并将它们物理合并为单一的、唯一的结构。
两种翻新方式：
1. Yoneda 方法： 这就像是拍摄每一个可能视角的城市照片，然后根据这些照片重建城市。这种方法很精确，但可能需要更大的蓝图（更大“宇宙”的数据）。
2. HIT 方法： 这使用了一种特殊的构造工具，称为高阶归纳类型（Higher Inductive Types）。想象一台 3D 打印机，它可以瞬间将重复的建筑拼接在一起，而不需要更大的蓝图。这种方法更高效，并且能保持城市规模不变。

4. 为什么这很重要？（Kleisli 的转折）

论文最后将这种翻新工具应用于一种特定类型的城市结构，称为 Kleisli 范畴。

类比： Kleisli 范畴就像是一个你只有在携带特殊“魔法袋”（Monad）时才能旅行的城市。
问题： 构建这些“魔法袋”城市的标准方式通常会导致混乱的布局，产生重复的建筑（它不是单价的）。
结果： 作者使用他们的 Rezk Completion 翻新工具，修复了这个混乱的“魔法袋”城市。他们证明了你总是可以构建出这些城市的“完美”版本，使得“长得像即为相同”的规则成立。这使得数学家可以使用这些复杂的结构，而不必担心隐藏的重复项。

论文主张摘要

结构同一性： 他们证明了对于这些富集城市，如果两个城市是等价的（看起来和表现都一样），那么它们就是恒等的。这被称为“结构恒等原理”。
无需魔术： 他们展示了如果两个城市之间的映射覆盖了所有内容并保留了所有纹理，它自动就是一个完美的等价关系。不需要额外的假设。
翻新工具： 他们提供了两种方法，可以将任何富集城市“翻新”成一个完美的、单价的版本（Rezk Completion）。
应用： 他们使用这种翻新来修复“Kleisli”城市（与编程逻辑和单子相关），确保它们在数学上是严谨且具有单价性的。

简而言之，这篇论文构建了一个严密的工具包，以确保当我们为数学地图添加额外的“纹理”时，不会意外创建破坏逻辑规则的重复项。它提供了修复任何此类混乱的蓝图，并确保城市是完美统一的。

技术摘要：单价富集范畴与 Rezk 完成

问题陈述
范畴论是数学和计算机科学的基础框架，其中富集范畴（enriched categories）在高等范畴论、同伦论以及编程语言语义学（例如使用 DCPO 处理效应语言）中发挥着至关重要的作用。然而，在单价基础（Univalent Foundations，即同伦类型论）的语境内，标准的范畴定义往往无法满足等价原理，即同构的对象应当是不可区分的。虽然对于普通范畴而言，“单价范畴”（univalent categories，即对象恒等性等价于同构）已被建立，但“单价富集范畴”的理论仍不发达。具体而言，目前缺乏关于结构恒等原理（structure identity principle）、等价刻画（characterization of equivalences）以及 Rezk 完成（即一种单价反射，Rezk completion）存在的形式化结果。此外，诸如 Kleisli 范畴之类的标准构造往往不是单价的，因此需要一种在富集设置下构建单价类似物的方法。

方法论
本文在 Rocq 证明助手中利用 UniMath 库开发了富集范畴理论，并遵循单价基础。其核心方法论包括：

将富集视为结构： 本文并非采用 Kelly 的定义（即将富集范畴定义为对象集合与同态对象），而是将它们定义为一个范畴连同一种富集。一个富集由单性范畴 $\mathcal{V}$ 中的同态对象、恒等态射与复合态射，以及范畴中态射与同态对象元素之间的对应关系组成。这种视角将富集范畴视为一个带有额外结构的单价范畴。
显示双范畴（Displayed Bicategories）： 为了证明结构恒等原理，作者利用了显示双范畴的机制。他们定义了一个在单价范畴双范畴（$UnivCat $）之上的显示双范畴$ dEnrichCat_{\mathcal{V}} $。该显示结构的总体双范畴为$ EnrichCat_{\mathcal{V}} $。这使得可以复用已有的关于$ UnivCat$ 的单价性结果来证明富集设置下的单价性。
正交分解系统（Orthogonal Factorization Systems）： 为了刻画等价关系，论文采用了双范畴中的正交分解系统。它定义了全忠实且本质全射的富集函子，并证明它们构成了一个正交分解系统。
两种 Rezk 完成的构造： 论文提供了两种不同的富集范畴 Rezk 完成的构造方式：
- Yoneda 嵌入： 将完成构造为富集 Yoneda 嵌入的像。这要求 $\mathcal{V}$ 是完备且对称单调闭的，但依赖于标准的范畴论。
- 高归纳类型（HITs）： 通过利用 HITs 的消去规则，为底层范畴的 Rezk 完成赋予一种富集。这种方法避免了对 $\mathcal{V}$ 完备性或闭性的假设，并在宇宙在对 HITs 封闭的情况下保持了宇宙层级。
普遍性质： 论文确立了 Rezk 完成的普遍性质，证明了通过弱等价（全忠实且本质全射的函子）进行预复合会诱导函子范畴之间的伴随等价。

主要贡献与结果

结构恒等原理： 论文证明了单价富集范畴的双范畴（ $EnrichCat_{\mathcal{V}}$ ）是单价的（定理 2.8）。这意味着两个单价富集范畴之间的恒等类型等价于它们之间的伴随等价类型。
等价刻画： 论文证明了每一个既是全忠实又是本质全射的富集函子都是伴随等价（定理 4.8）。这一结果是构造性的，且依赖于定义域和陪域的单价性，从而避免了选择公理。
Rezk 完成： 论文提供了两种富集范畴的 Rezk 完成构造（构造 5.5 和 5.7）。论文证明了每个富集范畴都存在 Rezk 完成，并满足如下普遍性质：任何到单价富集范畴的函子都可以沿着弱等价进行唯一扩展（定理 5.2）。
单价 Kleisli 范畴： 作者构造了单价富集 Kleisli 范畴。他们定义了标准 Kleisli 范畴 $K(T)$ 以及其单价对应物 $Kleisli(T)$（作为 Eilenberg-Moore 范畴的一个全子范畴）。利用 Rezk 完成和普遍性质，他们证明了 $Kleisli(T)$ 满足单价富集范畴双范畴中 Kleisli 对象（Kleisli objects）的普遍性质（构造 6.9）。
示例与刻画： 论文提供了许多示例，包括自富集（self-enrichment）、相反富集（opposite enrichments）以及基变换（changes of base）。它刻画了在笛卡尔结构（如 DCPO）上的富集，并引入了一种“支持 Smash 积的封闭结构”的概念来处理有标集合（pointed sets）和偏序集（posets），尽管它也指出了关于有标 DCPO 的局限性。

意义与主张
本文声称在单价基础内为富集范畴理论建立了稳健的基础。其主要意义在于：

形式化： 提供了一个用于富集范畴的 Rocq/UniMath 形式化库，此前该领域相比普通范畴缺乏广泛的形式化实现。
概念正确性： 证明了将富集范畴视为带有额外结构的单价范畴（通过富集）可以简化诸如结构恒等原理等基本性质的证明过程。
解决非单价问题： 解决了常见构造（如 Kleisli 范畴）本身并非单价的问题，通过提供一种系统性的方法（Reck 完成）来获得能够保持必要普遍性质的单价版本。
基础工具： 将单价富集范畴的双范畴确立为单价双范畴，这是在单价设置下进一步开发内部范畴论（例如单子、极限）的前提条件。

作者指出，虽然其方法涵盖了许多标准情况，但在处理某些结构（如有标 DCPO）的 Smash 积时存在局限性，因为这些情况下必须在适当的范畴中进行商运算而非在集合中。他们建议未来的工作可以涉及开发富集范畴的装备，或推广 Smash 积的概念以处理这些情况。

1. 什么是“富集范畴”？

2. 问题：“虚假”的等价

3. “Rezk 完成”：城市翻新工程

4. 为什么这很重要？（Kleisli 的转折）

论文主张摘要

类似论文