Why a type X cannot contain a predicate on X — via Russell's paradox

InconsistentImpredicativeSums.agda

{-# OPTIONS --type-in-type --no-positivity-check  #-}

module InconsistentImpredicativeSums where
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Product
open import Data.Empty
-- hiding (⊥-elim)
-- open import Data.Empty.Irrelevant

--------
-- Some setup
--------
_↔_ : Set → Set → Set
P ↔ Q = (P → Q) × (Q → P)
infix 2 _↔_

taut : ∀ P → ¬ (P ↔ ¬ P)
taut P (P→¬P , ¬P→P) = ¬p p
  where
    ¬p : ¬ P
    ¬p = λ p → P→¬P p p
    p : P
    p = ¬P→P ¬p
-- pP↔¬P

-- IS is an impredicative strong sum/Sigma-type: that is, IS a type of values that contain predicates on values.
record IS : Set where
  constructor
    pack
  field
    unpack : IS → Set

russell : IS → Set
russell (pack x) = ¬ x (pack x)

pRussell : IS
pRussell = pack russell

P : Set
P = IS.unpack pRussell pRussell

Peq : russell (pack russell) ≡ (¬ russell (pack russell))
Peq = refl

-- Really hard to write, since russell (pack russell) happily diverges
P↔¬P : P ↔ ¬ P
P↔¬P = (λ P _ → subst (λ x → x) Peq P P) , (λ ¬P → subst (λ x → x) (sym Peq) ¬P)

contra : ⊥
contra = taut P P↔¬P