{-# OPTIONS --type-in-type #-}

open import Data.Empty
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_; id)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst; cong; sym)

record _◁_ {} (A B : Set ) : Set  where
  constructor _,_,_
  field
    ϕ : A  B
    ψ : B  A
    retract : ψ  ϕ  id
open _◁_

record _◁′_ {} (A B : Set ) : Set  where
  constructor _,_,_
  field
    ϕ : A  B
    ψ : B  A
    retract : A  B  ψ  ϕ  id
open _◁′_

postulate
  EM :  {} (A : Set )  A  (¬ A)

 :  {}  Set   Set _
 X = X  Set

t :  {} (A B : Set )   A ◁′  B
t A B with EM ( A   B)
... | inj₁  ℘A◁℘B =
      let ϕ , ψ , retract = ℘A◁℘B
      in ϕ , ψ , λ _  retract
... | inj₂ ¬℘A◁℘B =
       _ _  ) ,  _ _  ) , λ ℘A◁℘B  ⊥-elim (¬℘A◁℘B ℘A◁℘B)

-- type-in-type allows U to be put into Set...
U : Set
U =  X   X

-- ...so that u: U can be applied to U itself
projᵤ : U   U
projᵤ u = u U

injᵤ :  U  U
injᵤ f X =
  let _ , ψ , _ = t X U
      ϕ , _ , _ = t U U
  in ψ (ϕ f)

projᵤ∘injᵤ : projᵤ  injᵤ  id
projᵤ∘injᵤ = retract (t U U) (id , id , refl)

_∈_ : U  U  Set
u  v = projᵤ u v

Russell :  U
Russell u = ¬ u  u

r : U
r = injᵤ Russell

-- up to here EM + impredicativity is enough,
-- as long as _≡_ itself is in the impredicative universe,
-- but to go further, large elimination (via subst) is required
r∈r≡r∉r : r  r  (¬ r  r)
r∈r≡r∉r = cong  f  f Russell r) projᵤ∘injᵤ

r∉r : ¬ r  r
r∉r r∈r =
  let r∈r→r∉r = subst id r∈r≡r∉r
  in r∈r→r∉r r∈r r∈r

false : 
false =
  let r∉r→r∈r = subst id (sym r∈r≡r∉r)
  in r∉r (r∉r→r∈r r∉r)