{-# OPTIONS --rewriting #-}

{- Lower can be a record if using type-in-type or allowing large eliminations:
{-# OPTIONS --type-in-type #-}
record Lower (A : Set₁) : Set where
  constructor lower
  field raise : A
open Lower
-}

postulate
  _≡_ :  {A : Set₁}  A  A  Set
  Lower : (A : Set₁)  Set
  lower :  {A}  A  Lower A
  raise :  {A}  Lower A  A
  beta :  {A} {a : A}  raise (lower a)  a

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE beta #-}

data  : Set where

 :  {}  Set   Set _
 {} S = S  Set

U : Set
U = Lower (∀ (X : Set)  ( ( X)  X)   ( X))

τ :  ( U)  U
τ t = lower  X f p  t  x  p (f (raise x X f))))

σ : U   ( U)
σ s = raise s U τ

Δ :  U
Δ y = Lower (∀ p  σ y p  p (τ (σ y)))  

Ω : U 
Ω = τ  p  (∀ x  σ x p  p x))

R :  p  (∀ x  σ x p  p x)  p Ω
R _ 𝟙 = 𝟙 Ω  x  𝟙 (τ (σ x)))

M :  x  σ x Δ  Δ x
M _ 𝟚 𝟛 =
  let 𝟛 = raise 𝟛
  in 𝟛 Δ 𝟚 (lower  p  𝟛  y  p (τ (σ y)))))

L : (∀ p  (∀ x  σ x p  p x)  p Ω)  
L 𝟘 = 𝟘 Δ M (lower  p  𝟘  y  p (τ (σ y)))))

false : 
false = L R