Test15.agda

{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

module Test15 where

data ⊥ : Set where
¬_ : ∀ {a} → Set a → Set a
¬ X = X → ⊥

subst : ∀ {a b} {A : Set a} (P : A → Set b) {x y : A} → x ≡ y → P x → P y
subst P refl x = x

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

ap : ∀ {a b} {A : Set a} {B : Set b} → (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

module _ {a} (code : Set (lsuc a) → Set a)
         (decode : ∀ {X} → code X → X)
         (encode : ∀ {X} → X → code X)
         (r : ∀ {A} {x : A} → decode (encode x) ≡ x)
  where
  data V : Set (lsuc a) where
    mk : (A : Set a) → (A → V) → V

  _∈v_ : V → V → Set (lsuc a)
  x ∈v mk A f = Σ A λ i → f i ≡ x

  R : V
  R = mk (Σ (code V) λ x → code (¬ (decode x ∈v decode x))) λ
    (a , _) → decode a

  X∈R→X∉X : {X : V} → X ∈v R → ¬ (X ∈v X)
  X∈R→X∉X ((I , I∉I) , refl) = decode I∉I

  R∉R : ¬ (R ∈v R)
  R∉R R∈R = X∈R→X∉X R∈R R∈R

  X∉X→X∈R : {X : V} → ¬ (X ∈v X) → X ∈v R
  X∉X→X∈R X∉X = (_ , encode (subst (λ w → ¬ (w ∈v w)) (sym r) X∉X)) , r

  paradox : ⊥
  paradox = R∉R (X∉X→X∈R R∉R)

data Graph : Set where
  c : (ℓ' : Level) → Graph

test : c lzero ≡ c (lsuc lzero) → ⊥
test w = paradox (codeₗ rem₁) (encodeₗ rem₁) (decodeₗ rem₁) (decode-encodeₗ rem₁) where
  rem₁ : lsuc lzero ≡ lzero
  rem₁ = ap (λ { (c x) → x }) (sym w)

  codeₗ : ∀ {a b} → a ≡ b → Set a → Set b
  codeₗ refl x = x

  encodeₗ : ∀ {a b} (p : a ≡ b) {X : Set a} → codeₗ p X → X
  encodeₗ refl x = x

  decodeₗ : ∀ {a b} (p : a ≡ b) {X : Set a} → X → codeₗ p X
  decodeₗ refl x = x

  decode-encodeₗ : ∀ {a b} (p : a ≡ b) {X : Set a} {a : X} → encodeₗ p (decodeₗ p a) ≡ a
  decode-encodeₗ refl = refl