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

Edit TL;DR: Lean4 有 Definitional proof irrelevance，所以本篇内容纯瞎搞。不过还有一部分没瞎搞的，所以留着。 --- 上上次被 Heterogeneous identity 创还是...