降级公理

降级公理是同伦类型论中类似分歧类型论中的规约公理的公理, 它指一种将原本属于更大宇宙的类型 “移动到” 更小宇宙中的公理. 这个 “移动” 的思想通过给出一个属于更小宇宙、但等价 (类似同构) 于原类型的新类型的方式实现.

降级公理延拓了命题宇宙的管辖范围, 使得它包含全部的命题. 由于命题宇宙可以被定义为非直谓的, 降级公理大大增加了能非直谓使用的类型的数量.

1定义

首先借助 $\Pi$ 类型定义何为命题:

$$\mathrm{isProp}A:=\prod _{a:A}\prod _{b:A}{\mathrm{Id}}_A(a,b)$$

定义 1.1. 降级公理指如下等价成立: $$\left(\sum _{A:\mathcal{U}}\mathrm{isProp}A\right)\simeq \mathrm{Prop}$$其中:

•	$\mathcal{U},\Sigma$ 分别指宇宙、$\Sigma$ 类型.
•	$\simeq$ 指等价 (类型论), 可以理解为一种同构. 降级公理不依赖等价的具体定义.
•	$\mathrm{Prop}$ 指命题宇宙, 一般来说是非直谓的 (否则降级公理就没有意义了).

术语翻译

降级公理 • 英文 axiom of resizing