非常搞笑的是，在我的Propositional Type Theory里，term和type之间的关系竟然没有稳定的解释。

在intro规则里，要解释成term⊃type，而在elim规则里，要反过来，解释成type⊃term，[允悲]

而好消息是，一旦接受这个中二设定，→intro和→elim都是「可证」的，不是基础规则，[二哈]

++++

发展形式化理论最重要的信仰是，「形式就是一切」，interpretation不重要。但凡简洁且富有表达力的系统，终将找到让哲学家和文科生都满意的解释。