A Naive Encoding of Russell's Paradox in 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).