paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Displayed Categories

展示范畴
LMCS vol.Volume 15, Issue 12019匹配度 2/10 · 该论文属于范畴论基础与 Coq/UniMath 形式化数学,虽涉及定理证明与证明工程,但与用户核心关注的 LLM/Agent 静态分析、浮点程序分析、贝叶斯程序分析均无直接交集。引用 5 inbox
Benedikt Ahrens, Peter LeFanu Lumsdaine
crossref: 2026-09-10

AI 速览

一句话:提出展示范畴概念,将纤维化等范畴构造从对象相等中解放,并在 Coq/UniMath 中形式化。

论文引入并发展展示范畴:它等价于一个到 C 的函子 F:D→C,但对象与态射按 C 的对象索引给出,而非单独集合。这种重述看似平凡,却让许多函子性质更自然;例如 Grothendieck 纤维化若用函子定义需涉及对象相等,而用展示范畴定义则无需对象相等。作者建议以展示范畴作为类型论中纤维化及相关概念的基础,并指出其在计算机形式化中的价值:统一抽象范畴论构造与证明技术,支持多组件结构范畴的模块化推理。文中大部分材料已在 UniMath 库的 Coq 中形式化。

问题
经典范畴论中纤维化等概念的定义常依赖对象相等,这在类型论和形式化中不自然;实践中范畴又常通过在已有范畴上添加数据或性质来构造。
方法
引入展示范畴,即以 C 的对象索引对象和态射的族,并证明其等价于带函子到 C 的范畴;在此基础上重新表述纤维化等概念,并在 Coq/UniMath 中形式化。
评估
通过概念澄清与 Coq/UniMath 机器化实现,展示其统一和抽象范畴论构造、支持多组件结构范畴模块化推理的能力,并形成可供后续开发使用的实用库。
原文摘要(Abstract)

We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.Comment: v3: Revised and slightly expanded for publication in LMCS. Theorem numbering changed

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot818,
  title = {Displayed Categories},
  author = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:20)2019}
}