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).

翻译：罗素悖论是说明朴素集合论不一致性的最易理解方式。本文提出了一种直接编码罗素悖论的方法，该方法利用类型在类型中的宇宙、Σ类型以及外延等同性（或结合等同性证明唯一性（UIP）的内涵等同性）实现。