单价公理

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

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

布尔否定给出自等价

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

在 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。