paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fibred fibration categories

纤维化的纤维化范畴
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 论文属于类型论、范畴语义与同伦类型论中的关系参数性研究，与用户关注的静态分析、Agentic/LLM 程序分析、浮点/贝叶斯程序分析及其与 LLM 交叉等核心方向无直接关联；仅作为 PL 形式语义基础可能间接相关。引用 9 inbox
Taichi Uemura
形式语义
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：引入纤维化的类型论纤维化范畴，为恒等类型的逻辑谓词提供范畴语义，并导出同伦类型论的关系参数性。

本文引入“纤维化的类型论纤维化范畴”，即在 Martin-Löf 类型论的范畴模型之间建立纤维范畴结构，用以刻画模型间的逻辑关系。该框架为恒等类型（identity types）的逻辑谓词提供了范畴描述，使得可在此语义层面研究类型论模型的关系性质。作为应用，作者证明了同伦类型论（homotopy type theory）的一个关系参数性结果。其推论表明：在环路空间（loop space）上，多态自函数类型的每个闭项都同伦于某个环路（loop）的若干次拼接。该工作连接了类型论的范畴语义、逻辑关系与参数性，为 HoTT 中多态性的关系推理提供了统一工具。

问题
如何为 Martin-Löf 类型论的范畴模型及其逻辑谓词（尤其 identity types）提供统一的纤维化范畴描述，并在同伦类型论中获得关系参数性？
方法
引入 fibred type-theoretic fibration categories，将类型论纤维化范畴组织成纤维范畴，并用其范畴化描述 identity types 的逻辑谓词。
评估
作为应用给出同伦类型论的关系参数性证明；推论表明 loop space 上多态自函数的每个闭项同伦于某环路迭代拼接。
原文摘要（Abstract）

We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Löf type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{Uemura17,
  title = {Fibred fibration categories},
  author = {Taichi Uemura},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005084}
}