粪海狂蛆 [index]
粪海狂蛆 [index]
2025年十月起的 seminar 笔记, 主要资料即 Principles of Dependent Type Theory. Russell’s paradox is the most easily understandable way to illustrate the inconsistency of naïve set theory. This note proposes a direct encoding of Russell’s paradox with
type-in-type universe, sigma types, and either extensional identity or intensional identity
with the uniqueness of identity proofs (UIP). See here for note in pdf. See here for the formalization in Agda and Rocq. 1. Principles of Dependent Type Theory 的笔记 [type-theory-book]
2. A Naive Encoding of Russell’s Paradox in Type Theory [naive-encode-of-russell-paradox]
