关于HoTT中累积宇宙（Cumulative Universes）是否属于公理的疑问

嘿，很高兴看到你刚入坑类型论和HoTT——这领域的细节确实容易让人挠头，你的观察特别到位，很多初学者都会卡在这个点上。我来试着帮你理清规则和公理的核心区别，以及累积宇宙到底归哪一类。

首先得明确HoTT里对“规则”和“公理”的定义：

• 规则是推导式的，它的逻辑是“如果你已经有了X，那你就能合法地得到Y”。它更像系统的操作手册，指导你怎么从已有构造生成新东西，不会凭空断言某个事物存在。
• 公理是断言式的，它直接告诉你“某个东西就是存在/成立”，不需要任何前置条件，是凭空给你加的一个“设定”。

回到累积宇宙：严格来说，HoTT里的累积性是作为规则引入的，而非公理。它的形式大概是这样：

如果A : U_i（也就是类型A属于第i个宇宙），那么你可以推导出A : U_j，其中j > i。

你看，这是一个推导规则——它没有直接说“存在一个包含所有小类型的大宇宙”，而是允许你把一个小宇宙里的类型“提升”到更大的宇宙里。这是基于已有前提的操作，不是凭空的断言。

要是把它做成公理的话，表述可能会变成“对于任意宇宙层级i，都存在一个更高层级j > i，使得所有U_i里的类型都属于U_j”——这就是一个直接的存在断言，不需要从已有结论推导，直接给系统加了一个设定。

当然，有时候你会看到有人把累积性叫做“公理”，这是因为在一些非形式化的讨论里，它看起来像是一个假设，但在HoTT的形式化系统中，它确实是规则的一部分。而HoTT核心系统说“没有公理”，指的是没有那种像ZFC里选择公理、无穷公理那样的直接存在断言，所有核心构造都是通过规则推导出来的。

举个简单例子：假设你有自然数类型ℕ : U₀，根据累积规则，你可以合法地写出ℕ : U₁、ℕ : U₂……这是规则允许你做的推导，而不是公理直接给了你一个包含ℕ的U₁。

备注：内容来源于stack exchange，提问作者dream