降级公理

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

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

目录

1定义

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

定义 1.1. 降级公理指如下等价成立: 其中:

分别指宇宙 类型.

指类似泛等公理中描述的等价, 可以理解为一种同构. 降级公理不依赖等价的具体定义.

命题宇宙, 一般来说是非直谓的 (否则降级公理就没有意义了).

术语翻译

降级公理英文 resizing axiom