单价公理 | Codeboy's Blog

形式陈述

在宇宙 $\mathcal U_i$ 中，固定

\begin{aligned} \mathsf{fib}_f(b)&=\Sigma(a:A).\mathsf{Id}_B(f(a),b),\\ \mathsf{isContr}(X)&=\Sigma(c:X).\Pi(x:X).\mathsf{Id}_X(c,x),\\ \mathsf{isEquiv}(f)&=\Pi(b:B).\mathsf{isContr}(\mathsf{fib}_f(b)),\\ (A\simeq B)&=\Sigma(f:A\to B).\mathsf{isEquiv}(f). \end{aligned}

这里选用每个纤维可缩的标准等价定义；带适当相干条件的半伴随等价给出等价的表述。由恒等类型的路径归纳，任何 $p:\mathsf{Id}_{\mathcal U_i}(A,B)$ 都诱导等价

\mathsf{idtoeqv}_{A,B}(p):A\simeq B,

且 $\mathsf{idtoeqv}(\mathsf{refl}_A)$ 计算为恒等等价。单价公理断言这个函数本身是等价：

\mathsf{isEquiv}(\mathsf{idtoeqv}_{A,B}).

等价地，可取得

\mathsf{ua}_{A,B}:(A\simeq B)\to \mathsf{Id}_{\mathcal U_i}(A,B)

以及两侧逆律

\mathsf{idtoeqv}(\mathsf{ua}(e))=e, \qquad \mathsf{ua}(\mathsf{idtoeqv}(p))=p,

其中等号都位于相应恒等类型，公理式 HoTT 不把它们默认升级为 judgmental equality。宇宙层级同样不可省略： $A,B:\mathcal U_i$ ，而谈论该宇宙及其等价结构可能位于更高层。单价性可对每层分别公设，也可由 universe-polymorphic 规则族给出。

“等价”不是一条任意函数，也不只是写出同样元素个数；本页要求每个纤维可缩。展示一个函数的同伦逆足以证明它满足这一条件，但不能直接把未经相干处理的“某个逆加两条逆律”数据类型当作 $\mathsf{isEquiv}(f)$ ；那份原始 quasi-inverse 数据在高阶类型上可能有额外的非平凡路径。对集合层类型，这与双射相符；对高阶类型，它保留全部路径结构。因而“同构即相等”只能作受控口号，不能把带结构对象的任意外部同构直接变成定义相等。

直觉

单价性说宇宙把类型按结构而非名字识别：若两个类型之间存在真正的等价，宇宙内部便有一条路径连接它们；反过来，沿任何宇宙路径运输都会产生等价。它把“用等价对象替换不改变数学内容”内化为可沿路径运输的原则。

这仍不是文本替换。 $A$ 与 $B$ 不会因为给出 $e:A\simeq B$ 就突然具有相同语法，类型检查器也不会在普通公理式 MLTT 中把 $\mathsf{ua}(e)$ 化成 refl。使用者得到的是恒等类型居民，可通过 transport、J 与高阶路径推理；计算行为取决于理论是否另外给 ua 以 judgmental rules。

例子与边界

布尔否定给出自等价

e_{\neg}:\mathsf{Bool}\simeq\mathsf{Bool}, \qquad e_{\neg}(\mathsf{true})=\mathsf{false}, \quad e_{\neg}(\mathsf{false})=\mathsf{true}.

单价性产生宇宙自路径 $p=\mathsf{ua}(e_{\neg}):\mathsf{Bool}=_{\mathcal U_i}\mathsf{Bool}$ 。在恒等族 $X\mapsto X$ 中沿 $p$ 运输 true，可由逆律证明

\mathsf{transport}_{\lambda X.X}(p,\mathsf{true}) =_{\mathsf{Bool}}\mathsf{false}.

在 HoTT Book 的公理口径，这通常是命题式等式，而非左端 judgmentally 约简为 false。若宇宙满足 UIP，所有 $\mathsf{Bool}=\mathsf{Bool}$ 路径都会与 $\mathsf{refl}$ 相同；经 $\mathsf{idtoeqv}$ 便迫使否定等价等同于恒等等价，与它们对 true 的不同作用冲突。因此含有布尔型的单价宇宙不兼容把所有恒等证明压平的 K/UIP。

边界还包括结构层次。群的同构可诱导底层载体等价，但要在“群的类型”中得到路径，必须把运算和定律纳入结构并证明相应 structure identity principle；裸单价性不会丢弃结构。范畴的对象同构与对象相等之间的 univalent category 条件也是进一步定义，不能直接从宇宙单价一句话替代。

推论与应用

单价性推出函数外延性，并支持沿等价运输定理、数据与结构。许多表示无关证明由此缩短：先构造等价，再使用 $\mathsf{ua}$ 把关于一种表示的性质运输到另一种表示。它还使宇宙自身拥有丰富高阶路径，成为同伦类型论研究空间、群胚与同伦层级的核心。

计算实现必须区分口径。把 ua 作为普通常量加入 MLTT，可获得公理推理与语义模型，却没有新增判断式 reduction，不能无条件宣称 canonicity。CCHM 立方类型论通过 interval、composition 和 Glue 构造计算性 univalence，使相关 transport 获得 reduction，并在该新理论中证明规范性。那是对单价原则的计算实现，不是把原公理悄悄改写成 β-rule。

参考资料

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013，§2.10 与 §§4.1–4.4，univalence、idtoeqv、quasi-inverse 数据与可缩纤维的区别。
Vladimir Voevodsky, “Univalent Foundations Project,” 2010 manuscript，单价基础纲领与 universe interpretation。
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom,” LIPIcs TYPES 2015 69, 2018, Article 5，Glue 与计算性 univalence。

形式陈述 ​

形式陈述