「一个类型宇宙就够了」：aramh 抛出类型理论七连暴论

spikedoanz · x · 2026-08-19

aramh 发起「争议观点日」，连抛七条类型理论暴论：一个类型宇宙足矣，现有类型理论需要多个 universe 只是尚未找到正确基础，是一种 hack；直觉主义无意义，构造主义才是关键；给类型理论加公理是骗局；MLTT 之外大有可探索空间；证明不相关性（proof irrelevance）是异端；前置性（predicativity）是审查制度；以及「tactics 绝不使用」。