命题截断的一般通用性质
逻辑
2015-10-23 v3
摘要
在 Shulman 意义上的类型论纤维化范畴（表示至少具有 1、Sigma、Pi 和恒等类型的依赖类型论）中，我们定义了从 A 到 B 的常函数类型。这涉及一个无限层的相容性条件塔，因此我们需要该范畴具有关于 omega 上图的 Reedy 极限。我们的主要结果是，如果该范畴进一步具有命题截断并满足函数外延性，则常函数类型等价于类型 ||A|| -> B。如果 B 对于给定的有限 n 是一个 n-类型，则相容性条件塔变为有限的，且对非平凡 Reedy 极限的要求消失。整个构造随后可以在同伦类型论（Homotopy Type Theory）中进行，并推广了截断的通用性质。这提供了一种在 B 未知是否为命题时定义函数 ||A|| -> B 的方法，并简化了寻找满足 A -> Q 和 Q -> B 的命题 Q 的常用途径。
引用
@article{arxiv.1411.2682,
title = {The General Universal Property of the Propositional Truncation},
author = {Nicolai Kraus},
journal= {arXiv preprint arXiv:1411.2682},
year = {2015}
}
备注
v1: 27 pages; v2: 34 pages, improved notation, improved presentation in general, added figures to improve readability, added proof for the finite cases, corrected conjecture; to appear in the post-proceedings of TYPES'14 (LIPIcs); v3: fixed the statement of Lemma 2.1