Two versions of Russell's paradox in type theory

Russell.agda

{-# OPTIONS --type-in-type --with-K #-}

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

{-
Russell's paradox can be encoded in MLTT + K + U:U, as formalised in
https://github.com/KonjacSource/Russell-paradox-in-TT.

The construction there uses Σ-types, but the completely dual
construction with Π-types also works. In both cases the idea is to
construct a set V such that V → Set is a retract of V up to isomorphism;
the contradiction then follows as usual from Lawvere's fixed point theorem.

The definition of V approximates V → Set by replacing V with either a
Σ- or Π-quantified type. In one case, most of the work happens in the
direction _∈_ : V → (V → Set), while in the other case most of the work
is in the other direction set-syntax : (V → Set) → Set.
-}

transp : {A B : Set} → A ≡ B → A → B
transp refl x = x

transp-eq : {A : Set} (x : A) (eq : A ≡ A) → transp eq x ≡ x
transp-eq x refl = refl

module Sigma where
  V : Set
  V = Σ[ A ∈ Set ] (A → Set)

  _∈_ : V → V → Set
  _∈_ a s = Σ[ eq ∈ V ≡ proj₁ s ] proj₂ s (transp eq a)

  set-syntax : (V → Set) → V
  set-syntax = V ,_

  syntax set-syntax (λ x → N) = [ x ∣ N ]

  R : V
  R = [ x ∣ ¬ x ∈ x ]

  R∉R : ¬ R ∈ R
  R∉R R∈R = proj₂ R∈R (subst (λ x → x ∈ x) (sym (transp-eq R (proj₁ R∈R))) R∈R)

  R∈R : R ∈ R
  R∈R = refl , R∉R

  bot : ⊥
  bot = R∉R R∈R

module Pi where
  V : Set
  V = (A : Set) → A → Set

  _∈_ : V → V → Set
  a ∈ s = s V a

  set-syntax : (V → Set) → V
  set-syntax p A x = (eq : A ≡ V) → p (transp eq x)

  syntax set-syntax (λ x → N) = [ x ∣ N ]

  R : V
  R = [ x ∣ ¬ x ∈ x ]

  R∉R : ¬ R ∈ R
  R∉R R∈R = R∈R refl R∈R

  R∈R : R ∈ R
  R∈R eq tR∈tR = R∉R (subst (λ x → x ∈ x) (transp-eq R eq) tR∈tR)

  bot : ⊥
  bot = R∉R R∈R

That's impressive. I tried to get rid of sigma-types, but failed.