前几天和群友一起学习了一下 Type-in-type 可能导致的问题。作为一个能够勉强背诵 ZFC 公理的工科🐖，感觉 Girard’s paradox 的构造十分神奇，遂做学习笔记，尝试在 Lea...