A Naive Encoding of Russell’s Paradox in Type Theory [naive-encode-of-russell-paradox]

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.