HoTT为什么不比集合论弱? 第1页

1. Lean4将会终止对HoTT的支持，目前来看Lean4将会更专注于传统数学形式化验证的生态位，如果你对学习类型论和HoTT有关的知识感兴趣的话建议别入坑Lean4
2. Lean3有三大特性破坏了canonicity（正规性，但我更愿意称之为可求值性）使得其不再是构造主义的，即propositional extensionality（命题宇宙等词，对应集合论的外延公理）, quotient soundness（商类型可靠，对应集合论的商集存在性）, choice（选择公理）。
3. Lean验证关于非构造命题的证明代码的具体做法是你只能在一个叫做noncomputable的子集里面间接引用破坏了canonicity的公理，在之后VM会将这些反构造主义的项用erase推理规则给擦除掉。更人话的说就是：你可以写非构造的证明代码，但你不准用这些代码来求值。
4. Lean对于非构造主义命题的自动证明推理应该也是SMT求解器，没什么特别的
5. 冷知识：HoTT也破坏canonicity，CuTT才满足canonicity
6. HoTT为什么不比集合论弱，自己看HoTT book的Theorem 10.5.8，简单来说就是它们将CZF变成了HoTT的内定理，然后加上选择公理AC就复原成了ZFC

如果你问的是这个构造子是怎么想出来的或者怎么写出来的，真的不会，，，回答不了

7.Lean为什么不比集合论弱，因为pCIC(predicative Calculus of Inductive Constructions)不比集合论弱，简单来说CIC的n+2层宇宙级别可以编码ZFC + n个不可达基数。但考虑到类型论需要保持canonicity，因此类似的推广似乎无法超过Con( 个不可达基数 )，无论如何都无法越过ZFC + 无界个^[1]不可达基数。目前类型论^[2]没有支持更强的大基数或者反射原理的计划。

参考

1. ^ 只不过这个无界可以不只是全体集合的势，而是某个超真类，但笔者认为企图通过这样那样的榨柠檬能榨到ZFC + Mahlo基数的水平是过于天真的
2. ^ NF/NFU有一些特有的公理可以翻译成TST上的公理并达到可测基数的水平，某一些大数函数引用了无穷博弈或许可以达到I0的水平，某一些范畴论公理或许可以达到 Vopenka 基数的水平；但至少，通俗的说，负责编译器研发的那个主流构造主义类型论学界，没有更高的大基数需求